Proof generation for CFG optimizations (Block coalescing and pruning of unreachable blocks)

.github/workflows/ci.yml

@@ -60,12 +60,21 @@ jobs:
       # for the session so that it does not have to rechecked every time
       - name: Set up Isabelle Boogie language session
         run: |
-          echo "$PWD/foundational_boogie/BoogieLang" >> isabelle_dir/ROOTS
-          isabelle_dir/bin/isabelle build -b -j4 -d $PWD/foundational_boogie/BoogieLang Boogie_Lang
+          echo "$PWD/foundational-boogie/BoogieLang" >> isabelle_dir/ROOTS
+          isabelle_dir/bin/isabelle build -b -j4 -d $PWD/foundational-boogie/BoogieLang Boogie_Lang
 
       - name: Check external benchmark proofs
         run: |
           python3 etc/scripts/check_proofs.py --inputdir table_benchmarks_proofs --reps 1
+
+      - name: Generate CFG optimization benchmarks
+        run: |
+          BOOGIE_EXE=$(find $PWD -type f -name "BoogieDriver") 
+          python3 etc/scripts/generate_proofs.py --inputdir ProofGenerationBenchmarks/cfg_optimizations_tests --outputdir cfg_optimizations_proofs --boogieproofExe $BOOGIE_EXE
+
+      #- name: Check CFG optimization proofs
+      #  run: |
+      #    python3 etc/scripts/check_proofs.py --inputdir cfg_optimizations_proofs --reps 1
 
       - name: Generate Boogie benchmark proofs
         run: |
@@ -74,4 +83,4 @@ jobs:
 
       - name: Check Boogie benchmark proofs
         run: |
-          python3 etc/scripts/check_proofs.py --inputdir boogie_benchmarks_proofs --reps 1
+          python3 etc/scripts/check_proofs.py --inputdir boogie_benchmarks_proofs --reps 1

.gitmodules

@@ -1,3 +1,4 @@
-[submodule "foundational_boogie"]
-	path = foundational_boogie
-	url = https://github.com/gauravpartha/foundational_boogie
+[submodule "foundational-boogie"]
+	path = foundational-boogie
+	url = https://github.com/viperproject/foundational-boogie
+	branch = cfg_optimizations

ProofGenerationBenchmarks/boogie_testsuite_benchmarks/inline/expansion4.bpl

@@ -1,11 +1,7 @@
 // RUN: %boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-/* MANUAL REWRITE:
 function foo(x:int) : int
   { if x <= 0 then 1 else foo(x - 1) + 2 }
