using model instead of labels

5 files changed, 62 insertions, 4 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index b478f11d..1a08cb54 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -447,6 +447,7 @@ namespace Microsoft.Boogie {
     public int EnhancedErrorMessages = 0;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public bool UseArrayTheory = false;

+    public bool UseLabels = false;

     public bool MonomorphicArrays {

       get {

         return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic;

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 40492ce4..7ffe8323 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -187,7 +187,7 @@ namespace Microsoft.Boogie.SMTLib
       if (common.Length == 0) {

         SendCommon("(set-option :print-success false)");

         SendCommon("(set-info :smt-lib-version 2.0)");

-        if (options.ExpectingModel())

+        if (options.ProduceModel())

           SendCommon("(set-option :produce-models true)");

         foreach (var opt in options.SmtOptions) {

           SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

@@ -449,9 +449,38 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    private string[] CalculatePath() {

+      SendThisVC("(get-value ((ControlFlow @cfc 0)))");

+      var path = new List<string>();

+      while (true) {

+        var resp = Process.GetProverResponse();

+        if (resp == null)

+          break;

+        if (!(resp.Name == "" && resp.ArgCount == 1)) break;

+        resp = resp.Arguments[0];

+        if (!(resp.Name == "" && resp.ArgCount == 2)) break;

+        resp = resp.Arguments[1];

+        var v = resp.Name;

+        if (v == "-" && resp.ArgCount == 1) 

+          v += resp.Arguments[0].Name;

+        else if (resp.ArgCount != 0) 

+          break;

+        if (v.StartsWith("-")) {

+          path.Add("@" + v.Substring(1));

+          break;

+        }

+        else {

+          path.Add("+" + v);

+        }

+        SendThisVC("(get-value ((ControlFlow @cfc " + v + ")))");

+      }

+      return path.ToArray();

+    }

+

     private string[] GetLabelsInfo(ErrorHandler handler)

     {

-      SendThisVC("(labels)");

+      if (CommandLineOptions.Clo.UseLabels)

+        SendThisVC("(labels)");

       if (options.ExpectingModel())

         SendThisVC("(get-model)");

       Process.Ping();

@@ -499,6 +528,14 @@ namespace Microsoft.Boogie.SMTLib
         }

       }

 

+      if (!CommandLineOptions.Clo.UseLabels) {

+        res = CalculatePath();

+        if (res.Length == 0) 

+          res = null;

+        else

+          labelNums = res.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

+      }

+

       if (labelNums != null) {

         ErrorModel m = null;

         if (theModel != null)

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index b7b7f24d..6fe025c0 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -41,6 +41,11 @@ namespace Microsoft.Boogie.SMTLib
     public string Inspector = null;

     public bool OptimizeForBv = false;

 

+    public bool ProduceModel() {

+      return !CommandLineOptions.Clo.UseLabels ||

+             ExpectingModel();

+    }

+

     public bool ExpectingModel()

     {

         return CommandLineOptions.Clo.PrintErrorModel >= 1 ||

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6026b862..49fa7144 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1536,9 +1536,24 @@ namespace VC {
           }

 		  ));

 

-        VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);

+        LocalVariable controlFlowVariable = null;

+

+        if (!CommandLineOptions.Clo.UseLabels) {

+          controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

+          impl.LocVars.Add(controlFlowVariable);

+        }

+

+        VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariable, label2absy, checker);

         Contract.Assert(vc != null);

 

+        if (!CommandLineOptions.Clo.UseLabels) {

+          VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);

+          Contract.Assert(controlFlowVariableExpr != null);

+          VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

+          Contract.Assert(controlFlowFunctionAppl != null);

+          vc = ctx.ExprGen.Implies(ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))), vc);

+        }

+        

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

           reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);

         } else {

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b84df433..6d4d8051 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -134,7 +134,7 @@ namespace VC {
             Contract.Assert(controlFlowVariableExpr != null);

             VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId)));

             Contract.Assert(controlFlowFunctionAppl != null);

-            VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(ac.UniqueId)));

+            VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(-ac.UniqueId)));

             if (ctxt.Label2absy == null) {

               return gen.AndSimp(gen.Implies(assertFailure, C), gen.Implies(C, N));

             } else {