summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs163
-rw-r--r--Source/VCGeneration/Model.cs2
-rw-r--r--Test/test15/Answer100
-rw-r--r--Test/test15/CaptureState.bpl1
-rw-r--r--Test/test15/runtest.bat7
5 files changed, 107 insertions, 166 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index eda5cfda..addb92de 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -195,98 +195,6 @@ namespace Microsoft.Boogie {
m.Write(wr);
}
}
-
- /*
- if (Model == null || MvInfo == null) {
- return;
- }
- if (!Model.definedFunctions.ContainsKey("@MV_state")) {
- return;
- }
- Console.WriteLine("Captured states:");
- List<List<int>> defs = Model.definedFunctions["@MV_state"];
- List<int> states = new List<int>();
- foreach (List<int> parameters in defs) {
- if (parameters.Count == 2) { // we expect this for all but possibly the last row
- int argPartition = parameters[0];
- object val = Model.partitionToValue[argPartition];
- if (val is BigNum) {
- BigNum n = (BigNum)val;
- states.Add(n.ToInt);
- }
- }
- }
- // we now have the list of states in 'states'
- states.Sort();
-#if DEBUG_PRINT
- Console.WriteLine("DEBUG: ---------- start ----------");
- foreach (Variable v in MvInfo.AllVariables) {
- List<string> names = new List<string>();
-
- {
- string ss = v.Name;
- VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v);
- if (vvar != null) {
- string uniqueName = Context.Lookup(vvar);
- ss += " -> " + uniqueName;
- }
- names.Add(ss);
- }
-
- foreach (int s in states) {
- if (0 <= s && s < MvInfo.CapturePoints.Count) {
- VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];
- var map = m.IncarnationMap;
- if (map.ContainsKey(v)) {
- Expr e = (Expr)map[v];
- var ss = string.Format("[{0}: {1}", m.Description, e.ToString());
- IdentifierExpr ide = e as IdentifierExpr;
- if (ide != null) {
- VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);
- if (vvar != null) {
- string uniqueName = Context.Lookup(vvar);
- ss += " -> " + uniqueName;
- }
- }
- ss += "]";
- names.Add(ss);
- }
- }
- }
-
- foreach (var nm in names) {
- Console.Write("{0} ", nm);
- }
- Console.WriteLine();
- }
- Console.WriteLine("DEBUG: ---------- end ----------");
-#endif
- List<Variable> changedVariables;
- if (states.Count <= 1) {
- changedVariables = MvInfo.AllVariables;
- } else {
- VC.ModelViewInfo.Mapping last = MvInfo.CapturePoints[MvInfo.CapturePoints.Count-1];
- changedVariables = new List<Variable>();
- List<Variable> unchangedVariables = new List<Variable>();
- foreach (Variable v in MvInfo.AllVariables) {
- if (last.IncarnationMap.ContainsKey(v)) {
- changedVariables.Add(v);
- } else {
- unchangedVariables.Add(v);
- }
- }
- PrintCapturedState(8, unchangedVariables, new Hashtable());
- }
- foreach (int s in states) {
- if (0 <= s && s < MvInfo.CapturePoints.Count) {
- VC.ModelViewInfo.Mapping m = MvInfo.CapturePoints[s];
- Console.WriteLine(" {0}", m.Description);
- PrintCapturedState(8, changedVariables, m.IncarnationMap);
- } else {
- Console.WriteLine(" undefined captured-state ID {0}", s);
- }
- }
- */
}
public Model GetModelWithStates()
@@ -314,23 +222,36 @@ namespace Microsoft.Boogie {
states.Sort();
- foreach (int s in states) {
- if (0 <= s && s < MvInfo.CapturePoints.Count) {
+ for (int i = 0; i < states.Count; ++i) {
+ var s = states[i];
+ if (0 <= s && s < MvInfo.CapturePoints.Count) {
VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s];
+ var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Hashtable();
var cs = m.MkState(map.Description);
foreach (Variable v in MvInfo.AllVariables) {
var e = (Expr)map.IncarnationMap[v];
if (e == null) continue;
+ // if (prevInc[v] == e) continue; // skip unchanged variables
+
Model.Element elt;
if (e is IdentifierExpr) {
IdentifierExpr ide = (IdentifierExpr)e;
- var f = m.TryGetFunc(ide.Decl.Name);
+ // first, get the unique name
+ string uniqueName;
+ VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);
+ if (vvar == null) {
+ uniqueName = ide.Decl.Name;
+ } else {
+ uniqueName = Context.Lookup(vvar);
+ }
+
+ var f = m.TryGetFunc(uniqueName);
if (f == null) {
- f = m.MkFunc(ide.Decl.Name, 0);
+ f = m.MkFunc(uniqueName, 0);
}
elt = f.GetConstant();
} else if (e is LiteralExpr) {
@@ -351,54 +272,6 @@ namespace Microsoft.Boogie {
return m;
}
- void PrintCapturedState(int indent, List<Variable> varSet, Hashtable/*Variable -> Expr*/ incarnations) {
- Contract.Requires(0 <= indent);
- Contract.Requires(varSet != null);
- Contract.Requires(Model != null && MvInfo != null);
- string ind = new string(' ', indent);
-
- foreach (Variable v in varSet) {
- string varName = v.Name;
- Variable incarnation = v;
- string val = null;
- if (incarnations.ContainsKey(v)) {
- Expr e = (Expr)incarnations[v];
- if (e is IdentifierExpr) {
- IdentifierExpr ide = (IdentifierExpr)e;
- incarnation = ide.Decl;
- } else if (e is LiteralExpr) {
- LiteralExpr lit = (LiteralExpr)e;
- val = lit.Val.ToString();
- } else {
- val = e.ToString(); // temporary hack to have something to do in this case
- }
- }
- if (val == null) {
- // first, get the unique name
- string uniqueName;
- VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(incarnation);
- if (vvar == null) {
- uniqueName = incarnation.Name;
- } else {
- uniqueName = Context.Lookup(vvar);
- }
- // look up the value in the model
- int zid;
- if (Model.identifierToPartition.TryGetValue(uniqueName, out zid)) {
- object pvalue = Model.partitionToValue[zid];
- if (pvalue != null) {
- val = pvalue.ToString();
- } else {
- val = "*" + zid; // temporary hack to have something to do in this case
- }
- } else {
- val = uniqueName; // temporary hack to have something to do in this case
- }
- }
- Console.WriteLine("{0}{1} = {2}", ind, varName, val);
- }
- }
-
public abstract int GetLocation();
}
@@ -1427,7 +1300,7 @@ namespace VC {
if (description != null) {
Expr mv = new NAryExpr(pc.tok, new FunctionCall(mvInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));
copy = Bpl.Expr.And(mv, copy);
- mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, incarnationMap));
+ mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, (Hashtable)incarnationMap.Clone()));
}
}
Contract.Assert(copy != null);
diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs
index 5e4a0a0f..d309c01d 100644
--- a/Source/VCGeneration/Model.cs
+++ b/Source/VCGeneration/Model.cs
@@ -370,7 +370,7 @@ namespace Microsoft.Boogie
continue;
wr.WriteLine("*** STATE {0}", s.Name);
foreach (var v in s.Variables)
- wr.WriteLine("{0} -> {1}", v, s.TryGet(v));
+ wr.WriteLine(" {0} -> {1}", v, s.TryGet(v));
wr.WriteLine("*** END_STATE", s.Name);
}
wr.WriteLine("*** END_MODEL");
diff --git a/Test/test15/Answer b/Test/test15/Answer
index 974f24fc..47bff793 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -192,29 +192,91 @@ Execution trace:
Boogie program verifier finished with 0 verified, 3 errors
-------------------- CaptureState --------------------
-CaptureState.bpl(26,1): Error BP5003: A postcondition might not hold on this return path.
+CaptureState.bpl(27,1): Error BP5003: A postcondition might not hold on this return path.
CaptureState.bpl(8,3): Related location: This is the postcondition that might not hold.
Execution trace:
CaptureState.bpl(12,3): anon0
CaptureState.bpl(16,5): anon4_Then
CaptureState.bpl(24,5): anon3
-Captured states:
- Heap = *8
- F = *10
- this = *9
- x = 797
- y = y@@1
- top
- r = r
- m = -2
- then
- r = r
- m = -1
- postUpdate0
- r = r
- m = -1
- end
- r = -2
- m = -1
+*** MODEL
+@true -> 6
+@false -> 7
+intType -> *4
+boolType -> *5
+RefType -> *6
+FieldNameType -> *7
+Heap -> *8
+this -> *9
+F -> *10
+m@0 -> -2
+r@0 -> -2
+x@@4 -> 797
+m@1 -> -1
+m@3 -> -1
+$pow2 -> {
+ 0 -> 1
+}
+tickleBool -> {
+ false -> true
+ true -> true
+}
+Ctor -> {
+ *4 -> 0
+ *5 -> 1
+ *6 -> 3
+ *7 -> 4
+ *18 -> 2
+}
+type -> {
+ *8 -> *18
+ *9 -> *6
+ *10 -> *7
+ *20 -> *4
+}
+MapType0Type -> {
+ *6 *7 *4 -> *18
+}
+MapType0TypeInv2 -> {
+ *18 -> *4
+}
+MapType0TypeInv1 -> {
+ *18 -> *7
+}
+MapType0TypeInv0 -> {
+ *18 -> *6
+}
+@MV_state -> {
+ 0 -> true
+ 1 -> true
+ 2 -> true
+ 5 -> true
+}
+MapType0Select -> {
+ *8 *9 *10 -> *20
+}
+U_2_int -> {
+ *20 -> -2
+}
+int_2_U -> {
+ -2 -> *20
+}
+*** STATE <initial>
+ Heap -> *8
+ F -> *10
+ this -> *9
+*** END_STATE
+*** STATE top
+*** END_STATE
+*** STATE then
+ m -> -2
+*** END_STATE
+*** STATE postUpdate0
+ m -> -1
+*** END_STATE
+*** STATE end
+ r -> -2
+ m -> 7
+*** END_STATE
+*** END_MODEL
Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl
index 7c73c411..7635ecdc 100644
--- a/Test/test15/CaptureState.bpl
+++ b/Test/test15/CaptureState.bpl
@@ -22,5 +22,6 @@ procedure P(this: Ref, x: int, y: int) returns (r: int)
assume {:captureState "postUpdate1"} true;
}
r := m + m;
+ m := 7;
assume {:captureState "end"} true;
}
diff --git a/Test/test15/runtest.bat b/Test/test15/runtest.bat
index fc25c876..83452323 100644
--- a/Test/test15/runtest.bat
+++ b/Test/test15/runtest.bat
@@ -9,8 +9,13 @@ for %%f in (NullInModel IntInModel ModelTest) do (
echo -------------------- %%f --------------------
"%BGEXE%" %* %%f.bpl /printModel:2
)
-for %%f in (InterpretedFunctionTests CaptureState) do (
+for %%f in (InterpretedFunctionTests) do (
echo.
echo -------------------- %%f --------------------
"%BGEXE%" %* %%f.bpl
)
+for %%f in (CaptureState) do (
+ echo.
+ echo -------------------- %%f --------------------
+ "%BGEXE%" %* %%f.bpl /mv:-
+)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 23:00:52 +0000