-*/
-function foo(x:int) : int;
-axiom( forall x:int :: ((x <= 0 ==> foo(x) == 1) && (x > 0 ==> foo(x) == foo(x - 1) + 2)));
 
 procedure bar()
 {

ProofGenerationBenchmarks/boogie_testsuite_benchmarks/secure/simple.bpl

@@ -1,11 +1,12 @@
-//:: ProofGen(IgnoreFile)
 // Z3 4.1: /trace /proverOpt:O:smt.mbqi=true /proverOpt:O:smt.relevancy=0
-function  xor(a: bool, b: bool) returns (bool)  { (!a && b) || (a && !b) }
+
+/** MANUAL REWRITE: Replaced all xor with xorCustom (since xor is already defined in Isabelle) */
+function  xorCustom(a: bool, b: bool) returns (bool)  { (!a && b) || (a && !b) }
 
 procedure Incorrect_A(
      a: bool,  b: bool)
 returns ( ap: bool,  bp: bool)
-  ensures xor(ap, bp) == xor(a, b);
+  ensures xorCustom(ap, bp) == xorCustom(a, b);
 {
    ap := a;
    bp := b;
@@ -14,7 +15,7 @@ returns ( ap: bool,  bp: bool)
 procedure Incorrect_B(
      a: bool,  b: bool)
 returns ( ap: bool,  bp: bool)
-  ensures xor(ap, bp) == xor(a, b);
+  ensures xorCustom(ap, bp) == xorCustom(a, b);
 {
    ap := a;
    bp := b;
@@ -23,7 +24,7 @@ returns ( ap: bool,  bp: bool)
 procedure Incorrect_X(
      a: bool,  b: bool)
 returns ( ap: bool,  bp: bool)
-  ensures xor(ap, bp) == xor(a, b);
+  ensures xorCustom(ap, bp) == xorCustom(a, b);
 {
    ap := a;
    bp := b;
@@ -32,27 +33,27 @@ returns ( ap: bool,  bp: bool)
 procedure Correct_A(
      a: bool,  b: bool)
 returns ( ap: bool,  bp: bool)
-  ensures xor(ap, bp) == xor(a, b);
+  ensures xorCustom(ap, bp) == xorCustom(a, b);
 {
    havoc ap;
-   bp := xor(xor(ap, a), b);
+   bp := xorCustom(xorCustom(ap, a), b);
 }
 
 procedure Correct_B(
      a: bool,  b: bool)
 returns ( ap: bool,  bp: bool)
-  ensures xor(ap, bp) == xor(a, b);
+  ensures xorCustom(ap, bp) == xorCustom(a, b);
 {
    havoc ap;
-   bp := xor(xor(ap, a), b);
+   bp := xorCustom(xorCustom(ap, a), b);
 }
 
 procedure Correct_X(
      a: bool,  b: bool)
 returns ( ap: bool,  bp: bool)
-  ensures xor(ap, bp) == xor(a, b);
+  ensures xorCustom(ap, bp) == xorCustom(a, b);
 {
    havoc ap;
-   bp := xor(xor(ap, a), b);
+   bp := xorCustom(xorCustom(ap, a), b);
 }
 

ProofGenerationBenchmarks/boogie_testsuite_benchmarks/stratifiedinline/bar4.bpl

@@ -27,20 +27,13 @@ modifies x, y;
 }
 
 
-procedure  main() returns (b: bool)
+procedure main() returns (b: bool)
 modifies x, y;
 {
   assume x == y;
   call foo();
   if (x == y) {
     call b := bar();
-    /** MANUAL REWRITE:
     assume (if b then x+1 != y else x != y+1);
-    */
-    if(b) {
-      assume x+1 != y;
-    } else {
-      assume x != y+1;
-    }
   }
 }

ProofGenerationBenchmarks/boogie_testsuite_benchmarks/test20/issue-32.bpl

@@ -1,10 +1,12 @@
 //:: ProofGen(IgnoreFile)
 // RUN: %boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-function  Lit<T>(x: T) : T;
-axiom Lit(true);
+
+/** MANUEL REWRITE renamed Lit to LitA to avoid Isabelle Lit clash **/
+function LitA<T>(x: T) : T; 
+axiom LitA(true);
 
 procedure test()
 {
-    assert Lit(true);
+    assert LitA(true);
 }

ProofGenerationBenchmarks/boogie_testsuite_benchmarks/textbook/DivMod.bpl

@@ -7,11 +7,7 @@
 //
 // Rustan Leino, 23 Sep 2010
 
-/** MANUAL REWRITE:
 function abs(x: int): int { if 0 <= x then x else -x }
-**/
-function abs(x: int): int;
-axiom (forall x: int :: ( 0<= x ==> abs(x) == x) && ( (!(0 <= x)) ==> abs(x) == -x));
 
 function divt(int, int): int;
 function modt(int, int): int;
@@ -43,29 +39,9 @@ procedure T_from_E(a,b: int) returns (q,r: int)
   qq := dive(a,b);
   rr := mode(a,b);
 
-  /** MANUAL REWRITE
   q := if 0 <= a || rr == 0 then qq else if 0 <= b then qq+1 else qq-1;
   r := if 0 <= a || rr == 0 then rr else if 0 <= b then rr-b else rr+b;
-  **/
-  if(0 <= a || rr == 0) {
-    q := qq;
-  } else {
-    if (0<=b) {
-      q := qq+1;
-    } else {
-      q := qq-1;
-    }
-  }
-  if (0 <= a || rr == 0) {
-    r := rr;
-  } else {
-    if(0 <= b) {
-      r := rr-b;
-    } else {
-      r := rr+b;
-    }
-  }
-  assume  true;
+  assume true;
 }
 
 procedure E_from_T(a,b: int) returns (q,r: int)
@@ -84,26 +60,6 @@ procedure E_from_T(a,b: int) returns (q,r: int)
   qq := divt(a,b);
   rr := modt(a,b);
 
-  /* MANUAL REWRITE
   q := if 0 <= rr then qq else if 0 < b then qq-1 else qq+1;
   r := if 0 <= rr then rr else if 0 < b then rr+b else rr-b;
-  */
-  if(0 <= rr) {
-    q := qq;
-  } else {
-    if (0< b) {
-      q := qq-1;
-    } else {
-      q := qq+1;
-    }
-  }
-  if (0 <= rr) {
-    r := rr;
-  } else {
-    if(0 < b) {
-      r := rr+b;
-    } else {
-      r := rr-b;
-    }
-  }
 }