Interim State

keydeps/README.user

@@ -4,9 +4,9 @@
 # Execute this in this folder.
 
 # Set to key/key/deployment/components/
-COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
+#COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
 #COMPONENTS=$HOME/work/key/key/deployment/components/
-#COMPONENTS=lib/components/
+COMPONENTS=lib/components/
 
 
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/Facade.java

@@ -75,6 +75,7 @@ public abstract class Facade {
         TransformAst astt = new TransformAst();
         ScriptLanguageParser.StartContext ctx = parseStream(stream);
         if (ctx.exception != null) throw ctx.exception;
+
         ctx.accept(astt);
         return astt.getScripts();
     }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java

@@ -26,6 +26,7 @@ package edu.kit.iti.formal.psdbg.parser;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import edu.kit.iti.formal.psdbg.parser.types.Type;
 import lombok.Getter;
+import lombok.NonNull;
 import lombok.Setter;
 
 import java.util.Iterator;
@@ -272,7 +273,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
     }
 
     @Override
-    public Void visit(FunctionCall func) {
+    public Void visit(@NonNull FunctionCall func) {
         s.append(func.getFunction().getName())
                 .append('(');
         func.getArguments().forEach(a -> {

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java

@@ -55,10 +55,10 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     private final List<ProofScript> scripts = new ArrayList<>(10);
     @Getter
     @Setter
-    private FunctionRegister functionRegister = new FunctionRegister();
+    private FunctionRegister functionRegister = FunctionRegister.getDefault();
 
     public TransformAst() {
-        functionRegister.loadDefault();
+        //functionRegister.loadDefault();
     }
 
     @Override

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Signature.java

@@ -55,7 +55,8 @@ public class Signature extends ASTNode<ScriptLanguageParser.ArgListContext> impl
     public Signature copy() {
         Signature signature = new Signature();
         forEach((k, v) -> signature.put(k.copy(), v));
-        signature.setRuleContext(this.ruleContext);
+        if (this.ruleContext != null)
+            signature.setRuleContext(this.ruleContext);
         return signature;
     }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/function/FunctionRegister.java

@@ -14,12 +14,17 @@ import java.util.ServiceLoader;
 public class FunctionRegister {
     private Map<String, ScriptFunction> functions = new HashMap<>();
 
+    public static FunctionRegister getDefault() {
+        return new FunctionRegister().loadDefault();
+    }
+
     /**
      * Load the default script functions via {@link java.util.ServiceLoader}.
      */
-    public void loadDefault() {
+    public FunctionRegister loadDefault() {
         ServiceLoader<ScriptFunction> sf = ServiceLoader.load(ScriptFunction.class);
         sf.forEach(s -> put(s.getName(), s));
+        return this;
     }
 
     public int size() {

lang/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.parser.function.ScriptFunction

+edu.kit.iti.formal.psdbg.interpreter.functions.FindInSequence
\ No newline at end of file

matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestComplexMatch.java

+package edu.kit.iti.formal.psdbg.termmatcher;
+
+
+import de.uka.ilkd.key.api.KeYApi;
+import de.uka.ilkd.key.api.ProofApi;
+import de.uka.ilkd.key.api.ProofManagementApi;
+import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.proof.init.ProofInputException;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import org.junit.Test;
+
+import java.io.File;
+import java.util.regex.Pattern;
+
+/*
+         shouldMatchSeq("seqPerm(seqDef{int u;}(0, result_1.length, any::select(heapAfter_copyArray_0, result_1, arr(u))), seqDef{int u;}(0, result_0.length, any::select(heapAfter_copyArray_0, result_0, arr(u))))",
+                "seqPerm(?X, ?Y)");
+ */
+public class TestComplexMatch {
+    @Test
+    public void test() throws ProblemLoaderException, ProofInputException {
+        ProofManagementApi a = KeYApi.loadFromKeyFile(new File("src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/project.key"));
+        ProofApi pa = a.startProof(a.getProofContracts().get(3));
+        Sequent sequent = pa.getProof().root().sequent();
+        System.out.println(sequent);
+       /* Matchings result = MatcherFacade.matches("... update-application(_, ?X) ...", sequent, false);
+        System.out.println(result);
+        String exp = normalize("\\<{exc=null;try { result=self.foo(_x)@Test;} catch (java.lang.Throwable e) { exc=e; } }\\> (and(and(and(gt(result,Z(0(#))),java.lang.Object::<inv>(heap,self)),equals(exc,null)),all{f:Field}(all{o:java.lang.Object}(or(or(elementOf(o,f,allLocs),and(not(equals(o,null)),not(equals(boolean::select(heapAtPre,o,java.lang.Object::<created>),TRUE)))),equals(any::select(heap,o,f),any::select(heapAtPre,o,f)))))))");
+        String x = normalize(result.iterator().next().get("?X").getUnit().toString().replace("\n", " "));
+        Assert.assertEquals(exp, x);*/
+    }
+
+    private String normalize(String s) {
+        Pattern re = Pattern.compile("\\s+");
+        return re.matcher(s).replaceAll(" ");
+    }
+
+}

matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/Simple.java

+ public final class Simple {
+ 
+ 
+    boolean b1;
+    boolean b2;
+    
+    /*@ public normal_behavior
+      @ ensures \dl_seqPerm(\dl_array2seq(\result), \old(\dl_array2seq(aarr)));
+      @ assignable \everything;
+     */
+    public int[] transitive(int[] aarr){
+        aarr = Simple.copyArray(aarr); 
+        sort(aarr); 
+        int[] barr = Simple.copyArray(aarr);
+        
+        if(b1){barr = Simple.copyArray(aarr);} 
+        if(b2){log(barr);}
+        return barr;
+    }
+
+    /*@ public normal_behavior
+      @ ensures \dl_seqPerm(\dl_array2seq(a), \old(\dl_array2seq(a)));
+      @ assignable a[*];
+      */
+    public void sort(int[] a){};
+
+    /*@ public normal_behavior
+      @ ensures (\forall int i; 0 <= i < input.length; input[i] == \result[i]) 
+      @ && \result.length == input.length;
+      @ ensures \fresh(\result);
+      @ ensures \dl_seqPerm(\dl_array2seq(\result), \dl_array2seq(input));
+      @ assignable \nothing;
+      */
+    public /*@helper@*/ static int[] copyArray(int[] input){}
+
+    /*@ public normal_behavior
+      @ assignable \strictly_nothing;
+      */
+    public void log(int[] a){};
+
+}

matcher/src/test/resources/edu/kit/iti/formal/psdbg/termmatcher/javacomplex/project.key

+\javaSource "";
+\chooseContract
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps

@@ -2,7 +2,10 @@
 //
 script test23(){
 impRight;
-impLeft;
+x:term := find(match `?rt ==>`);
+impLeft formula=x;
+
+
 cases{
     case match `q==>`:
       impRight;

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/transitive/script.kps

@@ -2,14 +2,20 @@
 script prove_transitive(){
  symbex;
  foreach{
- simp_upd;
+   simp_upd;
+   simp_heap;
+
    //simp_heap;
  }
  cases{
-  // case match  `seqPerm(?Res0Copy, ?Arr), seqPerm(?R, ?Res0Copy) ==>`:
+ // case match  `seqPerm(?Res0Copy, ?Arr), seqPerm(?R, ?Res0Copy) ==>`:
 
    //case match `seqPerm(?Res0Copy, ?Arr), seqPerm(?Res0Sort, ?Res0Copy), seqPerm(?Res1Copy0, ?Res0Sort),seqPerm(?Res2Copy1, ?Res0Sort) ==> seqPerm(?Res2Copy1, ?Arr)`:
-   // SeqPermSym on=`seqPerm(?Res0Copy, ?Arr) ==>`;
+   // SeqPermSym on=`seqPerm(?Res0Copy, ?Arr) ==>`[];
+
+   // case match `seqPerm(?Res0Copy, ?Arr):?X, seqPerm(?Res0Sort, ?Res0Copy), seqPerm(?Res1Copy0, ?Res0Sort),seqPerm(?Res2Copy1, ?Res0Sort) ==> seqPerm(?Res2Copy1, ?Arr)`:
+   //     SeqPermSym on=X;
+
    // SeqPermSym on=`seqPerm(?Res0Sort, ?Res0Copy) ==>`;
    // SeqPermSym on=`seqPerm(?Res1Copy0, ?Res0Sort)==>`;
    // SeqPermSym on=`seqPerm(?Res2Copy1, ?Res0Sort) ==>`;