Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.

10 files changed, 178 insertions, 264 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 630f6f14..9a0fe64e 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -494,8 +494,6 @@ namespace Microsoft.Boogie {
 

     public override void Typecheck(TypecheckingContext tc) {

       //Contract.Requires(tc != null);

-      if (Val is BvConst && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None)

-        tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");

       this.Type = ShallowType;

     }

 

@@ -2241,9 +2239,6 @@ namespace Microsoft.Boogie {
                TypeParameters == null) {

         TypeParamInstantiation tpInsts;

         Type = Fun.Typecheck(ref Args, out tpInsts, tc);

-        if (Type != null && Type.IsBv && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None) {

-          tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");

-        }

         TypeParameters = tpInsts;

       }

       IOverloadedAppliable oa = Fun as IOverloadedAppliable;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4ebad5cc..8647e79e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -241,7 +241,6 @@ namespace Microsoft.Boogie {
       Z3Native,

       ToInt

     }

-    public BvHandling Bitvectors = BvHandling.Z3Native;

     public bool UseArrayTheory = false;

     public bool MonomorphicArrays {

       get {

@@ -945,31 +944,6 @@ namespace Microsoft.Boogie {
             ForceBplErrors = true;

             break;

 

-          case "-bv":

-          case "/bv":

-            if (ps.ConfirmArgumentCount(1)) {

-              if (TheProverFactory == null) {

-                TheProverFactory = ProverFactory.Load("Z3");

-                ProverName = "Z3".ToUpper();

-              }

-

-              switch (args[ps.i]) {

-                case "n":

-                  Bitvectors = BvHandling.None;

-                  break;

-                case "z":

-                  Bitvectors = BvHandling.Z3Native;

-                  break;

-                case "i":

-                  Bitvectors = BvHandling.ToInt;

-                  break;

-                default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-                  break;

-              }

-            }

-            break;

-

           case "-contractInfer":

           case "/contractInfer":

             ContractInfer = true;

@@ -1918,15 +1892,6 @@ namespace Microsoft.Boogie {
      {:verify false}

        Skip verification of an implementation.

 

-     {:forceBvZ3Native true}

-       Verify the given implementation with the native Z3 bitvector

-       handling. Only works if /bv:i (or /bv:z, but then it does not do

-       anything) is given on the command line.

-

-     {:forceBvInt true}

-       Use int translation for the given implementation. Only work with

-       /bv:z (or /bv:i).

-

      {:vcs_max_cost N}

      {:vcs_max_splits N}

      {:vcs_max_keep_going_splits N}

@@ -1942,12 +1907,9 @@ namespace Microsoft.Boogie {
 

   ---- On functions ----------------------------------------------------------

 

+     {:builtin ""spec""}

      {:bvbuiltin ""spec""}

-       Z3 specific, used only with /bv:z.

-

-     {:bvint ""fn""}

-       With /bv:i rewrite the function to function symbol 'fn', except if

-       the 'fn' is 'id', in which case just strip the function altogether.

+       Rewrite the function to built-in prover function symbol 'fn'.

 

      {:never_pattern true}

        Terms starting with this function symbol will never be

@@ -2177,10 +2139,6 @@ namespace Microsoft.Boogie {
                    statement in that position) is ignored in checking contexts

                    (like other free things); this option includes these free

                    loop invariants as assumes in both contexts

-  /bv:<bv>       : bitvector handling

-                   n = none

-                   z = native Z3 bitvectors (default)

-                   i = unsoundly translate bitvectors to integers

   /inline:<i>    : use inlining strategy <i> for procedures with the :inline

                    attribute, see /attrHelp for details:

                    none

diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 60a8de22..8bf6bbf0 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie.Isabelle {
     public readonly bool AllTypes;

 

     public IsabelleContext(string outputFilename, bool allTypes)

-      : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/>(new string/*!*/[] { "bvInt", "bvDefSem", "bvint", "bvz", "external" }))) {

+      : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/> { "bvInt", "bvDefSem", "bvint", "bvz", "external" })) {

       Contract.Requires(outputFilename != null);

 

       this.OutputFilename = outputFilename;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 134cff4c..24e083d0 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -49,19 +49,7 @@ namespace Microsoft.Boogie {
     public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);

 

     private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {

-      if (impl == null)

-        return CommandLineOptions.Clo.Bitvectors;

-      bool force_int = false;

-      bool force_native = false;

-      cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);

-      impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

-      impl.CheckBooleanAttribute("forceBvInt", ref force_int);

-      impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native);

-      if (force_native)

-        return CommandLineOptions.BvHandling.Z3Native;

-      if (force_int)

-        return CommandLineOptions.BvHandling.ToInt;

-      return CommandLineOptions.Clo.Bitvectors;

+      return CommandLineOptions.BvHandling.Z3Native;

     }

 

     public bool WillingToHandle(Implementation impl, int timeout) {

diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer
index f0f65b04..e20474d9 100644
--- a/Test/bitvectors/Answer
+++ b/Test/bitvectors/Answer
@@ -28,12 +28,6 @@ Boogie program verifier finished with 1 verified, 0 errors
 bv7.bpl(4,14): error: arguments of extract need to be integer literals

 bv7.bpl(5,15): error: parentheses around bitvector bounds are not allowed

 2 parse errors detected in bv7.bpl

--------------------- bv4.bpl - /bv:n --------------------

-bv4.bpl(3,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-bv4.bpl(3,13): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-bv4.bpl(5,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-bv4.bpl(5,14): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-4 type checking errors detected in bv4.bpl

 -------------------- bv5.bpl --------------------

 bv5.bpl(10,3): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -52,6 +46,6 @@ Boogie program verifier finished with 2 verified, 0 errors
 -------------------- bv10.bpl --------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

--------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------

+-------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat
index a0480645..2a140368 100644
--- a/Test/bitvectors/runtest.bat
+++ b/Test/bitvectors/runtest.bat
@@ -5,16 +5,13 @@ set BGEXE=..\..\Binaries\Boogie.exe
 

 for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do (

   echo -------------------- %%f --------------------

-  %BGEXE% /proverWarnings:1 /bv:z %* /logPrefix:-0 %%f

+  %BGEXE% /proverWarnings:1 %* %%f

 )

 

-echo -------------------- bv4.bpl - /bv:n --------------------

-%BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl

-

 for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do (

   echo -------------------- %%f --------------------

   %BGEXE% %* %%f

 )

 

-echo -------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------

-%BGEXE% /bv:z /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl

+echo -------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------

+%BGEXE% /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index 9a6c95a3..954ea799 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -64,6 +64,10 @@ Boogie program verifier finished with 1 verified, 0 errors
 t3.bpl(38,5): Error BP5001: This assertion might not hold.

 Execution trace:

     t3.bpl(19,3): anon0

+    t3.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t3.bpl(11,5): anon0

+    Inlined call to procedure foo ends

     t3.bpl(27,3): anon3_LoopBody

     t3.bpl(23,3): anon3_LoopHead

     Inlined call to procedure foo begins

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index 290059d6..aee2722e 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -2,31 +2,31 @@
 bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.

 bar1.bpl(21,1): Related location: This is the postcondition that might not hold.

 Execution trace:

-        bar1.bpl(24,3): anon0

-        Inlined call to procedure foo begins

-            bar1.bpl(13,5): anon0

-            Inlined call to procedure bar begins

-                bar1.bpl(7,5): anon0

-            Inlined call to procedure bar ends

-            Inlined call to procedure bar begins

-                bar1.bpl(7,5): anon0

-            Inlined call to procedure bar ends

-        Inlined call to procedure foo ends

+    bar1.bpl(24,3): anon0

+    Inlined call to procedure foo begins

+        bar1.bpl(13,5): anon0

+        Inlined call to procedure bar begins

+            bar1.bpl(7,5): anon0

+        Inlined call to procedure bar ends

+        Inlined call to procedure bar begins

+            bar1.bpl(7,5): anon0

+        Inlined call to procedure bar ends

+    Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar2.bpl

 bar2.bpl(21,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        bar2.bpl(19,3): anon0

-        Inlined call to procedure foo begins

-            bar2.bpl(5,3): anon0

-            bar2.bpl(6,7): anon3_Then

-        Inlined call to procedure foo ends

-        Inlined call to procedure foo begins

-            bar2.bpl(5,3): anon0

-            bar2.bpl(9,7): anon3_Else

-        Inlined call to procedure foo ends

+    bar2.bpl(19,3): anon0

+    Inlined call to procedure foo begins

+        bar2.bpl(5,3): anon0

+        bar2.bpl(9,7): anon3_Else

+    Inlined call to procedure foo ends

+    Inlined call to procedure foo begins

+        bar2.bpl(5,3): anon0

+        bar2.bpl(6,7): anon3_Then

+    Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

@@ -34,23 +34,23 @@ Boogie program verifier finished with 0 verified, 1 error
 bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.

 bar3.bpl(34,1): Related location: This is the postcondition that might not hold.

 Execution trace:

-        bar3.bpl(38,3): anon0

-        Inlined call to procedure foo begins

-            bar3.bpl(18,3): anon0

-            bar3.bpl(19,7): anon3_Then

-            Inlined call to procedure bar begins

-                bar3.bpl(7,3): anon0

-                bar3.bpl(8,7): anon3_Then

-            Inlined call to procedure bar ends

-            Inlined call to procedure bar begins

-                bar3.bpl(7,3): anon0

-                bar3.bpl(8,7): anon3_Then

-            Inlined call to procedure bar ends

-        Inlined call to procedure foo ends

+    bar3.bpl(38,3): anon0

+    Inlined call to procedure foo begins

+        bar3.bpl(18,3): anon0

+        bar3.bpl(19,7): anon3_Then

+        Inlined call to procedure bar begins

+            bar3.bpl(7,3): anon0

+            bar3.bpl(8,7): anon3_Then

+        Inlined call to procedure bar ends

         Inlined call to procedure bar begins

             bar3.bpl(7,3): anon0

-            bar3.bpl(10,7): anon3_Else

+            bar3.bpl(8,7): anon3_Then

         Inlined call to procedure bar ends

+    Inlined call to procedure foo ends

+    Inlined call to procedure bar begins

+        bar3.bpl(7,3): anon0

+        bar3.bpl(10,7): anon3_Else

+    Inlined call to procedure bar ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 11f0e658..4e3886aa 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -2,56 +2,49 @@
 -------------------- NullInModel --------------------

 Z3 error model: 

 partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 3:int

-*3 {@false} -> 4:int

+*0 {%lbl%+24 %lbl%+37} -> true

+*1 {%lbl%@47} -> false

+*2 {s null} 

+*3 {refType} 

 *4 {intType} 

 *5 {boolType} 

-*6 {refType} 

-*7 {s null} 

-*8 -> 0:int

-*9 -> 1:int

-*10 -> 2:int

-*11 

+*6 -> 0:int

+*7 -> 1:int

+*8 -> 2:int

+*9 

 function interpretations:

-$pow2 -> {

-  *8 -> *9

-  else -> #unspecified

-}

 tickleBool -> {

-  *1 -> *0

   *0 -> *0

+  *1 -> *0

   else -> #unspecified

 }

-Ctor -> {

-  *4 -> *8

-  *5 -> *9

-  *6 -> *10

+type -> {

+  *2 -> *3

   else -> #unspecified

 }

-type -> {

-  *7 -> *6

+Ctor -> {

+  *4 -> *6

+  *5 -> *7

+  *3 -> *8

   else -> #unspecified

 }

 END_OF_MODEL

 .

 identifierToPartition:

-@true : *2

-@false : *3

+%lbl%+24 : *0

+%lbl%+37 : *0

+%lbl%@47 : *1

+s : *2

+null : *2

+refType : *3

 intType : *4

 boolType : *5

-refType : *6

-s : *7

-null : *7

 valueToPartition:

 True : *0

 False : *1

-3 : *2

-4 : *3

-0 : *8

-1 : *9

-2 : *10

+0 : *6

+1 : *7

+2 : *8

 End of model.

 NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -62,45 +55,38 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- IntInModel --------------------

 Z3 error model: 

 partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 2:int

-*3 {@false} -> 3:int

-*4 {intType} 

-*5 {boolType} 

-*6 {i} -> 0:int

-*7 -> 1:int

-*8 

+*0 {%lbl%+29 %lbl%+23} -> true

+*1 {%lbl%@39} -> false

+*2 {intType} 

+*3 {boolType} 

+*4 {i} -> 0:int

+*5 -> 1:int

+*6 

 function interpretations:

-$pow2 -> {

-  *6 -> *7

-  else -> #unspecified

-}

 tickleBool -> {

-  *1 -> *0

   *0 -> *0

+  *1 -> *0

   else -> #unspecified

 }

 Ctor -> {

-  *4 -> *6

-  *5 -> *7

+  *2 -> *4

+  *3 -> *5

   else -> #unspecified

 }

 END_OF_MODEL

 .

 identifierToPartition:

-@true : *2

-@false : *3

-intType : *4

-boolType : *5

-i : *6

+%lbl%+29 : *0

+%lbl%+23 : *0

+%lbl%@39 : *1

+intType : *2

+boolType : *3

+i : *4

 valueToPartition:

 True : *0

 False : *1

-2 : *2

-3 : *3

-0 : *6

-1 : *7

+0 : *4

+1 : *5

 End of model.

 IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -111,66 +97,59 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- ModelTest --------------------

 Z3 error model: 

 partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 5:int

-*3 {@false} -> 6:int

-*4 {intType} 

-*5 {boolType} 

+*0 {%lbl%+64 %lbl%+119} -> true

+*1 {%lbl%@182} -> false

+*2 {s} 

+*3 {j@2} -> 4:int

+*4 {boolType} 

+*5 {intType} 

 *6 {refType} 

-*7 {s} 

-*8 {r} 

-*9 {i@0} -> 1:int

-*10 {j@0} -> 2:int

-*11 {j@1} -> 3:int

-*12 {j@2} -> 4:int

-*13 -> 0:int

-*14 

+*7 {i@0} -> 1:int

+*8 {j@0} -> 2:int

+*9 {j@1} -> 3:int

+*10 {r} 

+*11 -> 0:int

+*12 

 function interpretations:

-$pow2 -> {

-  *13 -> *9

-  else -> #unspecified

-}

 tickleBool -> {

-  *1 -> *0

   *0 -> *0

+  *1 -> *0

   else -> #unspecified

 }

-Ctor -> {

-  *4 -> *13

-  *5 -> *9

-  *6 -> *10

+type -> {

+  *2 -> *6

+  *10 -> *6

   else -> #unspecified

 }

-type -> {

-  *7 -> *6

-  *8 -> *6

+Ctor -> {

+  *5 -> *11

+  *4 -> *7

+  *6 -> *8

   else -> #unspecified

 }

 END_OF_MODEL

 .

 identifierToPartition:

-@true : *2

-@false : *3

-intType : *4

-boolType : *5

+%lbl%+64 : *0

+%lbl%+119 : *0

+%lbl%@182 : *1

+s : *2

+j@2 : *3

+boolType : *4

+intType : *5

 refType : *6

-s : *7

-r : *8

-i@0 : *9

-j@0 : *10

-j@1 : *11

-j@2 : *12

+i@0 : *7

+j@0 : *8

+j@1 : *9

+r : *10

 valueToPartition:

 True : *0

 False : *1

-5 : *2

-6 : *3

-1 : *9

-2 : *10

-3 : *11

-4 : *12

-0 : *13

+4 : *3

+1 : *7

+2 : *8

+3 : *9

+0 : *11

 End of model.

 ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -199,86 +178,85 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

 *** MODEL

-@true -> 6

-@false -> 7

+%lbl%+112 -> true

+%lbl%+116 -> true

+%lbl%+110 -> true

+%lbl%+189 -> true

+%lbl%@334 -> false

+m@3 -> -1

+m@2 -> -1

+this -> *3

 intType -> *4

-boolType -> *5

-RefType -> *6

-FieldNameType -> *7

-Heap -> *8

-this -> *9

-F -> *10

-@MV_state_const -> 8

+Heap -> *5

+FieldNameType -> *6

 m@0 -> -2

 r@0 -> -2

+boolType -> *8

+RefType -> *9

+F -> *10

+@MV_state_const -> 6

 x@@4 -> 797

-m@2 -> -1

-m@3 -> -1

 y@@1 -> **y@@1

 r -> **r

 m -> **m

-$pow2 -> {

-  0 -> 1

-  else -> *23

-}

 tickleBool -> {

-  false -> true

   true -> true

-  else -> *23

-}

-Ctor -> {

-  *4 -> 0

-  *5 -> 1

-  *6 -> 3

-  *7 -> 4

-  *19 -> 2

-  else -> *23

+  false -> true

+  else -> true

 }

 type -> {

-  *8 -> *19

-  *9 -> *6

-  *10 -> *7

+  *5 -> *13

+  *3 -> *9

+  *10 -> *6

   -2 -> *4

-  else -> *23

+  else -> *13

 }

-MapType0Type -> {

-  *6 *7 *4 -> *19

-  else -> *23

-}

-MapType0TypeInv2 -> {

-  *19 -> *4

-  else -> *23

-}

-MapType0TypeInv1 -> {

-  *19 -> *7

-  else -> *23

-}

-MapType0TypeInv0 -> {

-  *19 -> *6

-  else -> *23

+Ctor -> {

+  *4 -> 0

+  *8 -> 1

+  *9 -> 3

+  *6 -> 4

+  *13 -> 2

+  else -> 0

 }

 @MV_state -> {

-  8 0 -> true

-  8 3 -> true

-  8 4 -> true

-  8 5 -> true

-  else -> *23

+  6 0 -> true

+  6 3 -> true

+  6 4 -> true

+  6 5 -> true

+  else -> true

 }

 [3] -> {

-  *8 *9 *10 -> -2

-  else -> *23

+  *5 *3 *10 -> -2

+  else -> -2

 }

 U_2_int -> {

   -2 -> -2

-  else -> *23

+  else -> -2

+}

+MapType0TypeInv1 -> {

+  *13 -> *6

+  else -> *6

+}

+MapType0Type -> {

+  *9 *6 *4 -> *13

+  else -> *13

+}

+MapType0TypeInv2 -> {

+  *13 -> *4

+  else -> *4

+}

+MapType0TypeInv0 -> {

+  *13 -> *9

+  else -> *9

 }

 int_2_U -> {

   -2 -> -2

-  else -> *23

+  else -> -2

 }

 *** STATE <initial>

-  Heap -> *8

-  this -> *9

+  Heap -> *5

+  this -> *3

   x -> 797

   y -> **y@@1

   r -> **r

diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 3dc7d0c3..8ce2f66e 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -24,7 +24,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
 )

 

 echo -------------------- sk_hack.bpl --------------------

-%BGEXE% %* /noinfer /bv:z sk_hack.bpl

+%BGEXE% %* /noinfer sk_hack.bpl

 

 for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (

   echo.