diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 6 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 3 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 19 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 15 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 93 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 102 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 178 | ||||
| -rw-r--r-- | Source/Graph/Graph.cs | 51 | ||||
| -rw-r--r-- | Source/Model/Model.cs | 28 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 6 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 699 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 122 | ||||
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 636 | ||||
| -rw-r--r-- | Source/Provers/Z3api/StubContext.cs | 3 | ||||
| -rw-r--r-- | Source/Provers/Z3api/TypeAdapter.cs | 121 | ||||
| -rw-r--r-- | Source/Provers/Z3api/VCExprVisitor.cs | 432 | ||||
| -rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 10 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 42 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 188 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 436 |
23 files changed, 1443 insertions, 1761 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index dcc007fe..88d8bdaa 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -512,6 +512,12 @@ namespace Microsoft.Boogie { }
outcome = svcgen.FindLeastToVerify(impl, program, ref ss);
errors = new List<Counterexample>();
+ Console.Write("Result: ");
+ foreach (var s in ss)
+ {
+ Console.Write("{0} ", s);
+ }
+ Console.WriteLine();
}
else
{
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 87b48740..825efa21 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -813,6 +813,9 @@ namespace Microsoft.Boogie { // VC generation and SCC computation
public BlockSeq/*!*/ Predecessors;
+ // This field is used during passification to null-out entries in block2Incartion hashtable early
+ public int succCount;
+
public HashSet<Variable/*!*/> liveVarsBefore;
[ContractInvariantMethod]
void ObjectInvariant() {
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 84ecce6d..8f2d0c68 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -259,6 +259,7 @@ namespace Microsoft.Boogie { BlockReach,
BlockNestedReach,
Dag,
+ DagIterative,
Doomed,
Unspecified
}
@@ -1049,6 +1050,9 @@ namespace Microsoft.Boogie { case "dag":
vcVariety = VCVariety.Dag;
break;
+ case "i":
+ vcVariety = VCVariety.DagIterative;
+ break;
case "doomed":
vcVariety = VCVariety.Doomed;
break;
@@ -1526,6 +1530,7 @@ namespace Microsoft.Boogie { TypeEncodingMethod = TypeEncoding.Monomorphic;
UseArrayTheory = true;
UseAbstractInterpretation = false;
+ MaxProverMemory = 0; // no max: avoids restarts
if (ProverName == "Z3API")
{
ProverCCLimit = 1;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 071dbd64..033bc239 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -843,6 +843,7 @@ WhileStmt<out Statement/*!*/ stmt> Expression guard;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ List<FrameExpression/*!*/> mod = null;
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
List<GuardedAlternative> alternatives;
@@ -851,20 +852,21 @@ WhileStmt<out Statement/*!*/ stmt> "while" (. x = t; .)
(
Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
- LoopSpec<out invariants, out decreases>
+ LoopSpec<out invariants, out decreases, out mod>
BlockStmt<out body, out bodyStart, out bodyEnd>
- (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
+ (. stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); .)
|
- LoopSpec<out invariants, out decreases>
+ LoopSpec<out invariants, out decreases, out mod>
AlternativeBlock<out alternatives>
- (. stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives); .)
+ (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)
)
.
-LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases.>
-= (. bool isFree; Expression/*!*/ e;
+LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
+= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
+ mod = null;
.)
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
@@ -873,6 +875,11 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!* Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
";"
| "decreases" DecreasesList<decreases, true> ";"
+ | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)
+ [ FrameExpression<out fe> (. mod.Add(fe); .)
+ { "," FrameExpression<out fe> (. mod.Add(fe); .)
+ }
+ ] ";"
}
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 99cf791f..0fd83011 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1660,20 +1660,25 @@ namespace Microsoft.Dafny { {
public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;
public readonly List<Expression/*!*/>/*!*/ Decreases;
+ public readonly List<FrameExpression/*!*/>/*!*/ Mod;
+ public readonly bool explictModifies;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Invariants));
Contract.Invariant(cce.NonNullElements(Decreases));
+ Contract.Invariant(Mod == null || cce.NonNullElements(Mod));
}
- public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases)
+ public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)
: base(tok)
{
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(invariants));
Contract.Requires(cce.NonNullElements(decreases));
+ Contract.Requires(mod == null || cce.NonNullElements(mod));
this.Invariants = invariants;
this.Decreases = decreases;
+ this.Mod = mod;
}
}
@@ -1687,9 +1692,9 @@ namespace Microsoft.Dafny { }
public WhileStmt(IToken tok, Expression guard,
- List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
+ List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,
Statement/*!*/ body)
- : base(tok, invariants, decreases) {
+ : base(tok, invariants, decreases, mod) {
Contract.Requires(tok != null);
Contract.Requires(body != null);
this.Guard = guard;
@@ -1705,9 +1710,9 @@ namespace Microsoft.Dafny { Contract.Invariant(Alternatives != null);
}
public AlternativeLoopStmt(IToken tok,
- List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
+ List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/> mod,
List<GuardedAlternative> alternatives)
- : base(tok, invariants, decreases) {
+ : base(tok, invariants, decreases, mod) {
Contract.Requires(tok != null);
Contract.Requires(alternatives != null);
this.Alternatives = alternatives;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 41fc89c5..b77f5e65 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,7 +25,7 @@ public class Parser { const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -144,10 +144,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -160,15 +160,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -192,7 +192,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -1189,6 +1189,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expression guard;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ List<FrameExpression/*!*/> mod = null;
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
List<GuardedAlternative> alternatives;
@@ -1199,13 +1200,13 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 33) {
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- LoopSpec(out invariants, out decreases);
+ LoopSpec(out invariants, out decreases, out mod);
BlockStmt(out body, out bodyStart, out bodyEnd);
- stmt = new WhileStmt(x, guard, invariants, decreases, body);
+ stmt = new WhileStmt(x, guard, invariants, decreases, mod, body);
} else if (StartOf(11)) {
- LoopSpec(out invariants, out decreases);
+ LoopSpec(out invariants, out decreases, out mod);
AlternativeBlock(out alternatives);
- stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
+ stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives);
} else SynErr(121);
}
@@ -1388,12 +1389,13 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(8);
}
- void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases) {
- bool isFree; Expression/*!*/ e;
+ void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod) {
+ bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
+ mod = null;
- while (la.kind == 29 || la.kind == 32 || la.kind == 59) {
+ while (StartOf(13)) {
if (la.kind == 29 || la.kind == 59) {
isFree = false;
if (la.kind == 29) {
@@ -1404,10 +1406,23 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(17);
- } else {
+ } else if (la.kind == 32) {
Get();
DecreasesList(decreases, true);
Expect(17);
+ } else {
+ Get();
+ mod = mod ?? new List<FrameExpression>();
+ if (StartOf(8)) {
+ FrameExpression(out fe);
+ mod.Add(fe);
+ while (la.kind == 19) {
+ Get();
+ FrameExpression(out fe);
+ mod.Add(fe);
+ }
+ }
+ Expect(17);
}
}
}
@@ -1483,7 +1498,7 @@ List<Expression/*!*/>/*!*/ decreases) { void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(13)) {
+ if (StartOf(14)) {
if (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
@@ -1531,12 +1546,12 @@ List<Expression/*!*/>/*!*/ decreases) { Term(out e0);
e = e0;
- if (StartOf(14)) {
+ if (StartOf(15)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
e = new BinaryExpr(x, op, e0, e1);
- while (StartOf(14)) {
+ while (StartOf(15)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1788,7 +1803,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new ITEExpr(x, e, e0, e1);
} else if (la.kind == 60) {
MatchExpression(out e);
- } else if (StartOf(15)) {
+ } else if (StartOf(16)) {
QuantifierGuts(out e);
} else if (la.kind == 38) {
ComprehensionExpr(out e);
@@ -2163,7 +2178,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(16)) {
+ if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2179,13 +2194,13 @@ List<Expression/*!*/>/*!*/ decreases) { public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
@@ -2198,8 +2213,9 @@ List<Expression/*!*/>/*!*/ decreases) { {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
@@ -2212,18 +2228,20 @@ List<Expression/*!*/>/*!*/ decreases) { public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
- public virtual void SynErr(string filename, int line, int col, string msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+
+ public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
- string GetSyntaxErrorString(int n) {
+ }
+
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2375,7 +2393,7 @@ public class Errors { default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2383,8 +2401,9 @@ public class Errors { Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
+
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index a8970f05..9970d61a 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -507,6 +507,10 @@ namespace Microsoft.Dafny { PrintSpec("invariant", s.Invariants, indent + IndentAmount);
PrintSpecLine("decreases", s.Decreases, indent + IndentAmount);
+ if (s.Mod != null)
+ {
+ PrintFrameSpecLine("modifies", s.Mod, indent + IndentAmount);
+ }
Indent(indent);
PrintStatement(s.Body, indent);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 17309836..c0bf4392 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1512,6 +1512,11 @@ namespace Microsoft.Dafny { }
// any type is fine
}
+ if(s.Mod != null) {
+ foreach (FrameExpression fe in s.Mod) {
+ ResolveFrameExpression(fe, "modifies");
+ }
+ }
s.IsGhost = bodyMustBeSpecOnly;
loopStack.Add(s); // push
if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 19157a32..81f556c8 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
-[ContractInvariantMethod]
-void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);}
- [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+ [ContractInvariantMethod]
+ void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);
+ }
+
+// [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){ }
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){ Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){ }
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -213,19 +215,20 @@ public class Scanner { const int noSym = 104;
-[ContractInvariantMethod]
-void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
-}
+ [ContractInvariantMethod]
+ void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+ }
+
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){ Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -290,9 +293,9 @@ void objectInvariant(){ start[Buffer.EOF] = -1;
}
-
- [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+// [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -302,15 +305,14 @@ void objectInvariant(){ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
-
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
- [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+// [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -319,10 +321,9 @@ void objectInvariant(){ buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
-
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -343,11 +344,11 @@ void objectInvariant(){ Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -358,7 +359,7 @@ void objectInvariant(){ }
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -366,9 +367,9 @@ void objectInvariant(){ // // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -418,7 +419,7 @@ void objectInvariant(){ return;
}
-
+
}
}
@@ -555,10 +556,13 @@ void objectInvariant(){ t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+ if (start.ContainsKey(ch)) {
+ Contract.Assert(start[ch] != null);
+ state = (int) start[ch];
+ }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -764,14 +768,14 @@ void objectInvariant(){ t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -792,7 +796,7 @@ void objectInvariant(){ }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 07e328a0..b2c46c8a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1003,7 +1003,7 @@ namespace Microsoft.Dafny { // play havoc with the heap according to the modifies clause
builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
// assume the usual two-state boilerplate information
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod, etran.Old, etran)) {
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod.Mod, etran.Old, etran, etran.Old)) {
if (tri.IsFree) {
builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));
}
@@ -1049,7 +1049,7 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null);
// set up the information used to verify the method's modifies clause
- DefineFrame(m.tok, m.Mod, builder, localVariables);
+ DefineFrame(m.tok, m.Mod, builder, localVariables, null);
}
Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
@@ -1065,7 +1065,7 @@ namespace Microsoft.Dafny { return CaptureState(tok, null);
}
- void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables){
+ void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(frameClause));
Contract.Requires(builder != null);
@@ -1074,9 +1074,9 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
// Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
- Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the name and type of the $_Frame variable
+ Bpl.IdentifierExpr theFrame = etran.TheFrame(tok); // this is a throw-away expression, used only to extract the type of the $_Frame variable
Contract.Assert(theFrame.Type != null); // follows from the postcondition of TheFrame
- Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, theFrame.Name, theFrame.Type));
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? theFrame.Name, theFrame.Type));
localVariables.Add(frame);
// $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
@@ -1099,14 +1099,14 @@ namespace Microsoft.Dafny { {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(calleeFrame));
- Contract.Requires(receiverReplacement != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires((receiverReplacement == null) == (substMap == null));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Requires(etran != null);
Contract.Requires(builder != null);
Contract.Requires(errorMessage != null);
Contract.Requires(predef != null);
- // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in calleeFrame ==> $_Frame[o,f]);
+ // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]);
Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
@@ -1230,7 +1230,7 @@ namespace Microsoft.Dafny { Contract.Requires(f != null);
Contract.Requires(etran != null);
Contract.Requires(cce.NonNullElements(rw));
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Requires(predef != null);
Contract.Requires((receiverReplacement == null) == (substMap == null));
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
@@ -1241,8 +1241,8 @@ namespace Microsoft.Dafny { Bpl.Expr disjunction = null;
foreach (FrameExpression rwComponent in rw) {
Expression e = rwComponent.E;
- if (substMap != null) {
- Contract.Assert(receiverReplacement != null);
+ if (receiverReplacement != null) {
+ Contract.Assert(substMap != null);
e = Substitute(e, receiverReplacement, substMap);
}
Bpl.Expr disjunct;
@@ -1355,7 +1355,7 @@ namespace Microsoft.Dafny { }
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
- DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals);
+ DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals, null);
CheckWellformedWithResult(f.Body, new WFOptions(f, null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
// check that postconditions hold
@@ -2539,7 +2539,7 @@ namespace Microsoft.Dafny { }
comment = null;
}
- if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {
+ if (!skipEnsures) foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod, etran.Old, etran, etran.Old)) {
ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
}
}
@@ -2766,15 +2766,15 @@ namespace Microsoft.Dafny { /// <summary>
/// There are 3 states of interest when generating two-state boilerplate:
- /// S0. the beginning of the method, which is where the modifies clause is interpreted
+ /// S0. the beginning of the method or loop, which is where the modifies clause is interpreted
/// S1. the pre-state of the two-state interval
/// S2. the post-state of the two-state interval
- /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
+ /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.
/// </summary>
- List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, Method/*!*/ method, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)
+ List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
{
Contract.Requires(tok != null);
- Contract.Requires(method != null);
+ Contract.Requires(modifiesClause != null);
Contract.Requires(etranPre != null);
Contract.Requires(etran != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));
@@ -2782,7 +2782,7 @@ namespace Microsoft.Dafny { List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();
// the frame condition, which is free since it is checked with every heap update and call
- boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, method.Mod, etranPre, etran), null, "frame condition"));
+ boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));
// HeapSucc(S1, S2)
Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);
@@ -2792,13 +2792,13 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// There are 3 states of interest when generating a freame condition:
- /// S0. the beginning of the method, which is where the modifies clause is interpreted
+ /// There are 3 states of interest when generating a frame condition:
+ /// S0. the beginning of the method/loop, which is where the modifies clause is interpreted
/// S1. the pre-state of the two-state interval
/// S2. the post-state of the two-state interval
- /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
+ /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.
/// </summary>
- Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran)
+ Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
{
Contract.Requires(tok != null);
Contract.Requires(etran != null);
@@ -2820,15 +2820,43 @@ namespace Microsoft.Dafny { Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);
Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
- Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.Old.IsAlloced(tok, o));
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));
Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
- consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etran.Old, null, null));
+ consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
}
-
+ Bpl.Expr/*!*/ FrameConditionUsingDefinedFrame(IToken/*!*/ tok, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(etran != null);
+ Contract.Requires(etranPre != null);
+ Contract.Requires(predef != null);
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ // generate:
+ // (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] }
+ // o != null && old($Heap)[o,alloc] ==>
+ // $Heap[o,f] == PreHeap[o,f] ||
+ // $_Frame[o,f])
+ Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
+ Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
+ Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
+
+ Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);
+ Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranPre.IsAlloced(tok, o));
+ Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
+
+ consequent = Bpl.Expr.Or(consequent, Bpl.Expr.SelectTok(tok, etranMod.TheFrame(tok), o, f));
+
+ Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
+ return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
+ }
// ----- Type ---------------------------------------------------------------------------------
Bpl.Type TrType(Type type)
@@ -3120,7 +3148,7 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "while statement");
var s = (WhileStmt)stmt;
TrLoop(s, s.Guard,
- delegate(Bpl.StmtListBuilder bld) { TrStmt(s.Body, bld, locals, etran); },
+ delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrStmt(s.Body, bld, locals, e); },
builder, locals, etran);
} else if (stmt is AlternativeLoopStmt) {
@@ -3129,7 +3157,7 @@ namespace Microsoft.Dafny { var tru = new LiteralExpr(s.Tok, true);
tru.Type = Type.Bool; // resolve here
TrLoop(s, tru,
- delegate(Bpl.StmtListBuilder bld) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, etran); },
+ delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, e); },
builder, locals, etran);
} else if (stmt is ForeachStmt) {
@@ -3322,7 +3350,7 @@ namespace Microsoft.Dafny { }
}
- delegate void BodyTranslator(Bpl.StmtListBuilder builder);
+ delegate void BodyTranslator(Bpl.StmtListBuilder builder, ExpressionTranslator etran);
void TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr,
Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
@@ -3343,6 +3371,17 @@ namespace Microsoft.Dafny { locals.Add(preLoopHeapVar);
Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar);
ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
+ ExpressionTranslator updatedFrameEtran;
+ string loopFrameName = "#_Frame#" + loopId;
+ if(s.Mod != null)
+ updatedFrameEtran = new ExpressionTranslator(etran, loopFrameName);
+ else
+ updatedFrameEtran = etran;
+
+ if (s.Mod != null) { // check that the modifies is a strict subset
+ CheckFrameSubset(s.Tok, s.Mod, null, null, etran, builder, "loop modifies clause may violate context's modifies clause", null);
+ DefineFrame(s.Tok, s.Mod, builder, locals, loopFrameName);
+ }
builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));
List<Bpl.Expr> initDecr = null;
@@ -3390,14 +3429,19 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);
}
// include boilerplate invariants
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod, etranPreLoop, etran)) {
- if (tri.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
- } else {
- Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
- invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
- }
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod.Mod, etranPreLoop, etran, etran.Old))
+ {
+ if (tri.IsFree) {
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
+ }
+ else {
+ Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
+ invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
+ }
}
+ // add a free invariant which says that the heap hasn't changed outside of the modifies clause.
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
+
// include a free invariant that says that all completed iterations so far have only decreased the termination metric
if (initDecr != null) {
List<IToken> toks = new List<IToken>();
@@ -3430,11 +3474,11 @@ namespace Microsoft.Dafny { // termination checking
if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {
// omit termination checking for this loop
- bodyTr(loopBodyBuilder);
+ bodyTr(loopBodyBuilder, updatedFrameEtran);
} else {
List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");
// time for the actual loop body
- bodyTr(loopBodyBuilder);
+ bodyTr(loopBodyBuilder, updatedFrameEtran);
// check definedness of decreases expressions
List<IToken> toks = new List<IToken>();
List<Type> types = new List<Type>();
@@ -3585,8 +3629,8 @@ namespace Microsoft.Dafny { ins.Add(param);
}
- // Check modifies clause
- CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);
+ // Check modifies clause of a subcall is a subset of the current frame.
+ CheckFrameSubset(tok, method.Mod, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
// Check termination
ModuleDecl module = cce.NonNull(method.EnclosingClass).Module;
@@ -4133,7 +4177,7 @@ namespace Microsoft.Dafny { "$obj" + i, predef.RefType, builder, locals);
prevObj[i] = obj;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj]);
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4164,7 +4208,7 @@ namespace Microsoft.Dafny { prevObj[i] = obj;
prevIndex[i] = fieldName;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj,index]);
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4195,7 +4239,7 @@ namespace Microsoft.Dafny { "$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);
prevObj[i] = obj;
prevIndex[i] = fieldName;
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing context's modifies clause"));
// check that this LHS is not the same as any previous LHSs
for (int j = 0; j < i; j++) {
@@ -4376,6 +4420,7 @@ namespace Microsoft.Dafny { public readonly PredefinedDecls predef;
public readonly Translator translator;
public readonly string This;
+ public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.
readonly Function applyLimited_CurrentFunction;
readonly int layerOffset = 0;
public int Statistics_FunctionCount = 0;
@@ -4420,18 +4465,34 @@ namespace Microsoft.Dafny { this.HeapExpr = heap;
this.This = thisVar;
}
-
- ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset) {
- Contract.Requires(translator != null);
- Contract.Requires(predef != null);
- Contract.Requires(heap != null);
- Contract.Requires(applyLimited_CurrentFunction != null);
- this.translator = translator;
- this.predef = predef;
- this.HeapExpr = heap;
- this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
- this.This = "this";
- this.layerOffset = layerOffset;
+
+ ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset)
+ {
+ Contract.Requires(translator != null);
+ Contract.Requires(predef != null);
+ Contract.Requires(heap != null);
+ Contract.Requires(applyLimited_CurrentFunction != null);
+ this.translator = translator;
+ this.predef = predef;
+ this.HeapExpr = heap;
+ this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
+ this.This = "this";
+ this.layerOffset = layerOffset;
+ }
+
+ public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)
+ {
+ Contract.Requires(etran != null);
+ Contract.Requires(modifiesFrame != null);
+ this.translator = etran.translator;
+ this.HeapExpr = etran.HeapExpr;
+ this.predef = etran.predef;
+ this.This = etran.This;
+ this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction;
+ this.layerOffset = etran.layerOffset;
+ this.Statistics_FunctionCount = etran.Statistics_FunctionCount;
+ this.oldEtran = etran.oldEtran;
+ this.modifiesFrame = modifiesFrame;
}
ExpressionTranslator oldEtran;
@@ -4476,7 +4537,7 @@ namespace Microsoft.Dafny { Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");
Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);
Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);
- return new Bpl.IdentifierExpr(tok, "$_Frame", ty);
+ return new Bpl.IdentifierExpr(tok, this.modifiesFrame ?? "$_Frame", ty);
}
public Bpl.IdentifierExpr Tick() {
@@ -5941,11 +6002,12 @@ namespace Microsoft.Dafny { static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(expr != null);
+ Contract.Requires(receiverReplacement != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != null);
Expression newExpr = null; // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
-
+
if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {
// nothing to substitute
} else if (expr is ThisExpr) {
@@ -6103,8 +6165,10 @@ namespace Microsoft.Dafny { static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
Contract.Requires(cce.NonNullElements(elist));
- Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
+ Contract.Requires((receiverReplacement == null) == (substMap == null));
+ Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));
+
List<Expression> newElist = null; // initialized lazily
for (int i = 0; i < elist.Count; i++)
{cce.LoopInvariant( newElist == null || newElist.Count == i);
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 9ad1ce22..99df97cd 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -184,10 +184,11 @@ namespace Graphing { int n = this.graph.Nodes.Count;
this.postOrderNumberToNode = new Maybe<Node>[n + 1];
this.nodeToPostOrderNumber = new Dictionary<Node, int>();
- HashSet<Node> visited = new HashSet<Node>();
- int currentNumber = 1;
+ //HashSet<Node> visited = new HashSet<Node>();
+ //int currentNumber = 1;
Contract.Assume(this.source != null);
- this.PostOrderVisit(this.source, visited, ref currentNumber);
+ //this.PostOrderVisit(this.source, visited, ref currentNumber);
+ this.PostOrderVisitIterative(this.source);
this.sourceNum = this.nodeToPostOrderNumber[source];
// for (int i = 1; i <= n; i++){ Console.WriteLine(postOrderNumberToNode[i]); }
this.doms = new int[n + 1]; // 0 is unused: means undefined
@@ -278,6 +279,50 @@ namespace Graphing { currentNumber++;
return;
}
+ // Iterative version: mimics the above recursive procedure
+ private void PostOrderVisitIterative(Node n)
+ {
+ Contract.Requires(n != null);
+ var visited = new HashSet<Node>();
+ var grey = new HashSet<Node>();
+ var stack = new Stack<Node>();
+
+ int currentNumber = 1;
+
+ stack.Push(n);
+ visited.Add(n);
+
+ while (stack.Count != 0)
+ {
+ var curr = stack.Pop();
+
+ if (grey.Contains(curr))
+ {
+ Contract.Assume(this.postOrderNumberToNode != null);
+ Contract.Assume(this.nodeToPostOrderNumber != null);
+ this.postOrderNumberToNode[currentNumber].Val = curr;
+ this.nodeToPostOrderNumber[curr] = currentNumber;
+ currentNumber++;
+ }
+ else
+ {
+ grey.Add(curr);
+ stack.Push(curr);
+ foreach (Node/*!*/ child in this.graph.Successors(curr))
+ {
+ Contract.Assert(child != null);
+ if (!visited.Contains(child))
+ {
+ visited.Add(child);
+ stack.Push(child);
+ }
+ }
+ }
+
+ }
+
+
+ }
}
public class Graph<Node> {
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 98a67409..50a8f45c 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -254,6 +254,24 @@ namespace Microsoft.Boogie }
/// <summary>
+ /// Look for function application with a subsequence of given arguments and return its value or null if no such application exists.
+ /// </summary>
+ public Element TryPartialEval(params Element[] args)
+ {
+ foreach (var tpl in apps) {
+ int j = 0;
+ for (int i = 0; i < args.Length; ++i) {
+ if (tpl.Args[j] == args[i]) {
+ j++;
+ if (j == tpl.Args.Length)
+ return tpl.Result;
+ }
+ }
+ }
+ return null;
+ }
+
+ /// <summary>
/// Short for TryEval(args) == (Element)true
/// </summary>
public bool IsTrue(params Element[] args)
@@ -515,6 +533,11 @@ namespace Microsoft.Boogie return res;
}
+ public Func TryGetSkolemFunc(string name)
+ {
+ return Functions.Where(f => f.Name.StartsWith(name + "!")).FirstOrDefault();
+ }
+
public Element GetElement(string name)
{
Element res;
@@ -524,6 +547,11 @@ namespace Microsoft.Boogie throw new KeyNotFoundException("element '" + name + "' undefined in the model");
}
+ public Element MkIntElement(int v)
+ {
+ return MkElement(v.ToString());
+ }
+
public void Write(System.IO.TextWriter wr)
{
wr.WriteLine("*** MODEL");
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 68c02c5d..95d8950a 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -511,7 +511,13 @@ namespace Microsoft.Boogie.Simplify { thmProver = null;
currentProverHasBeenABadBoy = false;
restarts++;
+
+ if (CommandLineOptions.Clo.StratifiedInlining > 0)
+ {
+ Console.WriteLine("Warning: restarting theorem prover. Context could be lost");
+ }
}
+
FireUpNewProver();
}
cce.EndExpose();
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index 3a9c74ae..f0aa3906 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -11,330 +11,451 @@ using Microsoft.Z3; using Microsoft.Boogie.VCExprAST;
using Microsoft.Basetypes;
-namespace Microsoft.Boogie.Z3
-{
- public class Z3Config
- {
- private Config config = new Config();
- private int counterexamples;
- private string logFilename;
- private List<string> debugTraces = new List<string>();
-
- public void SetModelCompletion(bool enabled)
- {
- config.SetParamValue("MODEL_VALUE_COMPLETION", (enabled ? "true" : "false"));
- }
+using Z3Model = Microsoft.Z3.Model;
+using BoogieModel = Microsoft.Boogie.Model;
+
+namespace Microsoft.Boogie.Z3 {
+ public class Z3apiProverContext : DeclFreeProverContext {
+ private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();
+ internal BacktrackDictionary<string, Term> constants = new BacktrackDictionary<string, Term>();
+ internal BacktrackDictionary<string, FuncDecl> functions = new BacktrackDictionary<string, FuncDecl>();
+ internal BacktrackDictionary<string, Term> labels = new BacktrackDictionary<string, Term>();
+
+ public Config config;
+ public Context z3;
+
+ private Z3TypeCachedBuilder tm;
+ private UniqueNamer namer;
+ private StreamWriter z3log;
+
+ private int counterexamples;
+ private string logFilename;
+ private List<string> debugTraces;
+
+ public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)
+ : base(gen, new VCGenerationOptions(new List<string>())) {
+ int timeout = opts.Timeout * 1000;
+ config = new Config();
+ config.SetParamValue("MODEL", "true");
+ config.SetParamValue("MODEL_V2", "true");
+ config.SetParamValue("MODEL_COMPLETION", "true");
+ config.SetParamValue("MBQI", "false");
+ config.SetParamValue("TYPE_CHECK", "true");
+ if (0 <= timeout) {
+ config.SetParamValue("SOFT_TIMEOUT", timeout.ToString());
+ }
+
+ if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
+ this.counterexamples = CommandLineOptions.Clo.ProverCCLimit;
+ }
+ if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
+ logFilename = CommandLineOptions.Clo.SimplifyLogFilePath;
+ }
+ this.debugTraces = new List<string>();
+
+ z3 = new Context(config);
+ z3.SetPrintMode(PrintMode.Smtlib2Compliant);
+ if (logFilename != null)
+ z3.OpenLog(logFilename);
+ foreach (string tag in debugTraces)
+ z3.EnableDebugTrace(tag);
+
+ this.z3log = null;
+ this.tm = new Z3TypeCachedBuilder(this);
+ this.namer = new UniqueNamer();
+ }
- public void SetModel(bool enabled)
- {
- config.SetParamValue("MODEL", (enabled ? "true" : "false"));
- }
+ public override void DeclareType(TypeCtorDecl t, string attributes) {
+ base.DeclareType(t, attributes);
+ log("(declare-sort {0})", t.Name);
+ }
- public void SetSoftTimeout(string timeout)
- {
- config.SetParamValue("SOFT_TIMEOUT", timeout);
- }
+ public override void DeclareConstant(Constant c, bool uniq, string attributes) {
+ base.DeclareConstant(c, uniq, attributes);
+ DeclareConstant(c.Name, c.TypedIdent.Type);
+ }
- public void SetTypeCheck(bool enabled)
- {
- config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false"));
- }
+ public override void DeclareFunction(Function f, string attributes) {
+ base.DeclareFunction(f, attributes);
+ List<Type> domain = new List<Type>();
+ foreach (Variable v in f.InParams) {
+ domain.Add(v.TypedIdent.Type);
+ }
+ if (f.OutParams.Length != 1)
+ throw new Exception("Cannot handle functions with " + f.OutParams + " out parameters.");
+ Type range = f.OutParams[0].TypedIdent.Type;
+
+ string functionName = f.Name;
+ Symbol symbolAst = GetSymbol(functionName);
+ var domainStr = "";
+ List<Sort> domainAst = new List<Sort>();
+ foreach (Type domainType in domain) {
+ Sort type = tm.GetType(domainType);
+ domainAst.Add(type);
+ domainStr += type.ToString() + " ";
+ }
+ Sort rangeAst = tm.GetType(range);
+ FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst);
+ functions.Add(functionName, constDeclAst);
+ log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);
+ }
- public void SetCounterExample(int counterexample)
- {
- this.counterexamples = counterexample;
- }
+ public override void DeclareGlobalVariable(GlobalVariable v, string attributes) {
+ base.DeclareGlobalVariable(v, attributes);
+ DeclareConstant(v.Name, v.TypedIdent.Type);
+ }
- public void SetLogFilename(string filename)
- {
- this.logFilename = filename;
- }
+ public override string Lookup(VCExprVar var) {
+ return namer.Lookup(var);
+ }
- public Config Config
- {
- get { return this.config; }
- }
- public int Counterexamples
- {
- get { return this.counterexamples; }
- }
- public string LogFilename
- {
- get { return this.logFilename; }
- }
+ public void log(string format, params object[] args) {
+ // Currently, this is a no-op because z3log is always null
+ // We use the default (automatic) tracing facility of z3
+ if (z3log != null) {
+ var str = string.Format(format, args);
+ // Do standard string replacement
+ str = str.Replace("array", "Array");
+ z3log.WriteLine(str);
+ z3log.Flush();
+ }
+ }
- public void EnableDebugTrace(string debugTrace)
- {
- this.debugTraces.Add(debugTrace);
- }
+ public void CloseLog() {
+ z3.CloseLog();
+ if (z3log != null) {
+ z3log.Close();
+ }
+ z3log = null;
+ }
- public List<string> DebugTraces
- {
- get { return this.debugTraces; }
- }
+ public void CreateBacktrackPoint() {
+ symbols.CreateBacktrackPoint();
+ constants.CreateBacktrackPoint();
+ functions.CreateBacktrackPoint();
+ labels.CreateBacktrackPoint();
+ z3.Push();
+ log("(push)");
}
- public abstract class Z3TermAst { }
- public abstract class Z3PatternAst { }
- public abstract class Z3ConstDeclAst { }
- public abstract class Z3LabeledLiterals { }
-
- public interface Z3Context
- {
- void CreateBacktrackPoint();
- void Backtrack();
- void AddAxiom(VCExpr axiom, LineariserOptions linOptions);
- void AddConjecture(VCExpr vc, LineariserOptions linOptions);
- void AddSmtlibString(string smtlibString);
- string GetDeclName(Z3ConstDeclAst constDeclAst);
- Z3PatternAst MakePattern(List<Z3TermAst> exprs);
- Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);
- ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors);
- void TypeCheckBool(Z3TermAst t);
- void TypeCheckInt(Z3TermAst t);
- void DeclareType(string typeName);
- void DeclareConstant(string constantName, Type boogieType);
- void DeclareFunction(string functionName, List<Type> domain, Type range);
- Z3TermAst GetConstant(string constantName, Type constantType);
- Z3TermAst MakeIntLiteral(string numeral);
- Z3TermAst MakeTrue();
- Z3TermAst MakeFalse();
- Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child);
- Z3LabeledLiterals GetRelevantLabels();
- Z3TermAst Make(string op, List<Z3TermAst> children);
- Z3TermAst MakeArraySelect(List<Z3TermAst> args);
- Z3TermAst MakeArrayStore(List<Z3TermAst> args);
- }
-
- internal class PartitionMap
- {
- private Context ctx;
- private Dictionary<Term, int> termToPartition = new Dictionary<Term, int>();
- private Dictionary<object, int> valueToPartition = new Dictionary<object, int>();
- private List<Object> partitionToValue = new List<Object>();
- private int partitionCounter = 0;
- public int PartitionCounter { get { return partitionCounter; } }
-
- public PartitionMap(Context ctx)
- {
- this.ctx = ctx;
- }
+ public void Backtrack() {
+ z3.Pop();
+ labels.Backtrack();
+ functions.Backtrack();
+ constants.Backtrack();
+ symbols.Backtrack();
+ log("(pop)");
+ }
- public int GetPartition(Term value)
- {
- int result;
- if (!termToPartition.TryGetValue(value, out result))
- {
- result = partitionCounter++;
- termToPartition.Add(value, result);
- partitionToValue.Add(null);
- object constant = Evaluate(value);
- valueToPartition.Add(constant, result);
- partitionToValue[result] = constant;
- }
- return result;
- }
+ public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) {
+ Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+ Term term = (Term)axiom.Accept(visitor, linOptions);
+ log("(assert {0})", term);
+ z3.AssertCnstr(term);
+ }
- private object Evaluate(Term v)
- {
- Sort s = v.GetSort();
- Sort boolSort = ctx.MkBoolSort();
- Sort intSort = ctx.MkIntSort();
- ArrayValue av;
-
- if (s.Equals(boolSort))
- {
- return ctx.GetBoolValue(v);
- }
- else if (s.Equals(intSort))
- {
- int i;
- if (ctx.TryGetNumeralInt(v, out i))
- {
- return BigNum.FromInt(i);
- }
- else
- {
- return BigNum.FromString(ctx.GetNumeralString(v));
- }
- }
- else if (ctx.TryGetArrayValue(v, out av))
- {
- List<List<int>> arrayValue = new List<List<int>>();
- List<int> tuple;
- for (int i = 0; i < av.Domain.Length; i++)
- {
- tuple = new List<int>();
- tuple.Add(GetPartition(av.Domain[i]));
- tuple.Add(GetPartition(av.Range[i]));
- arrayValue.Add(tuple);
- }
- tuple = new List<int>();
- tuple.Add(GetPartition(av.ElseCase));
- arrayValue.Add(tuple);
- return arrayValue;
- }
- else
- {
- // The term is uninterpreted; just return the partition id.
- return GetPartition(v);
- }
- }
+ public void AddConjecture(VCExpr vc, LineariserOptions linOptions) {
+ VCExpr not_vc = (VCExpr)this.gen.Not(vc);
+ Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+ Term term = (Term)not_vc.Accept(visitor, linOptions);
+ log("(assert {0})", term);
+ z3.AssertCnstr(term);
+ }
- public List<Object> PartitionToValue(Context ctx)
- {
- return partitionToValue;
- }
+ public void AddSmtlibString(string smtlibString) {
+ FuncDecl[] decls;
+ Term[] assumptions;
+ Term[] terms;
+ Sort[] sorts;
+ string tmp;
+
+ z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { },
+ out assumptions, out terms, out decls, out sorts, out tmp);
+ // TBD: check with Nikolaj about the correct position of assumptions
+ foreach (FuncDecl decl in decls) {
+ Symbol symbol = z3.GetDeclName(decl);
+ string functionName = z3.GetSymbolString(symbol);
+ functions.Add(functionName, decl);
+ }
+ foreach (Term assumption in assumptions) {
+ log("(assert {0})", assumption);
+ z3.AssertCnstr(assumption);
+ }
+ }
- public Dictionary<object, int> ValueToPartition(Context ctx)
- {
- return valueToPartition;
- }
+ private List<Sort> GetTypes(List<Type> boogieTypes) {
+ List<Sort> z3Types = new List<Sort>();
+ foreach (Type boogieType in boogieTypes) {
+ Sort type = tm.GetType(boogieType);
+ z3Types.Add(type);
+ }
+ return z3Types;
}
- internal class BacktrackDictionary<K, V>
- {
- private Dictionary<K, V> dictionary = new Dictionary<K, V>();
- private Stack<List<K>> keyStack = new Stack<List<K>>();
+ private static bool Equals(List<string> l, List<string> r) {
+ Debug.Assert(l != null);
+ if (r == null)
+ return false;
- public BacktrackDictionary()
- {
- CreateBacktrackPoint();
- }
+ if (l.Count != r.Count)
+ return false;
- public bool TryGetValue(K key, out V val)
- {
- return dictionary.TryGetValue(key, out val);
- }
+ for (int i = 0; i < l.Count; i++)
+ if (!l[i].Equals(r[i]))
+ return false;
+ return true;
+ }
+
+ private void DisplayRelevantLabels(List<string> relevantLabels) {
+ foreach (string labelName in relevantLabels) {
+ System.Console.Write(labelName + ",");
+ }
+ System.Console.WriteLine("---");
+ }
+
+ private void DeclareConstant(string constantName, Type boogieType) {
+ Symbol symbolAst = GetSymbol(constantName);
+ Sort typeAst = tm.GetType(boogieType);
+
+ Term constAst = z3.MkConst(symbolAst, typeAst);
+ constants.Add(constantName, constAst);
+ log("(declare-funs (({0} {1})))", constAst, typeAst);
+ }
- public void Add(K key, V v)
- {
- if (dictionary.ContainsKey(key))
- {
- dictionary.Remove(key);
- }
- dictionary.Add(key, v);
- keyStack.Peek().Add(key);
+ public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {
+ Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
+ boogieErrors = new List<Z3ErrorModelAndLabels>();
+ LBool outcome = LBool.Undef;
+ Debug.Assert(0 < this.counterexamples);
+ while (true) {
+ Z3Model z3Model;
+ outcome = z3.CheckAndGetModel(out z3Model);
+
+ log("(check-sat)");
+ if (outcome == LBool.False)
+ break;
+
+ if (outcome == LBool.Undef && z3Model == null) {
+ // Blame this on timeout
+ return ProverInterface.Outcome.TimeOut;
}
- public bool ContainsKey(K k)
- {
- return dictionary.ContainsKey(k);
+ Debug.Assert(z3Model != null);
+ LabeledLiterals labels = z3.GetRelevantLabels();
+ Debug.Assert(labels != null);
+
+ List<string> labelStrings = new List<string>();
+ uint numLabels = labels.GetNumLabels();
+ for (uint i = 0; i < numLabels; ++i) {
+ Symbol sym = labels.GetLabel(i);
+ string labelName = z3.GetSymbolString(sym);
+ if (!labelName.StartsWith("@")) {
+ labels.Disable(i);
+ }
+ labelStrings.Add(labelName);
}
- public void CreateBacktrackPoint()
- {
- keyStack.Push(new List<K>());
+ var sw = new StringWriter();
+ sw.WriteLine("*** MODEL");
+ z3Model.Display(sw);
+ sw.WriteLine("*** END_MODEL");
+ var sr = new StringReader(sw.ToString());
+ var models = Microsoft.Boogie.Model.ParseModels(sr);
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+ boogieErrors.Add(e);
+
+ if (boogieErrors.Count < this.counterexamples) {
+ z3.BlockLiterals(labels);
+ log("block-literals {0}", labels);
}
- public void Backtrack()
- {
- List<K> keysToErase = keyStack.Pop();
- foreach (K key in keysToErase)
- {
- dictionary.Remove(key);
- }
- if (keyStack.Count == 0)
- this.CreateBacktrackPoint();
+ labels.Dispose();
+ z3Model.Dispose();
+ if (boogieErrors.Count == this.counterexamples)
+ break;
+ }
+
+ if (boogieErrors.Count > 0) {
+ return ProverInterface.Outcome.Invalid;
+ }
+ else if (outcome == LBool.False) {
+ return ProverInterface.Outcome.Valid;
+ }
+ else {
+ Debug.Assert(outcome == LBool.Undef);
+ return ProverInterface.Outcome.Undetermined;
+ }
+ }
+
+ public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions,
+ out List<Z3ErrorModelAndLabels> boogieErrors,
+ out List<int> unsatCore) {
+ Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
+ boogieErrors = new List<Z3ErrorModelAndLabels>();
+ unsatCore = new List<int>();
+ LBool outcome = LBool.Undef;
+
+ Z3Model z3Model;
+ Term proof;
+ Term[] core;
+ Term[] assumption_terms = new Term[assumptions.Count];
+ var logstring = "";
+ for (int i = 0; i < assumptions.Count; i++) {
+ Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+ Term z3ast = (Term)assumptions[i].Accept(visitor, linOptions);
+ assumption_terms[i] = z3ast;
+ logstring += string.Format("({0}) ", assumption_terms[i]);
+ }
+
+ log("(get-core {0})", logstring);
+ outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);
+
+ if (outcome != LBool.False) {
+ Debug.Assert(z3Model != null);
+ LabeledLiterals labels = z3.GetRelevantLabels();
+ Debug.Assert(labels != null);
+
+ List<string> labelStrings = new List<string>();
+ uint numLabels = labels.GetNumLabels();
+ for (uint i = 0; i < numLabels; ++i) {
+ Symbol sym = labels.GetLabel(i);
+ string labelName = z3.GetSymbolString(sym);
+ if (!labelName.StartsWith("@")) {
+ labels.Disable(i);
+ }
+ labelStrings.Add(labelName);
}
- public IEnumerator GetEnumerator()
- {
- return dictionary.Keys.GetEnumerator();
+ var sw = new StringWriter();
+ sw.WriteLine("*** MODEL");
+ z3Model.Display(sw);
+ sw.WriteLine("*** END_MODEL");
+ var sr = new StringReader(sw.ToString());
+ var models = Microsoft.Boogie.Model.ParseModels(sr);
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+ boogieErrors.Add(e);
+
+ labels.Dispose();
+ z3Model.Dispose();
+ }
+
+ if (boogieErrors.Count > 0) {
+ return ProverInterface.Outcome.Invalid;
+ }
+ else if (outcome == LBool.False) {
+ foreach (Term t in core) {
+ for (int i = 0; i < assumption_terms.Length; i++) {
+ if (t.Equals(assumption_terms[i]))
+ unsatCore.Add(i);
+ }
}
+ return ProverInterface.Outcome.Valid;
+ }
+ else {
+ Debug.Assert(outcome == LBool.Undef);
+ return ProverInterface.Outcome.Undetermined;
+ }
}
- internal class BoogieErrorModelBuilder
- {
- private Z3Context container;
- private PartitionMap partitionMap;
+ private Symbol GetSymbol(string symbolName) {
+ if (!symbols.ContainsKey(symbolName)) {
+ Symbol symbolAst = z3.MkSymbol(symbolName);
+ symbols.Add(symbolName, symbolAst);
+ }
+ Symbol result;
+ if (!symbols.TryGetValue(symbolName, out result))
+ throw new Exception("symbol " + symbolName + " is undefined");
+ return result;
+ }
- public BoogieErrorModelBuilder(Z3Context container)
- {
- this.container = container;
- this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3);
- }
-
- private Dictionary<string, int> CreateConstantToPartition(Model z3Model)
- {
- Dictionary<string, int> constantToPartition = new Dictionary<string, int>();
- foreach (FuncDecl c in z3Model.GetModelConstants())
- {
- string name = container.GetDeclName(new Z3TypeSafeConstDecl(c));
- int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0]));
- constantToPartition.Add(name, pid);
- }
- return constantToPartition;
- }
+ public Term GetConstant(string constantName, Type constantType) {
+ Term typeSafeTerm;
+ if (!constants.ContainsKey(constantName))
+ this.DeclareConstant(constantName, constantType);
- private List<List<string>> CreatePartitionToConstant(Dictionary<string, int> constantToPartition)
- {
- List<List<string>> partitionToConstant = new List<List<string>>();
- for (int i = 0; i < partitionMap.PartitionCounter; i++)
- {
- partitionToConstant.Add(new List<string>());
- }
- foreach (string s in constantToPartition.Keys)
- {
- partitionToConstant[constantToPartition[s]].Add(s);
- }
- return partitionToConstant;
- }
+ if (!constants.TryGetValue(constantName, out typeSafeTerm))
+ throw new Exception("constant " + constantName + " is not defined");
+ return typeSafeTerm;
+ }
- private Dictionary<string, List<List<int>>> CreateFunctionToPartition(Model z3Model)
- {
- Dictionary<string, List<List<int>>> functionToPartition = new Dictionary<string, List<List<int>>>();
-
- foreach (KeyValuePair<FuncDecl, FunctionGraph> kv in z3Model.GetFunctionGraphs())
- {
- List<List<int>> f_tuples = new List<List<int>>();
- string f_name = container.GetDeclName(new Z3TypeSafeConstDecl(kv.Key));
- FunctionGraph graph = kv.Value;
- foreach (FunctionEntry entry in graph.Entries)
- {
- List<int> tuple = new List<int>();
- foreach (Term v in entry.Arguments)
- {
- tuple.Add(partitionMap.GetPartition(z3Model.Eval(v)));
- }
- tuple.Add(partitionMap.GetPartition(z3Model.Eval(entry.Result)));
- f_tuples.Add(tuple);
- }
- List<int> else_tuple = new List<int>();
- else_tuple.Add(partitionMap.GetPartition(z3Model.Eval(graph.Else)));
- f_tuples.Add(else_tuple);
- functionToPartition.Add(f_name, f_tuples);
- }
- return functionToPartition;
- }
+ public FuncDecl GetFunction(string functionName) {
+ FuncDecl f;
+ if (!functions.TryGetValue(functionName, out f))
+ throw new Exception("function " + functionName + " is undefined");
+ return f;
+ }
- public Z3ErrorModel BuildBoogieModel(Model z3Model)
- {
- Dictionary<string, int> constantToPartition = CreateConstantToPartition(z3Model);
- Dictionary<string, List<List<int>>> functionToPartition = CreateFunctionToPartition(z3Model);
- List<List<string>> partitionToConstant = CreatePartitionToConstant(constantToPartition);
- List<Object> partitionToValue = partitionMap.PartitionToValue(((Z3SafeContext)container).z3);
- Dictionary<object, int> valueToPartition = partitionMap.ValueToPartition(((Z3SafeContext)container).z3);
- return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition);
- }
+ public Term MakeLabel(string labelName, bool pos, Term child) {
+ Symbol labelSymbol = this.GetSymbol(labelName);
+ Term labeledExpr = z3.MkLabel(labelSymbol, pos, child);
+ labels.Add(labelName, labeledExpr);
+ return labeledExpr;
}
- public class Z3ErrorModelAndLabels
- {
- private Z3ErrorModel _errorModel;
- private List<string> _relevantLabels;
- public Z3ErrorModel ErrorModel
- {
- get { return this._errorModel; }
- }
- public List<string> RelevantLabels
- {
- get { return this._relevantLabels; }
- }
- public Z3ErrorModelAndLabels(Z3ErrorModel errorModel, List<string> relevantLabels)
- {
- this._errorModel = errorModel;
- this._relevantLabels = relevantLabels;
- }
+ public LabeledLiterals GetRelevantLabels() {
+ LabeledLiterals safeLiterals = z3.GetRelevantLabels();
+ log("get-relevant-labels");
+ return safeLiterals;
+ }
+ }
+
+ internal class BacktrackDictionary<K, V> {
+ private Dictionary<K, V> dictionary = new Dictionary<K, V>();
+ private Stack<List<K>> keyStack = new Stack<List<K>>();
+
+ public BacktrackDictionary() {
+ CreateBacktrackPoint();
+ }
+
+ public bool TryGetValue(K key, out V val) {
+ return dictionary.TryGetValue(key, out val);
}
+
+ public void Add(K key, V v) {
+ if (dictionary.ContainsKey(key)) {
+ dictionary.Remove(key);
+ }
+ dictionary.Add(key, v);
+ keyStack.Peek().Add(key);
+ }
+
+ public bool ContainsKey(K k) {
+ return dictionary.ContainsKey(k);
+ }
+
+ public void CreateBacktrackPoint() {
+ keyStack.Push(new List<K>());
+ }
+
+ public void Backtrack() {
+ List<K> keysToErase = keyStack.Pop();
+ foreach (K key in keysToErase) {
+ dictionary.Remove(key);
+ }
+ if (keyStack.Count == 0)
+ this.CreateBacktrackPoint();
+ }
+
+ public IEnumerator GetEnumerator() {
+ return dictionary.Keys.GetEnumerator();
+ }
+ }
+
+ public class Z3ErrorModelAndLabels {
+ private ErrorModel _errorModel;
+ private List<string> _relevantLabels;
+ public ErrorModel ErrorModel {
+ get { return this._errorModel; }
+ }
+ public List<string> RelevantLabels {
+ get { return this._relevantLabels; }
+ }
+ public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels) {
+ this._errorModel = errorModel;
+ this._relevantLabels = relevantLabels;
+ }
+ }
+
+
+
}
\ No newline at end of file diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 5f776bff..64793c9e 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -47,27 +47,23 @@ namespace Microsoft.Boogie.Z3 public override void Close()
{
base.Close();
- Z3SafeContext cm = context.cm;
- cm.CloseLog();
- cm.z3.Dispose();
- cm.config.Config.Dispose();
+ context.CloseLog();
+ context.z3.Dispose();
+ context.config.Dispose();
}
public void PushAxiom(VCExpr axiom)
{
- Z3SafeContext cm = context.cm;
- cm.CreateBacktrackPoint();
+ context.CreateBacktrackPoint();
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- cm.AddAxiom(axiom, linOptions);
-
+ context.AddAxiom(axiom, linOptions);
}
private void PushConjecture(VCExpr conjecture)
{
- Z3SafeContext cm = context.cm;
- cm.CreateBacktrackPoint();
+ context.CreateBacktrackPoint();
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- cm.AddConjecture(conjecture, linOptions);
+ context.AddConjecture(conjecture, linOptions);
}
public override void PushVCExpression(VCExpr vc)
@@ -78,61 +74,53 @@ namespace Microsoft.Boogie.Z3 public void CreateBacktrackPoint()
{
- Z3SafeContext cm = context.cm;
- cm.CreateBacktrackPoint();
+ context.CreateBacktrackPoint();
}
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- Z3SafeContext cm = context.cm;
Push();
- cm.AddAxiom(context.Axioms, linOptions);
- cm.AddConjecture(vc, linOptions);
- outcome = cm.Check(out z3LabelModels);
+ context.AddAxiom(context.Axioms, linOptions);
+ context.AddConjecture(vc, linOptions);
+ outcome = context.Check(out z3LabelModels);
Pop();
}
public override void Check()
{
- Z3SafeContext cm = context.cm;
- outcome = cm.Check(out z3LabelModels);
+ outcome = context.Check(out z3LabelModels);
}
public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
- Z3SafeContext cm = context.cm;
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
+ outcome = context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
}
public override void Push()
{
- Z3SafeContext cm = context.cm;
- cm.CreateBacktrackPoint();
+ context.CreateBacktrackPoint();
}
public override void Pop()
{
- Z3SafeContext cm = context.cm;
- cm.Backtrack();
+ context.Backtrack();
}
public override void Assert(VCExpr vc, bool polarity)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- Z3SafeContext cm = context.cm;
if (polarity)
- cm.AddAxiom(vc, linOptions);
+ context.AddAxiom(vc, linOptions);
else
- cm.AddConjecture(vc, linOptions);
+ context.AddConjecture(vc, linOptions);
}
public override void AssertAxioms()
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- Z3SafeContext cm = context.cm;
- cm.AddAxiom(context.Axioms, linOptions);
+ context.AddAxiom(context.Axioms, linOptions);
}
// Number of axioms pushed since the last call to FlushAxioms
@@ -188,80 +176,6 @@ namespace Microsoft.Boogie.Z3 return result;
}
}
-
- public class Z3apiProverContext : DeclFreeProverContext
- {
- public Z3SafeContext cm;
-
- public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)
- : base(gen, new VCGenerationOptions(new List<string>()))
- {
- Z3Config config = BuildConfig(opts.Timeout * 1000, true);
- this.cm = new Z3SafeContext(this, config, gen);
- }
- private static Z3Config BuildConfig(int timeout, bool nativeBv)
- {
- Z3Config config = new Z3Config();
- config.SetModelCompletion(false);
- config.SetModel(true);
-
- if (0 <= CommandLineOptions.Clo.ProverCCLimit)
- {
- config.SetCounterExample(CommandLineOptions.Clo.ProverCCLimit);
- }
-
- if (0 <= timeout)
- {
- config.SetSoftTimeout(timeout.ToString());
- }
-
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null)
- {
- config.SetLogFilename(CommandLineOptions.Clo.SimplifyLogFilePath);
- }
-
- config.SetTypeCheck(true);
- return config;
- }
-
- public override void DeclareType(TypeCtorDecl t, string attributes)
- {
- base.DeclareType(t, attributes);
- cm.DeclareType(t.Name);
- }
-
- public override void DeclareConstant(Constant c, bool uniq, string attributes)
- {
- base.DeclareConstant(c, uniq, attributes);
- cm.DeclareConstant(c.Name, c.TypedIdent.Type);
- }
-
- public override void DeclareFunction(Function f, string attributes)
- {
- base.DeclareFunction(f, attributes);
- List<Type> domain = new List<Type>();
- foreach (Variable v in f.InParams)
- {
- domain.Add(v.TypedIdent.Type);
- }
- if (f.OutParams.Length != 1)
- throw new Exception("Cannot handle functions with " + f.OutParams + " out parameters.");
- Type range = f.OutParams[0].TypedIdent.Type;
-
- cm.DeclareFunction(f.Name, domain, range);
- }
-
- public override void DeclareGlobalVariable(GlobalVariable v, string attributes)
- {
- base.DeclareGlobalVariable(v, attributes);
- cm.DeclareConstant(v.Name, v.TypedIdent.Type);
- }
-
- public override string Lookup(VCExprVar var)
- {
- return cm.Namer.Lookup(var);
- }
- }
}
namespace Microsoft.Boogie.Z3api
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index a7ed29eb..72192804 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -12,641 +12,5 @@ using Microsoft.Boogie.VCExprAST; namespace Microsoft.Boogie.Z3
{
- internal class Z3TypeSafeTerm : Z3TermAst
- {
- private Term termAst;
- public Z3TypeSafeTerm(Term termAst)
- {
- this.termAst = termAst;
- }
- public Term TermAst
- {
- get { return this.termAst; }
- }
- }
-
- internal class Z3TypeSafePattern : Z3PatternAst
- {
- private Pattern patternAst;
- public Z3TypeSafePattern(Pattern patternAst)
- {
- this.patternAst = patternAst;
- }
- public Pattern PatternAst
- {
- get { return this.patternAst; }
- }
- }
-
- internal class Z3TypeSafeConstDecl : Z3ConstDeclAst
- {
- private FuncDecl constDeclAst;
- public Z3TypeSafeConstDecl(FuncDecl constDeclAst)
- {
- this.constDeclAst = constDeclAst;
- }
- public FuncDecl ConstDeclAst
- {
- get { return this.constDeclAst; }
- }
- }
-
- public class Z3SafeType : Z3Type
- {
- private Sort typeAst;
- public Z3SafeType(Sort typeAst)
- {
- this.typeAst = typeAst;
- }
- public Sort TypeAst
- {
- get { return this.typeAst; }
- }
- }
-
- public class Z3SafeLabeledLiterals : Z3LabeledLiterals
- {
- private LabeledLiterals labeledLiterals;
- public Z3SafeLabeledLiterals(LabeledLiterals labeledLiterals)
- {
- this.labeledLiterals = labeledLiterals;
- }
- public LabeledLiterals LabeledLiterals
- {
- get { return this.labeledLiterals; }
- }
- }
-
- public class Z3SafeContext : Z3Context
- {
- private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();
- internal BacktrackDictionary<string, Z3TypeSafeTerm> constants = new BacktrackDictionary<string, Z3TypeSafeTerm>();
- internal BacktrackDictionary<string, Z3TypeSafeConstDecl> functions = new BacktrackDictionary<string, Z3TypeSafeConstDecl>();
- internal BacktrackDictionary<string, Z3TypeSafeTerm> labels = new BacktrackDictionary<string, Z3TypeSafeTerm>();
-
- public Context z3;
- public Z3Config config;
- public Z3apiProverContext ctxt;
- private VCExpressionGenerator gen;
- private Z3TypeCachedBuilder tm;
- private UniqueNamer namer;
- public UniqueNamer Namer
- {
- get { return namer; }
- }
- private StreamWriter z3log;
- public Z3SafeContext(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen)
- {
- Context z3 = new Context(config.Config);
- if (config.LogFilename != null)
- z3.OpenLog(config.LogFilename);
- foreach (string tag in config.DebugTraces)
- z3.EnableDebugTrace(tag);
- this.ctxt = ctxt;
- this.z3 = z3;
- this.config = config;
- this.tm = new Z3TypeCachedBuilder(this);
- this.gen = gen;
- this.namer = new UniqueNamer();
- this.z3.SetPrintMode(PrintMode.Smtlib2Compliant);
- this.z3log = null;
- }
-
- public void log(string format, params object[] args)
- {
- // Currently, this is a no-op because z3log is always null
- // We use the default (automatic) tracing facility of z3
- if (z3log != null)
- {
- var str = string.Format(format, args);
- // Do standard string replacement
- str = str.Replace("array", "Array");
- z3log.WriteLine(str);
- z3log.Flush();
- }
- }
-
- public void CloseLog()
- {
- z3.CloseLog();
- if (z3log != null)
- {
- z3log.Close();
- }
- z3log = null;
- }
-
- public void CreateBacktrackPoint()
- {
- symbols.CreateBacktrackPoint();
- constants.CreateBacktrackPoint();
- functions.CreateBacktrackPoint();
- labels.CreateBacktrackPoint();
- z3.Push();
- log("(push)");
- }
-
- public void Backtrack()
- {
- z3.Pop();
- labels.Backtrack();
- functions.Backtrack();
- constants.Backtrack();
- symbols.Backtrack();
- log("(pop)");
- }
-
- public void AddAxiom(VCExpr axiom, LineariserOptions linOptions)
- {
- Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
- Z3TermAst z3ast = (Z3TermAst)axiom.Accept(visitor, linOptions);
- Term term = Unwrap(z3ast);
- log("(assert {0})", term);
- z3.AssertCnstr(term);
- }
-
- public void AddConjecture(VCExpr vc, LineariserOptions linOptions)
- {
- VCExpr not_vc = (VCExpr)this.gen.Not(vc);
- Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
- Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions);
- Term term = Unwrap(z3ast);
- log("(assert {0})", term);
- z3.AssertCnstr(term);
- }
-
- public void AddSmtlibString(string smtlibString)
- {
- FuncDecl[] decls;
- Term[] assumptions;
- Term[] terms;
- Sort[] sorts;
- string tmp;
-
- z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { },
- out assumptions, out terms, out decls, out sorts, out tmp);
- // TBD: check with Nikolaj about the correct position of assumptions
- foreach (FuncDecl decl in decls)
- {
- Symbol symbol = z3.GetDeclName(decl);
- string functionName = z3.GetSymbolString(symbol);
- functions.Add(functionName, new Z3TypeSafeConstDecl(decl));
- }
- foreach (Term assumption in assumptions)
- {
- log("(assert {0})", assumption);
- z3.AssertCnstr(assumption);
- }
- }
-
- public string GetDeclName(Z3ConstDeclAst constDeclAst)
- {
- Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst;
- Symbol symbol = z3.GetDeclName(typeSafeConstDecl.ConstDeclAst);
- return z3.GetSymbolString(symbol);
- }
-
- private List<Term> Unwrap(List<Z3TermAst> terms)
- {
- List<Term> unwrap = new List<Term>();
- foreach (Z3TermAst term in terms)
- {
- Term unwrapTerm = Unwrap(term);
- unwrap.Add(unwrapTerm);
- }
- return unwrap;
- }
-
- private List<Pattern> Unwrap(List<Z3PatternAst> patterns)
- {
- List<Pattern> unwrap = new List<Pattern>();
- foreach (Z3PatternAst pattern in patterns)
- {
- Z3TypeSafePattern typeSafePattern = (Z3TypeSafePattern)pattern;
- unwrap.Add(typeSafePattern.PatternAst);
- }
- return unwrap;
- }
-
- private Sort Unwrap(Z3Type type)
- {
- Z3SafeType typeSafeTerm = (Z3SafeType)type;
- return typeSafeTerm.TypeAst;
- }
-
- private Term Unwrap(Z3TermAst term)
- {
- Z3TypeSafeTerm typeSafeTerm = (Z3TypeSafeTerm)term;
- return typeSafeTerm.TermAst;
- }
-
- private FuncDecl Unwrap(Z3ConstDeclAst constDeclAst)
- {
- Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst;
- return typeSafeConstDecl.ConstDeclAst;
- }
-
- private Z3TypeSafeTerm Wrap(Term term)
- {
- return new Z3TypeSafeTerm(term);
- }
-
- private Z3TypeSafeConstDecl Wrap(FuncDecl constDecl)
- {
- return new Z3TypeSafeConstDecl(constDecl);
- }
-
- private Z3TypeSafePattern Wrap(Pattern pattern)
- {
- return new Z3TypeSafePattern(pattern);
- }
-
- public Z3PatternAst MakePattern(List<Z3TermAst> exprs)
- {
- List<Term> unwrapExprs = Unwrap(exprs);
- Pattern pattern = z3.MkPattern(unwrapExprs.ToArray());
- Z3PatternAst wrapPattern = Wrap(pattern);
- return wrapPattern;
- }
-
- private List<Sort> GetTypes(List<Type> boogieTypes)
- {
- List<Sort> z3Types = new List<Sort>();
- foreach (Type boogieType in boogieTypes)
- {
- Z3Type type = tm.GetType(boogieType);
- Sort unwrapType = Unwrap(type);
- z3Types.Add(unwrapType);
- }
- return z3Types;
- }
-
- public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body)
- {
- List<Pattern> unwrapPatterns = Unwrap(patterns);
- List<Term> unwrapNoPatterns = Unwrap(no_patterns);
- Term unwrapBody = Unwrap(body);
-
- List<Term> bound = new List<Term>();
- for (int i = 0; i < varNames.Count; i++)
- {
- Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]);
- bound.Add(Unwrap(t));
- }
-
- Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid.ToString()), unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), bound.ToArray(), unwrapBody);
- return Wrap(termAst);
- }
- private static bool Equals(List<string> l, List<string> r)
- {
- Debug.Assert(l != null);
- if (r == null)
- return false;
-
- if (l.Count != r.Count)
- return false;
-
- for (int i = 0; i < l.Count; i++)
- if (!l[i].Equals(r[i]))
- return false;
- return true;
- }
-
- private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels)
- {
- BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this);
- Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model);
- return new Z3ErrorModelAndLabels(boogieModel, new List<string>(relevantLabels));
- }
-
- private void DisplayRelevantLabels(List<string> relevantLabels)
- {
- foreach (string labelName in relevantLabels)
- {
- System.Console.Write(labelName + ",");
- }
- System.Console.WriteLine("---");
- }
-
- public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors)
- {
- Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
- boogieErrors = new List<Z3ErrorModelAndLabels>();
- LBool outcome = LBool.Undef;
- Debug.Assert(0 < this.config.Counterexamples);
- while (true)
- {
- Model z3Model;
- outcome = z3.CheckAndGetModel(out z3Model);
- log("(check-sat)");
- if (outcome == LBool.False)
- break;
-
- if (outcome == LBool.Undef && z3Model == null)
- {
- // Blame this on timeout
- return ProverInterface.Outcome.TimeOut;
- }
-
- Debug.Assert(z3Model != null);
- LabeledLiterals labels = z3.GetRelevantLabels();
- Debug.Assert(labels != null);
-
- List<string> labelStrings = new List<string>();
- uint numLabels = labels.GetNumLabels();
- for (uint i = 0; i < numLabels; ++i)
- {
- Symbol sym = labels.GetLabel(i);
- string labelName = z3.GetSymbolString(sym);
- if (!labelName.StartsWith("@"))
- {
- labels.Disable(i);
- }
- labelStrings.Add(labelName);
- }
- boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
-
- if (boogieErrors.Count < this.config.Counterexamples)
- {
- z3.BlockLiterals(labels);
- log("block-literals {0}", labels);
- }
-
- labels.Dispose();
- z3Model.Dispose();
- if (boogieErrors.Count == this.config.Counterexamples)
- break;
- }
-
- if (boogieErrors.Count > 0)
- {
- return ProverInterface.Outcome.Invalid;
- }
- else if (outcome == LBool.False)
- {
- return ProverInterface.Outcome.Valid;
- }
- else
- {
- Debug.Assert(outcome == LBool.Undef);
- return ProverInterface.Outcome.Undetermined;
- }
- }
-
- public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions,
- out List<Z3ErrorModelAndLabels> boogieErrors,
- out List<int> unsatCore)
- {
- Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
- boogieErrors = new List<Z3ErrorModelAndLabels>();
- unsatCore = new List<int>();
- LBool outcome = LBool.Undef;
-
- Model z3Model;
- Term proof;
- Term[] core;
- Term[] assumption_terms = new Term[assumptions.Count];
- var logstring = "";
- for (int i = 0; i < assumptions.Count; i++)
- {
- Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
- Z3TermAst z3ast = (Z3TermAst)assumptions[i].Accept(visitor, linOptions);
- assumption_terms[i] = Unwrap(z3ast);
- logstring += string.Format("({0}) ", assumption_terms[i]);
- }
-
- log("(get-core {0})", logstring);
- outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);
-
- if (outcome != LBool.False)
- {
- Debug.Assert(z3Model != null);
- LabeledLiterals labels = z3.GetRelevantLabels();
- Debug.Assert(labels != null);
-
- List<string> labelStrings = new List<string>();
- uint numLabels = labels.GetNumLabels();
- for (uint i = 0; i < numLabels; ++i)
- {
- Symbol sym = labels.GetLabel(i);
- string labelName = z3.GetSymbolString(sym);
- if (!labelName.StartsWith("@"))
- {
- labels.Disable(i);
- }
- labelStrings.Add(labelName);
- }
- boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
-
- labels.Dispose();
- z3Model.Dispose();
- }
-
- if (boogieErrors.Count > 0)
- {
- return ProverInterface.Outcome.Invalid;
- }
- else if (outcome == LBool.False)
- {
- foreach (Term t in core)
- {
- for (int i = 0; i < assumption_terms.Length; i++)
- {
- if (t.Equals(assumption_terms[i]))
- unsatCore.Add(i);
- }
- }
- return ProverInterface.Outcome.Valid;
- }
- else
- {
- Debug.Assert(outcome == LBool.Undef);
- return ProverInterface.Outcome.Undetermined;
- }
- }
-
- public void TypeCheckBool(Z3TermAst term)
- {
- Term unwrapTerm = Unwrap(term);
- bool boolType = z3.GetSort(unwrapTerm).Equals(z3.MkBoolSort());
- if (!boolType)
- throw new Exception("Failed Bool Typecheck");
- }
-
- public void TypeCheckInt(Z3TermAst term)
- {
- Term unwrapTerm = Unwrap(term);
- bool intType = z3.GetSort(unwrapTerm).Equals(z3.MkIntSort());
- if (!intType)
- throw new Exception("Failed Int Typecheck");
- }
-
- public void DeclareType(string typeName)
- {
- log("(declare-sort {0})", typeName);
- }
-
- public void DeclareConstant(string constantName, Type boogieType)
- {
- Symbol symbolAst = GetSymbol(constantName);
- Z3Type typeAst = tm.GetType(boogieType);
- Sort unwrapTypeAst = Unwrap(typeAst);
-
- Term constAst = z3.MkConst(symbolAst, unwrapTypeAst);
- constants.Add(constantName, Wrap(constAst));
- log("(declare-funs (({0} {1})))", constAst, unwrapTypeAst);
- }
-
- public void DeclareFunction(string functionName, List<Type> domain, Type range)
- {
- Symbol symbolAst = GetSymbol(functionName);
-
- var domainStr = "";
- List<Sort> domainAst = new List<Sort>();
- foreach (Type domainType in domain)
- {
- Z3Type type = tm.GetType(domainType);
- Sort unwrapType = Unwrap(type);
- domainAst.Add(unwrapType);
- domainStr += unwrapType.ToString() + " ";
- }
- Z3Type rangeAst = tm.GetType(range);
- Sort unwrapRangeAst = Unwrap(rangeAst);
- FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), unwrapRangeAst);
- Z3TypeSafeConstDecl typeSafeConstDecl = Wrap(constDeclAst);
- functions.Add(functionName, typeSafeConstDecl);
- log("(declare-funs (({0} {1} {2})))", functionName, domainStr, unwrapRangeAst);
- }
-
- private List<Symbol> GetSymbols(List<string> symbolNames)
- {
- List<Symbol> symbols = new List<Symbol>();
- foreach (string symbolName in symbolNames)
- symbols.Add(GetSymbol(symbolName));
- return symbols;
- }
-
- private Symbol GetSymbol(string symbolName)
- {
- if (!symbols.ContainsKey(symbolName))
- {
- Symbol symbolAst = z3.MkSymbol(symbolName);
- symbols.Add(symbolName, symbolAst);
- }
- Symbol result;
- if (!symbols.TryGetValue(symbolName, out result))
- throw new Exception("symbol " + symbolName + " is undefined");
- return result;
- }
-
- public Z3TermAst GetConstant(string constantName, Type constantType)
- {
- Z3TypeSafeTerm typeSafeTerm;
- if (!constants.ContainsKey(constantName))
- this.DeclareConstant(constantName, constantType);
-
- if (!constants.TryGetValue(constantName, out typeSafeTerm))
- throw new Exception("constant " + constantName + " is not defined");
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeIntLiteral(string numeral)
- {
- Term term = z3.MkNumeral(numeral, z3.MkIntSort());
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeTrue()
- {
- Term term = z3.MkTrue();
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeFalse()
- {
- Term term = z3.MkFalse();
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child)
- {
- Symbol labelSymbol = this.GetSymbol(labelName);
- Term unwrapChild = Unwrap(child);
-
- Term labeledExpr = z3.MkLabel(labelSymbol, pos, unwrapChild);
-
- Z3TypeSafeTerm wrapLabeledExpr = Wrap(labeledExpr);
- labels.Add(labelName, wrapLabeledExpr);
- return wrapLabeledExpr;
- }
-
- public Z3LabeledLiterals GetRelevantLabels()
- {
- Z3SafeLabeledLiterals safeLiterals = new Z3SafeLabeledLiterals(z3.GetRelevantLabels());
- log("get-relevant-labels");
- return safeLiterals;
- }
-
- public Z3TermAst Make(string op, List<Z3TermAst> children)
- {
- Term[] unwrapChildren = Unwrap(children).ToArray();
- Term term;
- switch (op)
- {
- // formulas
- case "AND": term = z3.MkAnd(unwrapChildren); break;
- case "OR": term = z3.MkOr(unwrapChildren); break;
- case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break;
- case "NOT": term = z3.MkNot(unwrapChildren[0]); break;
- case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break;
- // terms
- case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break;
- case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break;
- case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break;
- // terms
- case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break;
- case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break;
- case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break;
- case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break;
- case "+": term = z3.MkAdd(unwrapChildren); break;
- case "-": term = z3.MkSub(unwrapChildren); break;
- case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break;
- case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break;
- case "*": term = z3.MkMul(unwrapChildren); break;
- default:
- {
- FuncDecl f = GetFunction(op);
- term = z3.MkApp(f, unwrapChildren);
- }
- break;
- }
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- private FuncDecl GetFunction(string functionName)
- {
- Z3TypeSafeConstDecl function;
- if (!functions.TryGetValue(functionName, out function))
- throw new Exception("function " + functionName + " is undefined");
- FuncDecl unwrapFunction = Unwrap(function);
- return unwrapFunction;
- }
-
- public Z3TermAst MakeArraySelect(List<Z3TermAst> args)
- {
- Term[] unwrapChildren = Unwrap(args).ToArray();
- return Wrap(z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]));
- }
-
- public Z3TermAst MakeArrayStore(List<Z3TermAst> args)
- {
- Term[] unwrapChildren = Unwrap(args).ToArray();
- return Wrap(z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]));
- }
- }
}
\ No newline at end of file diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs index b8aa607f..b129b378 100644 --- a/Source/Provers/Z3api/StubContext.cs +++ b/Source/Provers/Z3api/StubContext.cs @@ -45,6 +45,9 @@ namespace Microsoft.Boogie.Z3 { public Z3TermAst MakeIntLiteral(string numeral) {
return new Z3StubTermAst();
}
+ public Z3TermAst MakeBvLiteral(int i, uint bvSize) {
+ return new Z3StubTermAst();
+ }
public Z3TermAst MakeTrue() {
return new Z3StubTermAst();
}
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index 009a6a59..e1c6de0b 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -65,93 +65,107 @@ namespace Microsoft.Boogie.Z3 }
}
- private Dictionary<MapType, Z3Type> mapTypes = new Dictionary<MapType, Z3Type>(new MapTypeComparator());
- private Dictionary<BvType, Z3Type> bvTypes = new Dictionary<BvType, Z3Type>(new BvTypeComparator());
- private Dictionary<BasicType, Z3Type> basicTypes = new Dictionary<BasicType, Z3Type>(new BasicTypeComparator());
- private Z3Context container;
+ private class CtorTypeComparator : IEqualityComparer<CtorType> {
+ public bool Equals(CtorType x, CtorType y) {
+ return (x.Decl.Name == y.Decl.Name);
+ }
+
+ public int GetHashCode(CtorType ctorType) {
+ return ctorType.Decl.Name.GetHashCode();
+ }
+ }
+
+ private Dictionary<MapType, Sort> mapTypes = new Dictionary<MapType, Sort>(new MapTypeComparator());
+ private Dictionary<BvType, Sort> bvTypes = new Dictionary<BvType, Sort>(new BvTypeComparator());
+ private Dictionary<BasicType, Sort> basicTypes = new Dictionary<BasicType, Sort>(new BasicTypeComparator());
+ private Dictionary<CtorType, Sort> ctorTypes = new Dictionary<CtorType, Sort>(new CtorTypeComparator());
- public Z3TypeCachedBuilder(Z3Context context)
+ private Z3apiProverContext container;
+
+ public Z3TypeCachedBuilder(Z3apiProverContext context)
{
this.container = context;
}
- private Z3Type GetMapType(MapType mapType)
- {
- Context z3 = ((Z3SafeContext)container).z3;
- if (!mapTypes.ContainsKey(mapType))
- {
- Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1");
- Z3Type domain = GetType(mapType.Arguments[0]);
- Z3Type range = GetType(mapType.Result);
- Z3Type typeAst = BuildMapType(domain, range);
- mapTypes.Add(mapType, typeAst);
+ private Sort GetMapType(MapType mapType) {
+ Context z3 = ((Z3apiProverContext)container).z3;
+ if (!mapTypes.ContainsKey(mapType)) {
+ Type result = mapType.Result;
+ for (int i = mapType.Arguments.Length-1; i > 0; i--) {
+ GetType(result);
+ result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result);
}
- Z3Type result;
- bool containsKey = mapTypes.TryGetValue(mapType, out result);
- Debug.Assert(containsKey);
- return result;
+ mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result)));
+ }
+ return mapTypes[mapType];
}
- private Z3Type GetBvType(BvType bvType)
+ private Sort GetBvType(BvType bvType)
{
if (!bvTypes.ContainsKey(bvType))
{
- Z3Type typeAst = BuildBvType(bvType);
+ Sort typeAst = BuildBvType(bvType);
bvTypes.Add(bvType, typeAst);
}
- Z3Type result;
+ Sort result;
bool containsKey = bvTypes.TryGetValue(bvType, out result);
Debug.Assert(containsKey);
return result;
}
- private Z3Type GetBasicType(BasicType basicType)
+ private Sort GetBasicType(BasicType basicType)
{
if (!basicTypes.ContainsKey(basicType))
{
- Z3Type typeAst = BuildBasicType(basicType);
+ Sort typeAst = BuildBasicType(basicType);
basicTypes.Add(basicType, typeAst);
}
- Z3Type result;
+ Sort result;
bool containsKey = basicTypes.TryGetValue(basicType, out result);
Debug.Assert(containsKey);
return result;
}
- public virtual Z3Type GetType(Type boogieType)
- {
- if (boogieType.GetType().Equals(typeof(BvType)))
- return GetBvType((BvType)boogieType);
- else if (boogieType.GetType().Equals(typeof(BasicType)))
- return GetBasicType((BasicType)boogieType);
- else if (boogieType.GetType().Equals(typeof(MapType)))
- return GetMapType((MapType)boogieType);
- else
- throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
+ private Sort GetCtorType(CtorType ctorType) {
+ if (!ctorTypes.ContainsKey(ctorType)) {
+ Sort typeAst = BuildCtorType(ctorType);
+ ctorTypes.Add(ctorType, typeAst);
+ }
+ Sort result;
+ bool containsKey = ctorTypes.TryGetValue(ctorType, out result);
+ Debug.Assert(containsKey);
+ return result;
}
- private Z3Type WrapType(Sort typeAst)
- {
- return new Z3SafeType(typeAst);
+ public virtual Sort GetType(Type boogieType) {
+ System.Type type = boogieType.GetType();
+ if (type.Equals(typeof(BvType)))
+ return GetBvType((BvType)boogieType);
+ else if (type.Equals(typeof(BasicType)))
+ return GetBasicType((BasicType)boogieType);
+ else if (type.Equals(typeof(MapType)))
+ return GetMapType((MapType)boogieType);
+ else if (type.Equals(typeof(CtorType)))
+ return GetCtorType((CtorType)boogieType);
+ else
+ throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
}
- public Z3Type BuildMapType(Z3Type domain, Z3Type range)
+ public Sort BuildMapType(Sort domain, Sort range)
{
- Context z3 = ((Z3SafeContext)container).z3;
- Sort typeAst = z3.MkArraySort(((Z3SafeType)domain).TypeAst, ((Z3SafeType)range).TypeAst);
- return WrapType(typeAst);
+ Context z3 = ((Z3apiProverContext)container).z3;
+ return z3.MkArraySort(domain, range);
}
- public Z3Type BuildBvType(BvType bvType)
+ public Sort BuildBvType(BvType bvType)
{
- Context z3 = ((Z3SafeContext)container).z3;
- Sort typeAst = z3.MkBvSort((uint)bvType.Bits);
- return WrapType(typeAst);
+ Context z3 = ((Z3apiProverContext)container).z3;
+ return z3.MkBvSort((uint)bvType.Bits);
}
- public Z3Type BuildBasicType(BasicType basicType)
+ public Sort BuildBasicType(BasicType basicType)
{
- Context z3 = ((Z3SafeContext)container).z3;
+ Context z3 = ((Z3apiProverContext)container).z3;
Sort typeAst;
if (basicType.IsBool)
{
@@ -163,9 +177,14 @@ namespace Microsoft.Boogie.Z3 }
else
throw new Exception("Unknown Basic Type " + basicType.ToString());
- return WrapType(typeAst);
+ return typeAst;
}
- }
- public class Z3Type { }
+ public Sort BuildCtorType(CtorType ctorType) {
+ Context z3 = ((Z3apiProverContext)container).z3;
+ if (ctorType.Arguments.Length > 0)
+ throw new Exception("Type constructor of non-zero arity are not handled");
+ return z3.MkSort(ctorType.Decl.Name);
+ }
+ }
}
\ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index c2eeb45f..149a23f1 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -11,54 +11,135 @@ using System.Collections.Generic; using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
+using Microsoft.Z3;
namespace Microsoft.Boogie.Z3
{
- public class Z3apiExprLineariser : IVCExprVisitor<Z3TermAst, LineariserOptions>
+ public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>
{
- private Z3apiOpLineariser OpLinObject = null;
- private IVCExprOpVisitor<Z3TermAst, LineariserOptions> OpLineariser
+ private Z3apiOpLineariser opLineariser = null;
+ private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser
{
get
{
Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);
- if (OpLinObject == null)
- OpLinObject = new Z3apiOpLineariser(this);
- return OpLinObject;
+ if (opLineariser == null)
+ opLineariser = new Z3apiOpLineariser(this);
+ return opLineariser;
}
}
internal readonly UniqueNamer namer;
- internal readonly Dictionary<VCExprVar, Z3TermAst> letBindings;
- protected Z3Context cm;
+ internal readonly Dictionary<VCExprVar, Term> letBindings;
+ protected Z3apiProverContext cm;
- public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer)
+ public Z3apiExprLineariser(Z3apiProverContext cm, UniqueNamer namer)
{
this.cm = cm;
this.namer = namer;
- this.letBindings = new Dictionary<VCExprVar, Z3TermAst>();
+ this.letBindings = new Dictionary<VCExprVar, Term>();
}
- public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)
+ public Term Linearise(VCExpr expr, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(expr != null);
- return expr.Accept<Z3TermAst, LineariserOptions>(this, options);
+ return expr.Accept<Term, LineariserOptions>(this, options);
}
/////////////////////////////////////////////////////////////////////////////////////
- public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options)
+ public Term Make(VCExprOp op, List<Term> children) {
+ Context z3 = cm.z3;
+ Term[] unwrapChildren = children.ToArray();
+ VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp;
+ if (boogieFunctionOp != null) {
+ FuncDecl f = cm.GetFunction(boogieFunctionOp.Func.Name);
+ return z3.MkApp(f, unwrapChildren);
+ }
+ VCExprDistinctOp distinctOp = op as VCExprDistinctOp;
+ if (distinctOp != null) {
+ return z3.MkDistinct(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.AndOp) {
+ return z3.MkAnd(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.OrOp) {
+ return z3.MkOr(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.ImpliesOp) {
+ return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.NotOp) {
+ return z3.MkNot(unwrapChildren[0]);
+ }
+
+ if (op == VCExpressionGenerator.EqOp) {
+ return z3.MkEq(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.NeqOp) {
+ return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1]));
+ }
+
+ if (op == VCExpressionGenerator.LtOp) {
+ return z3.MkLt(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.LeOp) {
+ return z3.MkLe(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.GtOp) {
+ return z3.MkGt(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.GeOp) {
+ return z3.MkGe(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.AddOp) {
+ return z3.MkAdd(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.SubOp) {
+ return z3.MkSub(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.DivOp) {
+ return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.MulOp) {
+ return z3.MkMul(unwrapChildren);
+ }
+
+ if (op == VCExpressionGenerator.ModOp) {
+ return z3.MkMod(unwrapChildren[0], unwrapChildren[1]);
+ }
+
+ if (op == VCExpressionGenerator.IfThenElseOp) {
+ return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);
+ }
+
+ throw new Exception("unhandled boogie operator");
+ }
+
+ public Term Visit(VCExprLiteral node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
if (node == VCExpressionGenerator.True)
- return cm.MakeTrue();
+ return cm.z3.MkTrue();
else if (node == VCExpressionGenerator.False)
- return cm.MakeFalse();
+ return cm.z3.MkFalse();
else if (node is VCExprIntLit)
- return cm.MakeIntLiteral(((VCExprIntLit)node).Val.ToString());
+ return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());
else
{
Contract.Assert(false);
@@ -66,7 +147,7 @@ namespace Microsoft.Boogie.Z3 }
}
- public Z3TermAst Visit(VCExprNAry node, LineariserOptions options)
+ public Term Visit(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -76,7 +157,7 @@ namespace Microsoft.Boogie.Z3 if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))
{
// handle these operators without recursion
- List<Z3TermAst> asts = new List<Z3TermAst>();
+ List<Term> asts = new List<Term>();
string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR";
IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
@@ -90,13 +171,13 @@ namespace Microsoft.Boogie.Z3 }
}
- return cm.Make(opString, asts);
+ return Make(op, asts);
}
- return node.Accept<Z3TermAst, LineariserOptions>(OpLineariser, options);
+ return node.Accept<Term, LineariserOptions>(OpLineariser, options);
}
- public Z3TermAst Visit(VCExprVar node, LineariserOptions options)
+ public Term Visit(VCExprVar node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -111,7 +192,7 @@ namespace Microsoft.Boogie.Z3 }
}
- public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options)
+ public Term Visit(VCExprQuantifier node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -123,11 +204,11 @@ namespace Microsoft.Boogie.Z3 List<string> varNames;
List<Type> varTypes;
VisitBounds(node.BoundVars, out varNames, out varTypes);
- List<Z3PatternAst> patterns;
- List<Z3TermAst> no_patterns;
+ List<Pattern> patterns;
+ List<Term> no_patterns;
VisitTriggers(node.Triggers, options, out patterns, out no_patterns);
- Z3TermAst body = Linearise(node.Body, options);
- Z3TermAst result;
+ Term body = Linearise(node.Body, options);
+ Term result;
uint weight = 1;
string qid = "";
int skolemid = 0;
@@ -153,10 +234,10 @@ namespace Microsoft.Boogie.Z3 switch (node.Quan)
{
- case Quantifier.ALL:
- result = cm.MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
- case Quantifier.EX:
- result = cm.MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
+ case Microsoft.Boogie.VCExprAST.Quantifier.ALL:
+ result = MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
+ case Microsoft.Boogie.VCExprAST.Quantifier.EX:
+ result = MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
default:
throw new Exception("unknown quantifier kind " + node.Quan);
}
@@ -167,7 +248,18 @@ namespace Microsoft.Boogie.Z3 namer.PopScope();
}
}
-
+
+ private Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Pattern> patterns, List<Term> no_patterns, Term body) {
+ List<Term> bound = new List<Term>();
+ for (int i = 0; i < varNames.Count; i++) {
+ Term t = cm.GetConstant(varNames[i], boogieTypes[i]);
+ bound.Add(t);
+ }
+
+ Term termAst = cm.z3.MkQuantifier(isForall, weight, cm.z3.MkSymbol(qid), cm.z3.MkSymbol(skolemid.ToString()), patterns.ToArray(), no_patterns.ToArray(), bound.ToArray(), body);
+ return termAst;
+ }
+
private void VisitBounds(List<VCExprVar> boundVars, out List<string> varNames, out List<Type> varTypes)
{
varNames = new List<string>();
@@ -180,44 +272,42 @@ namespace Microsoft.Boogie.Z3 }
}
- private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Z3PatternAst> patterns, out List<Z3TermAst> no_patterns)
+ private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Pattern> patterns, out List<Term> no_patterns)
{
- patterns = new List<Z3PatternAst>();
- no_patterns = new List<Z3TermAst>();
+ patterns = new List<Pattern>();
+ no_patterns = new List<Term>();
foreach (VCTrigger trigger in triggers)
{
- List<Z3TermAst> exprs = new List<Z3TermAst>();
+ List<Term> exprs = new List<Term>();
foreach (VCExpr expr in trigger.Exprs)
{
System.Diagnostics.Debug.Assert(expr != null);
- Z3TermAst termAst = Linearise(expr, options);
+ Term termAst = Linearise(expr, options);
exprs.Add(termAst);
}
if (exprs.Count > 0)
{
- if (trigger.Pos)
- {
- Z3PatternAst pattern = cm.MakePattern(exprs);
- patterns.Add(pattern);
- }
- else
- {
- System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats");
- foreach (Z3TermAst expr in exprs)
- no_patterns.Add(expr);
- }
+ if (trigger.Pos) {
+ Pattern pattern = cm.z3.MkPattern(exprs.ToArray());
+ patterns.Add(pattern);
+ }
+ else {
+ System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats");
+ foreach (Term expr in exprs)
+ no_patterns.Add(expr);
+ }
}
}
}
- public Z3TermAst Visit(VCExprLet node, LineariserOptions options)
+ public Term Visit(VCExprLet node, LineariserOptions options)
{
foreach (VCExprLetBinding b in node)
{
- Z3TermAst defAst = Linearise(b.E, options);
+ Term defAst = Linearise(b.E, options);
letBindings.Add(b.V, defAst);
}
- Z3TermAst letAst = Linearise(node.Body, options);
+ Term letAst = Linearise(node.Body, options);
foreach (VCExprLetBinding b in node)
{
letBindings.Remove(b.V);
@@ -227,7 +317,7 @@ namespace Microsoft.Boogie.Z3 /////////////////////////////////////////////////////////////////////////////////////
- internal class Z3apiOpLineariser : IVCExprOpVisitor<Z3TermAst, LineariserOptions>
+ internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions>
{
[ContractInvariantMethod]
void ObjectInvariant()
@@ -245,100 +335,73 @@ namespace Microsoft.Boogie.Z3 ///////////////////////////////////////////////////////////////////////////////////
- private Z3TermAst WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)
+ private Term WriteApplication(VCExprOp op, IEnumerable<VCExpr> terms, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(op != null);
Contract.Requires(cce.NonNullElements(terms));
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in terms)
{
Contract.Assert(e != null);
args.Add(ExprLineariser.Linearise(e, options));
}
- return ExprLineariser.cm.Make(op, args);
+ return ExprLineariser.Make(op, args);
}
///////////////////////////////////////////////////////////////////////////////////
- public Z3TermAst VisitNotOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitNotOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("NOT", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitEqOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitEqOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("EQ", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitNeqOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("NEQ", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitAndOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitAndOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("AND", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitOrOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitOrOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("OR", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitImpliesOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- if (options.InverseImplies)
- {
- List<Z3TermAst> args = new List<Z3TermAst>();
-
- args.Add(ExprLineariser.Linearise(node[1], options));
- List<Z3TermAst> t = new List<Z3TermAst>();
- t.Add(ExprLineariser.Linearise(node[0], options));
- args.Add(ExprLineariser.cm.Make("NOT", t));
- return ExprLineariser.cm.Make("OR", args);
- }
- else
- {
- return WriteApplication("IMPLIES", node, options);
- }
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitDistinctOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)
{
- Contract.Requires(options != null);
- Contract.Requires(node != null);
-
- if (node.Length < 2)
- {
- return ExprLineariser.Linearise(VCExpressionGenerator.True, options);
- }
- else
- {
- List<Z3TermAst> args = new List<Z3TermAst>();
- foreach (VCExpr e in node)
- {
- Contract.Assert(e != null);
- args.Add(ExprLineariser.Linearise(e, options));
- }
- return ExprLineariser.cm.Make("DISTINCT", args);
- }
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitLabelOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -347,182 +410,191 @@ namespace Microsoft.Boogie.Z3 return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options));
}
- public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitSelectOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in node)
{
Contract.Assert(e != null);
args.Add(ExprLineariser.Linearise(e, options));
}
- return ExprLineariser.cm.MakeArraySelect(args);
- // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args);
+ System.Diagnostics.Debug.Assert(args.Count >= 2);
+
+ Term selectTerm = args[0];
+ for (int i = 1; i < args.Count; i++) {
+ selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]);
+ }
+ return selectTerm;
+ }
+
+ private Term ConstructStoreTerm(Term mapTerm, List<Term> args, int index) {
+ System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1);
+ if (index == args.Count - 2) {
+ return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]);
+ }
+ else {
+ Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1);
+ return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t);
+ }
}
- public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in node)
{
Contract.Assert(e != null);
args.Add(ExprLineariser.Linearise(e, options));
}
- return ExprLineariser.cm.MakeArrayStore(args);
- // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args);
+ return ConstructStoreTerm(args[0], args, 1);
}
- public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitBvOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("$make_bv" + node.Type.BvBits, node, options);
+ List<int> args = new List<int>();
+ foreach (VCExpr e in node) {
+ VCExprIntLit literal = e as VCExprIntLit;
+ System.Diagnostics.Debug.Assert(literal != null);
+ args.Add(literal.Val.ToInt);
+ }
+ System.Diagnostics.Debug.Assert(args.Count == 1);
+ return ExprLineariser.cm.z3.MkNumeral(args[0], ExprLineariser.cm.z3.MkBvSort((uint)node.Type.BvBits));
}
- public Z3TermAst VisitBvExtractOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(SimplifyLikeExprLineariser.BvExtractOpName(node), node, options);
+ public Term VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+
+ VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;
+ Contract.Assert(op != null);
+ System.Diagnostics.Debug.Assert(0 <= op.Start && op.Start < op.End);
+
+ List<Term> args = new List<Term>();
+ foreach (VCExpr e in node) {
+ Contract.Assert(e != null);
+ args.Add(ExprLineariser.Linearise(e, options));
+ }
+ System.Diagnostics.Debug.Assert(args.Count == 1);
+ return ExprLineariser.cm.z3.MkBvExtract((uint) op.End - 1, (uint) op.Start, args[0]);
}
- public Z3TermAst VisitBvConcatOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(SimplifyLikeExprLineariser.BvConcatOpName(node), node, options);
+ public Term VisitBvConcatOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+
+ VCExprBvConcatOp op = (VCExprBvConcatOp)node.Op;
+ Contract.Assert(op != null);
+
+ List<Term> args = new List<Term>();
+ foreach (VCExpr e in node) {
+ Contract.Assert(e != null);
+ args.Add(ExprLineariser.Linearise(e, options));
+ }
+ System.Diagnostics.Debug.Assert(args.Count == 2);
+ return ExprLineariser.cm.z3.MkBvConcat(args[0], args[1]);
}
- public Z3TermAst VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
-
- List<Z3TermAst> args = new List<Z3TermAst>();
- args.Add(ExprLineariser.Linearise(node[0], options));
- args.Add(ExprLineariser.Linearise(node[1], options));
- args.Add(ExprLineariser.Linearise(node[2], options));
- return ExprLineariser.cm.Make("ITE", args);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitCustomOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(node != null);
Contract.Requires(options != null);
- VCExprCustomOp op = (VCExprCustomOp)node.Op;
- List<Z3TermAst> args = new List<Z3TermAst>();
- foreach (VCExpr arg in node)
- {
- args.Add(ExprLineariser.Linearise(arg, options));
- }
- return ExprLineariser.cm.Make(op.Name, args);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitAddOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- if (CommandLineOptions.Clo.ReflectAdd)
- {
- return WriteApplication("Reflect$Add", node, options);
- }
- else
- {
- return WriteApplication("+", node, options);
- }
+ public Term VisitAddOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitSubOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitSubOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("-", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitMulOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitMulOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("*", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitDivOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitDivOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("/", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitModOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitModOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("%", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitLtOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitLtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitLeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<=", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitGtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication(">", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitGeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication(">=", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<:", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
+ public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("<::", node, options);
+ return WriteApplication(node.Op, node, options);
}
- public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
- Contract.Assert(op != null);
- string funcName = op.Func.Name;
- Contract.Assert(funcName != null);
- string bvzName = op.Func.FindStringAttribute("external");
- if (bvzName != null) funcName = bvzName;
-
- List<Z3TermAst> args = new List<Z3TermAst>();
- foreach (VCExpr e in node)
- {
- Contract.Assert(e != null);
- args.Add(ExprLineariser.Linearise(e, options));
- }
- return ExprLineariser.cm.Make(funcName, args);
+ return WriteApplication(node.Op, node, options);
}
}
}
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index 05cc8f9f..94184957 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -146,6 +146,14 @@ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
+ <ProjectReference Include="..\..\Model\Model.csproj">
+ <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
+ <Name>Model</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
<ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
<Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
<Name>VCExpr</Name>
@@ -169,8 +177,6 @@ </Compile>
<Compile Include="ContextLayer.cs" />
<Compile Include="ProverLayer.cs" />
- <Compile Include="SafeContext.cs" />
- <Compile Include="StubContext.cs" />
<Compile Include="TypeAdapter.cs">
<SubType>Code</SubType>
</Compile>
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 2e279479..8f8f145e 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -19,7 +19,7 @@ using Microsoft.Boogie.VCExprAST; namespace Microsoft.Boogie {
public class CalleeCounterexampleInfo {
public Counterexample counterexample;
- public List<object>/*!>!*/ args;
+ public List<Model.Element>/*!>!*/ args;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -28,7 +28,7 @@ namespace Microsoft.Boogie { }
- public CalleeCounterexampleInfo(Counterexample cex, List<object/*!>!*/> x) {
+ public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {
Contract.Requires(cex != null);
Contract.Requires(cce.NonNullElements(x));
counterexample = cex;
@@ -76,7 +76,7 @@ namespace Microsoft.Boogie { [Peer]
public BlockSeq Trace;
- public ErrorModel Model;
+ public Model Model;
public VC.ModelViewInfo MvInfo;
public ProverContext Context;
[Peer]
@@ -84,7 +84,7 @@ namespace Microsoft.Boogie { public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
- internal Counterexample(BlockSeq trace, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context) {
+ internal Counterexample(BlockSeq trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) {
Contract.Requires(trace != null);
Contract.Requires(context != null);
this.Trace = trace;
@@ -211,7 +211,7 @@ namespace Microsoft.Boogie { {
if (Model == null) return null;
- Model m = Model.ToModel();
+ Model m = Model;
var mvstates = m.TryGetFunc("@MV_state");
if (MvInfo == null || mvstates == null)
@@ -308,7 +308,7 @@ namespace Microsoft.Boogie { }
- public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+ public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
: base(trace, model, mvInfo, context) {
Contract.Requires(trace != null);
Contract.Requires(failingAssert != null);
@@ -338,7 +338,7 @@ namespace Microsoft.Boogie { }
- public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+ public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
: base(trace, model, mvInfo, context) {
Contract.Requires(!failingRequires.Free);
Contract.Requires(trace != null);
@@ -371,7 +371,7 @@ namespace Microsoft.Boogie { }
- public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, ErrorModel model, VC.ModelViewInfo mvInfo, ProverContext context)
+ public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)
: base(trace, model, mvInfo, context) {
Contract.Requires(trace != null);
Contract.Requires(context != null);
@@ -1131,6 +1131,7 @@ namespace VC { #region Create an assume command equating v_prime with its last incarnation in pred
#region Create an identifier expression for the last incarnation in pred
Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(block2Incarnation[pred]);
+
Expr pred_incarnation_exp;
Expr o = (Expr)predMap[v];
if (o == null) {
@@ -1236,17 +1237,38 @@ namespace VC { // processed all of a node's predecessors before we process the node.
Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();
Block exitBlock = null;
+ Hashtable exitIncarnationMap = null;
foreach (Block b in sortedNodes) {
Contract.Assert(b != null);
Contract.Assert(!block2Incarnation.Contains(b));
Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);
+ // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out.
+ b.liveVarsBefore = null;
+
+ // Decrement the succCount field in each predecessor. Once the field reaches zero in any block,
+ // all its successors have been passified. Consequently, its entry in block2Incarnation can be removed.
+ foreach (Block p in b.Predecessors) {
+ p.succCount--;
+ if (p.succCount == 0)
+ block2Incarnation.Remove(p);
+ }
+
#region Each block's map needs to be available to successor blocks
- block2Incarnation.Add(b, incarnationMap);
+ GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+ if (gotoCmd == null) {
+ b.succCount = 0;
+ }
+ else {
+ // incarnationMap needs to be added only if there is some successor of b
+ b.succCount = gotoCmd.labelNames.Length;
+ block2Incarnation.Add(b, incarnationMap);
+ }
#endregion Each block's map needs to be available to successor blocks
TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst);
exitBlock = b;
+ exitIncarnationMap = incarnationMap;
}
// Verify that exitBlock is indeed the unique exit block
@@ -1254,7 +1276,7 @@ namespace VC { Contract.Assert(exitBlock.TransferCmd is ReturnCmd);
#endregion Convert to Passive Commands
- return (Hashtable)block2Incarnation[exitBlock];
+ return exitIncarnationMap;
}
/// <summary>
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 85ceb8e3..1bb70879 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -609,6 +609,7 @@ namespace VC abstract public void Pop();
abstract public void AddAxiom(VCExpr vc);
abstract public void LogComment(string str);
+ abstract public void updateMainVC(VCExpr vcMain);
virtual public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
Outcome ret;
@@ -657,6 +658,11 @@ namespace VC numQueries = 0;
}
+ public override void updateMainVC(VCExpr vcMain)
+ {
+ this.vcMain = vcMain;
+ }
+
public override Outcome CheckVC()
{
Contract.Requires(vcMain != null);
@@ -757,6 +763,11 @@ namespace VC TheoremProver.Assert(vcMain, false);
}
+ public override void updateMainVC(VCExpr vcMain)
+ {
+ throw new NotImplementedException("Stratified non-incremental search is not yet supported with z3api");
+ }
+
public override Outcome CheckVC()
{
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
@@ -850,11 +861,11 @@ namespace VC public class VerificationState
{
// The VC of main
- public VCExpr vcMain;
+ public VCExpr vcMain { get; private set; }
// The call tree
public FCallHandler calls;
// Error reporter (stores models)
- public StratifiedInliningErrorReporter reporter;
+ public ProverInterface.ErrorHandler reporter;
// The theorem prover interface
//public Checker checker;
public StratifiedCheckerInterface checker;
@@ -872,7 +883,7 @@ namespace VC }
public VerificationState(VCExpr vcMain, FCallHandler calls,
- StratifiedInliningErrorReporter reporter, Checker checker)
+ ProverInterface.ErrorHandler reporter, Checker checker)
{
this.vcMain = vcMain;
this.calls = calls;
@@ -888,6 +899,12 @@ namespace VC vcSize = 0;
expansionCount = 0;
}
+
+ public void updateMainVC(VCExpr vcMain)
+ {
+ this.vcMain = vcMain;
+ checker.updateMainVC(vcMain);
+ }
}
public Outcome FindLeastToVerify(Implementation impl, Program program, ref HashSet<string> allBoolVars)
@@ -897,12 +914,26 @@ namespace VC // Record current time
var startTime = DateTime.Now;
+ // No Max: avoids theorem prover restarts
+ CommandLineOptions.Clo.MaxProverMemory = 0;
+
+ // Initialize cache
+ satQueryCache = new Dictionary<int, List<HashSet<string>>>();
+ unsatQueryCache = new Dictionary<int, List<HashSet<string>>>();
+
// Get the checker
Checker checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);
Contract.Assert(implName2StratifiedInliningInfo != null);
this.program = program;
+ // Build VCs for all procedures
+ foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)
+ {
+ Contract.Assert(info != null);
+ GenerateVCForStratifiedInlining(program, info, checker);
+ }
+
// Get the VC of the current procedure
VCExpr vcMain;
Hashtable/*<int, Absy!>*/ mainLabel2absy;
@@ -912,15 +943,30 @@ namespace VC Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);
vcMain = GenerateVC(impl, null, out mainLabel2absy, checker);
- StratifiedCheckerInterface apiChecker = null;
+ // Find all procedure calls in vc and put labels on them
+ FCallHandler calls = new FCallHandler(checker.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
+ calls.setCurrProcAsMain();
+ vcMain = calls.Mutate(vcMain, true);
- if (checker.TheoremProver is ApiProverInterface)
- {
- apiChecker = new ApiChecker(vcMain, new EmptyErrorHandler(), checker);
- }
- else
+ // Put all of the necessary state into one object
+ var vState = new VerificationState(vcMain, calls, new EmptyErrorHandler(), checker);
+ vState.coverageManager = null;
+
+ // We'll restore the original state of the theorem prover at the end
+ // of this procedure
+ vState.checker.Push();
+
+ // Do eager inlining
+ while (calls.currCandidates.Count > 0)
{
- apiChecker = new NormalChecker(vcMain, new EmptyErrorHandler(), checker);
+ List<int> toExpand = new List<int>();
+
+ foreach (int id in calls.currCandidates)
+ {
+ Debug.Assert(calls.getRecursionBound(id) <= 1, "Recursion not supported");
+ toExpand.Add(id);
+ }
+ DoExpansion(true, toExpand, vState);
}
// Find all the boolean constants
@@ -930,11 +976,12 @@ namespace VC var constant = decl as Constant;
if (constant == null) continue;
if (!allBoolVars.Contains(constant.Name)) continue;
- allConsts.Add(checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(constant));
+ var v = checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(constant);
+ allConsts.Add(v);
}
// Now, lets start the algo
- var min = refinementLoop(apiChecker, new HashSet<VCExprVar>(), allConsts, allConsts);
+ var min = refinementLoop(vState.checker, new HashSet<VCExprVar>(), allConsts, allConsts);
var ret = new HashSet<string>();
foreach (var v in min)
@@ -943,6 +990,9 @@ namespace VC ret.Add(v.Name);
}
allBoolVars = ret;
+
+ vState.checker.Pop();
+
return Outcome.Correct;
}
@@ -985,11 +1035,31 @@ namespace VC return refinementLoop(apiChecker, a, c, allVars);
}
+ Dictionary<int, List<HashSet<string>>> satQueryCache;
+ Dictionary<int, List<HashSet<string>>> unsatQueryCache;
+
private bool refinementLoopCheckPath(StratifiedCheckerInterface apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars)
{
var assumptions = new List<VCExpr>();
List<int> temp = null;
+ var query = new HashSet<string>();
+ varsToSet.Iter(v => query.Add(v.Name));
+
+ if (checkCache(query, unsatQueryCache))
+ {
+ apiChecker.LogComment("FindLeast: Query Cache Hit");
+ return true;
+ }
+ if (checkCache(query, satQueryCache))
+ {
+ apiChecker.LogComment("FindLeast: Query Cache Hit");
+ return false;
+ }
+
+
+ apiChecker.LogComment("FindLeast: Query Begin");
+
//Console.Write("Query: ");
foreach (var c in allVars)
{
@@ -1008,11 +1078,37 @@ namespace VC var o = apiChecker.CheckAssumptions(assumptions, out temp);
Debug.Assert(o == Outcome.Correct || o == Outcome.Errors);
//Console.WriteLine("Result = " + o.ToString());
+ apiChecker.LogComment("FindLeast: Query End");
+
+ if (o == Outcome.Correct)
+ {
+ insertCache(query, unsatQueryCache);
+ return true;
+ }
+
+ insertCache(query, satQueryCache);
+ return false;
+ }
- if (o == Outcome.Correct) return true;
+ private bool checkCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache)
+ {
+ if (!cache.ContainsKey(q.Count)) return false;
+ foreach (var s in cache[q.Count])
+ {
+ if (q.SetEquals(s)) return true;
+ }
return false;
}
+ private void insertCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache)
+ {
+ if (!cache.ContainsKey(q.Count))
+ {
+ cache.Add(q.Count, new List<HashSet<string>>());
+ }
+ cache[q.Count].Add(q);
+ }
+
public static void Partition<T>(HashSet<T> values, out HashSet<T> part1, out HashSet<T> part2)
{
part1 = new HashSet<T>();
@@ -1326,7 +1422,7 @@ namespace VC Outcome ret;
List<int> unsatCore;
- var reporter = vState.reporter;
+ var reporter = vState.reporter as StratifiedInliningErrorReporter;
var calls = vState.calls;
var checker = vState.checker;
@@ -1533,7 +1629,7 @@ namespace VC calls.currInlineCount = id;
calls.setCurrProc(procName);
expansion = calls.Mutate(expansion, true);
- vState.coverageManager.addRecentEdges(id);
+ if(vState.coverageManager != null) vState.coverageManager.addRecentEdges(id);
//expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
expansion = checker.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
@@ -1547,7 +1643,6 @@ namespace VC // Does on-demand inlining -- inlines procedures into the VC of main.
private void DoExpansionAndInline(List<int>/*!*/ candidates, VerificationState vState)
{
- Contract.Requires(vState.vcMain != null);
Contract.Requires(candidates != null);
Contract.Requires(vState.calls != null);
Contract.Requires(vState.checker != null);
@@ -1619,7 +1714,7 @@ namespace VC }
- vState.vcMain = inliner.Mutate(vState.vcMain, true);
+ vState.updateMainVC(inliner.Mutate(vState.vcMain, true));
vState.vcSize = SizeComputingVisitor.ComputeSize(vState.vcMain);
}
@@ -2207,7 +2302,7 @@ namespace VC {
if (errModel == null)
return;
- var cex = GenerateTraceMain(labels, errModel, mvInfo);
+ var cex = GenerateTraceMain(labels, errModel.ToModel(), mvInfo);
Debug.Assert(candidatesToExpand.Count == 0);
if(cex != null) callback.OnCounterexample(cex, null);
return;
@@ -2216,7 +2311,7 @@ namespace VC Contract.Assert(calls != null);
Contract.Assert(errModel != null);
- GenerateTraceMain(labels, errModel, mvInfo);
+ GenerateTraceMain(labels, errModel.ToModel(), mvInfo);
/*
foreach (string lab in labels)
@@ -2233,13 +2328,13 @@ namespace VC }
// Construct the interprocedural trace
- private Counterexample GenerateTraceMain(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo)
+ private Counterexample GenerateTraceMain(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo)
{
Contract.Requires(errModel != null);
Contract.Requires(cce.NonNullElements(labels));
if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null)
{
- errModel.Print(ErrorReporter.ModelWriter);
+ errModel.Write(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
@@ -2270,7 +2365,7 @@ namespace VC return newCounterexample;
}
- private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo,
+ private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,
int candidateId, Implementation procImpl)
{
Contract.Requires(errModel != null);
@@ -2319,7 +2414,7 @@ namespace VC }
private Counterexample GenerateTraceRec(
- IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo, int candidateId,
+ IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo, int candidateId,
Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,
Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)
{
@@ -2361,28 +2456,28 @@ namespace VC var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
// Record concrete value of the argument to this procedure
- var args = new List<int>();
+ var args = new List<Model.Element>();
if (expr is VCExprIntLit)
{
- args.Add(errModel.valueToPartition[(expr as VCExprIntLit).Val]);
+ args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));
}
else if (expr is VCExprVar)
{
var idExpr = expr as VCExprVar;
string name = context.Lookup(idExpr);
Contract.Assert(name != null);
- if (errModel.identifierToPartition.ContainsKey(name))
+ Model.Func f = errModel.TryGetFunc(name);
+ if (f != null)
{
- args.Add(errModel.identifierToPartition[name]);
+ args.Add(f.GetConstant());
}
}
else
{
Contract.Assert(false);
}
- var values = errModel.PartitionsToValues(args);
calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(null, values);
+ new CalleeCounterexampleInfo(null, args);
continue;
}
@@ -2401,7 +2496,7 @@ namespace VC calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
new CalleeCounterexampleInfo(
cce.NonNull(GenerateTrace(labels, errModel, mvInfo, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),
- new List<object>());
+ new List<Model.Element>());
}
}
@@ -2485,6 +2580,39 @@ namespace VC }
}
+ public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
+ {
+ // Construct the set of inlined procs in the original program
+ var inlinedProcs = new HashSet<string>();
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ // Implementations
+ if (decl is Implementation)
+ {
+ var impl = decl as Implementation;
+ if (!(impl.Proc is LoopProcedure))
+ {
+ inlinedProcs.Add(impl.Name);
+ }
+ }
+
+ // And recording procedures
+ if (decl is Procedure)
+ {
+ var proc = decl as Procedure;
+ if (proc.Name.StartsWith(recordProcName))
+ {
+ Debug.Assert(!(decl is LoopProcedure));
+ inlinedProcs.Add(proc.Name);
+ }
+ }
+ }
+
+ return extractLoopTraceRec(
+ new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
+ mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ }
+
protected override bool elIsLoop(string procname)
{
LazyInliningInfo info = null;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 11db59b0..ff106380 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1627,6 +1627,9 @@ namespace VC { vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context);
}
break;
+ case CommandLineOptions.VCVariety.DagIterative:
+ vc = LetVCIterative(impl.Blocks, controlFlowVariable, label2absy, ch.TheoremProver.Context);
+ break;
case CommandLineOptions.VCVariety.Doomed:
vc = FlatBlockVC(impl, label2absy, false, false, true, ch.TheoremProver.Context);
break;
@@ -1919,7 +1922,7 @@ namespace VC { Contract.Assert(traceNodes.Contains(entryBlock));
trace.Add(entryBlock);
- Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, MvInfo, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());
+ Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel == null ? null : errModel.ToModel(), MvInfo, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());
if (newCounterexample == null)
return;
@@ -2014,7 +2017,7 @@ namespace VC { if (b.Cmds.Has(a)) {
BlockSeq trace = new BlockSeq();
trace.Add(b);
- Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, MvInfo, context, incarnationOriginMap);
+ Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel == null ? null : errModel.ToModel(), MvInfo, context, incarnationOriginMap);
callback.OnCounterexample(newCounterexample, null);
goto NEXT_ASSERT;
}
@@ -2317,14 +2320,6 @@ namespace VC { storeIncarnationMaps(impl.Name, exitIncarnationMap);
#endregion
- if (CommandLineOptions.Clo.LiveVariableAnalysis == 1) {
- Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
- }
- // TODO: fix
- //else if (CommandLineOptions.Clo.LiveVariableAnalysis == 2) {
- // Microsoft.Boogie.InterProcGenKill.ClearLiveVariables(impl, program);
- //}
-
#region Peep-hole optimizations
if (CommandLineOptions.Clo.RemoveEmptyBlocks){
#region Get rid of empty blocks
@@ -2463,30 +2458,30 @@ namespace VC { }
}
- public Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
+ public virtual Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
{
// Construct the set of inlined procs in the original program
- var inlinedProcs = new Dictionary<string, Procedure>();
+ var inlinedProcs = new HashSet<string>();
foreach (var decl in program.TopLevelDeclarations)
{
if (decl is Procedure)
- {
+ {
if (!(decl is LoopProcedure))
{
var p = decl as Procedure;
- inlinedProcs.Add(p.Name, p);
+ inlinedProcs.Add(p.Name);
}
}
}
return extractLoopTraceRec(
- new CalleeCounterexampleInfo(cex, new List<object>()),
+ new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
}
- private CalleeCounterexampleInfo extractLoopTraceRec(
+ protected CalleeCounterexampleInfo extractLoopTraceRec(
CalleeCounterexampleInfo cexInfo, string currProc,
- Dictionary<string, Procedure> inlinedProcs,
+ HashSet<string> inlinedProcs,
Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
{
Contract.Requires(currProc != null);
@@ -2507,7 +2502,11 @@ namespace VC { for (int numInstr = 0; numInstr < block.Cmds.Length; numInstr ++) {
Cmd cmd = block.Cmds[numInstr];
var loc = new TraceLocation(numBlock, numInstr);
- if (!cex.calleeCounterexamples.ContainsKey(loc)) continue;
+ if (!cex.calleeCounterexamples.ContainsKey(loc))
+ {
+ if (getCallee(cex.getTraceCmd(loc), inlinedProcs) != null) callCnt++;
+ continue;
+ }
string callee = cex.getCalledProcName(cex.getTraceCmd(loc));
Contract.Assert(callee != null);
var calleeTrace = cex.calleeCounterexamples[loc];
@@ -2543,33 +2542,13 @@ namespace VC { // return the position of the i^th CallCmd in the block (count only those Calls that call a procedure in inlinedProcs).
// Assert failure if there isn't any.
// Assert that the CallCmd found calls "callee"
- private int getCallCmdPosition(Block block, int i, Dictionary<string, Procedure> inlinedProcs, string callee)
+ private int getCallCmdPosition(Block block, int i, HashSet<string> inlinedProcs, string callee)
{
Debug.Assert(i >= 1);
for (int pos = 0; pos < block.Cmds.Length; pos++)
{
Cmd cmd = block.Cmds[pos];
- string procCalled = null;
- if (cmd is CallCmd)
- {
- var cc = (CallCmd)cmd;
- if (inlinedProcs.ContainsKey(cc.Proc.Name))
- {
- procCalled = cc.Proc.Name;
- }
- }
-
- if (cmd is AssumeCmd)
- {
- var expr = (cmd as AssumeCmd).Expr as NAryExpr;
- if (expr != null)
- {
- if (inlinedProcs.ContainsKey(expr.Fun.FunctionName))
- {
- procCalled = expr.Fun.FunctionName;
- }
- }
- }
+ string procCalled = getCallee(cmd, inlinedProcs);
if (procCalled != null)
{
@@ -2586,6 +2565,32 @@ namespace VC { return -1;
}
+ private string getCallee(Cmd cmd, HashSet<string> inlinedProcs)
+ {
+ string procCalled = null;
+ if (cmd is CallCmd)
+ {
+ var cc = (CallCmd)cmd;
+ if (inlinedProcs.Contains(cc.Proc.Name))
+ {
+ procCalled = cc.Proc.Name;
+ }
+ }
+
+ if (cmd is AssumeCmd)
+ {
+ var expr = (cmd as AssumeCmd).Expr as NAryExpr;
+ if (expr != null)
+ {
+ if (inlinedProcs.Contains(expr.Fun.FunctionName))
+ {
+ procCalled = expr.Fun.FunctionName;
+ }
+ }
+ }
+ return procCalled;
+ }
+
protected virtual bool elIsLoop(string procname)
{
Contract.Requires(procname != null);
@@ -2618,11 +2623,11 @@ namespace VC { }
private static Counterexample LazyCounterexample(
- ErrorModel/*!*/ errModel, ModelViewInfo mvInfo,
+ Model/*!*/ errModel, ModelViewInfo mvInfo,
Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,
ProverContext/*!*/ context,
Program/*!*/ program,
- string/*!*/ implName, List<int>/*!*/ values)
+ string/*!*/ implName, List<Model.Element>/*!*/ values)
{
Contract.Requires(errModel != null);
Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
@@ -2641,9 +2646,10 @@ namespace VC { trace.Add(b);
VCExprVar cfcVar = boogieExprTranslator.LookupVariable(info.controlFlowVariable);
string cfcName = context.Lookup(cfcVar);
- int cfcPartition = errModel.LookupSkolemFunctionAt(cfcName + "!" + info.uniqueId, values);
- int cfcValue = errModel.LookupPartitionValue(cfcPartition);
-
+ Model.Func skolemFunction = errModel.TryGetSkolemFunc(cfcName + "!" + info.uniqueId);
+ Model.Element cfcValue = skolemFunction.TryPartialEval(values.ToArray());
+
+ Model.Func controlFlowFunction = errModel.GetFunc("ControlFlow");
var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
while (true) {
CmdSeq cmds = b.Cmds;Contract.Assert(cmds != null);
@@ -2652,7 +2658,7 @@ namespace VC { {
Cmd cmd = cce.NonNull( cmds[i]);
AssertCmd assertCmd = cmd as AssertCmd;
- if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId) == assertCmd.UniqueId)
+ if (assertCmd != null && controlFlowFunction.TryEval(cfcValue, errModel.MkIntElement(b.UniqueId)).AsInt() == assertCmd.UniqueId)
{
Counterexample newCounterexample;
newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, context, cce.NonNull(info.incarnationOriginMap));
@@ -2668,15 +2674,16 @@ namespace VC { Contract.Assert(calleeName != null);
if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;
- List<int> args = new List<int>();
+ List<Model.Element> args = new List<Model.Element>();
foreach (Expr expr in naryExpr.Args)
{Contract.Assert(expr != null);
VCExprVar exprVar;
string name;
LiteralExpr litExpr = expr as LiteralExpr;
+
if (litExpr != null)
{
- args.Add(errModel.valueToPartition[litExpr.Val]);
+ args.Add(errModel.MkElement(litExpr.Val.ToString()));
continue;
}
@@ -2688,7 +2695,7 @@ namespace VC { {
exprVar = boogieExprTranslator.LookupVariable(var);
name = context.Lookup(exprVar);
- args.Add(errModel.identifierToPartition[name]);
+ args.Add(errModel.GetFunc(name).GetConstant());
continue;
}
@@ -2732,17 +2739,18 @@ namespace VC { exprVar = boogieExprTranslator.LookupVariable(var);
name = context.Lookup(exprVar);
- args.Add(errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values));
+ Model.Func skolemFunction1 = errModel.TryGetSkolemFunc(name + "!" + info.uniqueId);
+ args.Add(skolemFunction1.TryPartialEval(values.ToArray()));
}
calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
new CalleeCounterexampleInfo(
LazyCounterexample(errModel, mvInfo, implName2LazyInliningInfo, context, program, calleeName, args),
- errModel.PartitionsToValues(args));
+ args);
}
GotoCmd gotoCmd = transferCmd as GotoCmd;
if (gotoCmd == null) break;
- int nextBlockId = errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId);
+ int nextBlockId = controlFlowFunction.TryEval(cfcValue, errModel.MkIntElement(b.UniqueId)).AsInt();
foreach (Block x in gotoCmd.labelTargets) {
if (nextBlockId == x.UniqueId) {
b = x;
@@ -2766,7 +2774,7 @@ namespace VC { }
static Counterexample TraceCounterexample(
- Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, ErrorModel errModel, ModelViewInfo mvInfo,
+ Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, Model errModel, ModelViewInfo mvInfo,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,
ProverContext/*!*/ context, Program/*!*/ program,
@@ -2807,13 +2815,13 @@ namespace VC { if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;
Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;
Contract.Assert(boogieExprTranslator != null);
- List<int> args = new List<int>();
+ List<Model.Element> args = new List<Model.Element>();
foreach (Expr expr in naryExpr.Args)
{Contract.Assert(expr != null);
LiteralExpr litExpr = expr as LiteralExpr;
if (litExpr != null)
{
- args.Add(errModel.valueToPartition[litExpr.Val]);
+ args.Add(errModel.MkElement(litExpr.Val.ToString()));
continue;
}
@@ -2824,12 +2832,12 @@ namespace VC { Contract.Assert(var != null);
string name = context.Lookup(var);
Contract.Assert(name != null);
- args.Add(errModel.identifierToPartition[name]);
+ args.Add(errModel.GetFunc(name).GetConstant());
}
calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
new CalleeCounterexampleInfo(
LazyCounterexample(errModel, mvInfo, implName2LazyInliningInfo, context, program, calleeName, args),
- errModel.PartitionsToValues(args));
+ args);
#endregion
}
@@ -3335,231 +3343,7 @@ namespace VC { }
}
- //returned int is zID
- static int GetValuesFromModel(Bpl.Expr expr, Hashtable /*Variable -> Expr*/ incarnationMap, ErrorModel errModel,
- Dictionary<Bpl.Expr/*!*/, object>/*!*/ exprToPrintableValue)
- //modifies exprToPrintableValue.*;
- {
- Contract.Requires(expr != null);
- Contract.Requires(incarnationMap != null);
- Contract.Requires(errModel != null);
- Contract.Requires(exprToPrintableValue != null);
- // call GetValuesFromModel on all proper subexpressions, returning their value,
- // so they only have to be computed once!
- if (expr is LiteralExpr) {
- // nothing needs to be added to the exprToPrintableValue map, because e.g. 0 -> 0 is not interesting
- object o = ((LiteralExpr) expr).Val;
- if (o == null) {
- o = "nullObject";
- }
- int idForExprVal;
- if (errModel.valueToPartition.TryGetValue(o, out idForExprVal)) {
- return idForExprVal;
- } else {
- return -1;
- }
- }
- else if (expr is IdentifierExpr) {
- // if the expression expr is in the incarnation map, then use its incarnation,
- // otherwise just use the actual expression
- string s = ((IdentifierExpr) expr).Name;
- object o = null;
- Variable v = ((IdentifierExpr) expr).Decl;
- if (v != null && incarnationMap.ContainsKey(v)) {
- if (incarnationMap[v] is IdentifierExpr) {
- s = ((IdentifierExpr) incarnationMap[v]).Name;
- } else if (incarnationMap[v] is LiteralExpr) {
- o = ((LiteralExpr) incarnationMap[v]).Val;
- }
- }
- // if o is not null, then we got a LiteralExpression, that needs separate treatment
- if (o == null) {
- // if the expression (respectively its incarnation) is mapped to some partition
- // then return that id, else return the error code -1
- if (errModel.identifierToPartition.ContainsKey(s)) {
- int i = errModel.identifierToPartition[s];
- // if the key is already in the map we can assume that it is the same map we would
- // get now and thus just ignore it
- if (!exprToPrintableValue.ContainsKey(expr)) {
- exprToPrintableValue.Add(expr, ValueFromZID(errModel, i, ((IdentifierExpr) expr).Name));
- }
- return i;
- } else {
- return -1;
- }
- } else if (errModel.valueToPartition.ContainsKey(o)) {
- int i = errModel.valueToPartition[o];
- if (!exprToPrintableValue.ContainsKey(expr))
- exprToPrintableValue.Add(expr, ValueFromZID(errModel, i));
- return i;
- } else {
- return -1;
- }
- }
- else if (expr is Bpl.NAryExpr) {
- Bpl.NAryExpr e = (Bpl.NAryExpr)expr;
- List<int> zargs = new List<int>();
- bool undefined = false;
- // do the recursion first
- foreach (Expr argument in ((NAryExpr) expr).Args) {
- int zid = -1;
- if (argument != null) {
- zid = GetValuesFromModel(argument, incarnationMap, errModel, exprToPrintableValue);
- }
- // if one of the arguments is 'undefined' then return -1 ('noZid') for this
- // but make sure the recursion is complete first1
- if (zid == -1) {
- undefined = true;
- }
- zargs.Add(zid);
- }
- IAppliable fun = e.Fun;
- Contract.Assert(fun != null);
- string functionName = fun.FunctionName; // PR: convert to select1, select2, etc in case of a map?
- // same as IndexedExpr:
- int id = TreatFunction(functionName, zargs, undefined, errModel);
- if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {
- exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));
- }
- return id;
- }
- else if (expr is Bpl.OldExpr) {
- //Bpl.OldExpr e = (Bpl.OldExpr)expr;
- // We do not know which heap is the old heap and what the latest state change was,
- // therefore we cannot return anything useful here!
- return -1;
- }
- else if (expr is Bpl.QuantifierExpr) {
- Bpl.QuantifierExpr q = (Bpl.QuantifierExpr)expr;
- for (int i = 0; i < q.Dummies.Length; i++) {
- Bpl.Variable v = q.Dummies[i];
- if (v != null) {
- // add to the incarnation map a connection between the bound variable v
- // of the quantifier and its skolemized incarnation, if available,
- // i.e., search through the list of identifiers in the model and look for
- // v.sk.(q.SkolemId), only pick those that are directly associated to a value
- // DISCLAIMER: of course it is very well possible that one of these incarnations
- // could be used without actually having a value, but it seems better to pick those
- // with a value, that is they are more likely to contribute useful information to
- // the output
- List<Bpl.IdentifierExpr> quantVarIncarnationList = new List<Bpl.IdentifierExpr>();
- List<int> incarnationZidList = new List<int>();
- int numberOfNonNullValueIncarnations = 0;
- for (int j = 0; j < errModel.partitionToIdentifiers.Count; j++){
- List<string> pti = errModel.partitionToIdentifiers[j];
- Contract.Assert(pti != null);
- if (pti != null) {
- for (int k = 0; k < pti.Count; k++) {
- // look for v.sk.(q.SkolemId)
- // if there is more than one look at if there is exactly one with a non-null value
- // associated, see above explanation
- if (pti[k].StartsWith(v + ".sk." + q.SkolemId) &&
- errModel.partitionToValue[errModel.identifierToPartition[pti[k]]] != null) {
- quantVarIncarnationList.Add(new Bpl.IdentifierExpr(Bpl.Token.NoToken, pti[k], new Bpl.UnresolvedTypeIdentifier(Token.NoToken, "TName")));
- incarnationZidList.Add(j);
- if (errModel.partitionToValue[errModel.identifierToPartition[pti[k]]] != null) {
- numberOfNonNullValueIncarnations++;
- }
- }
- }
- }
- }
- // only one such variable found, associate it with v
- if (quantVarIncarnationList.Count == 1) {
- incarnationMap[v] = quantVarIncarnationList[0];
- } else if (quantVarIncarnationList.Count > 1 && numberOfNonNullValueIncarnations == 1) {
- // if there are multiple candidate incarnations and exactly one of them has a value
- // we can pick that one; otherwise it is not clear how to pick one out of multiple
- // incarnations without a value or out of multiple incarnations with a value associated
- for (int n = 0; n < incarnationZidList.Count; n++) {
- if (errModel.partitionToValue[incarnationZidList[n]] != null) {
- // quantVarIncarnationList and incarnationZidList are indexed in lockstep, so if
- // for the associated zid the partitionToValue map is non-null then that is the one
- // thus distinguished incarnation we want to put into the incarnationMap
- incarnationMap[v] = quantVarIncarnationList[n];
- break;
- }
- }
- }
- }
- }
- // generate the value of the body but do not return that outside
- GetValuesFromModel(q.Body, incarnationMap, errModel, exprToPrintableValue);
- // the quantifier cannot contribute any one value to the rest of the
- // expression, thus just return -1
- return -1;
- }
- else if (expr is Bpl.BvExtractExpr) {
- Bpl.BvExtractExpr ex = (Bpl.BvExtractExpr) expr;
- Bpl.Expr e0 = ex.Bitvector;
- Bpl.Expr e1 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.Start));
- Bpl.Expr e2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.End));
- string functionName = "$bv_extract";
- List<int> zargs = new List<int>();
- bool undefined = false;
-
- int zid = -1;
- zid = GetValuesFromModel(e0, incarnationMap, errModel, exprToPrintableValue);
- if (zid == -1) {
- undefined = true;
- }
- zargs.Add(zid);
-
- zid = -1;
- zid = GetValuesFromModel(e1, incarnationMap, errModel, exprToPrintableValue);
- if (zid == -1) {
- undefined = true;
- }
- zargs.Add(zid);
-
- zid = -1;
- zid = GetValuesFromModel(e2, incarnationMap, errModel, exprToPrintableValue);
- if (zid == -1) {
- undefined = true;
- }
- zargs.Add(zid);
-
- //same as NAryExpr:
- int id = TreatFunction(functionName, zargs, undefined, errModel);
- if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {
- exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));
- }
- return id;
- }
- else if (expr is Bpl.BvConcatExpr) {
- // see comment above
- Bpl.BvConcatExpr bvc = (Bpl.BvConcatExpr) expr;
- string functionName = "$bv_concat";
- List<int> zargs = new List<int>();
- bool undefined = false;
-
- int zid = -1;
- zid = GetValuesFromModel(bvc.E0, incarnationMap, errModel, exprToPrintableValue);
- if (zid == -1) {
- undefined = true;
- }
- zargs.Add(zid);
-
- zid = -1;
- zid = GetValuesFromModel(bvc.E0, incarnationMap, errModel, exprToPrintableValue);
- if (zid == -1) {
- undefined = true;
- }
- zargs.Add(zid);
-
- //same as NAryExpr:
- int id = TreatFunction(functionName, zargs, undefined, errModel);
- if (id != -1 && !exprToPrintableValue.ContainsKey(expr)) {
- exprToPrintableValue.Add(expr, ValueFromZID(errModel, id));
- }
- return id;
- }
- else {
- Contract.Assert(false);throw new cce.UnreachableException(); // unexpected Bpl.Expr
- }
- }
-
- protected static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel, ModelViewInfo mvInfo, ProverContext context,
+ protected static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, Model errModel, ModelViewInfo mvInfo, ProverContext context,
Dictionary<Incarnation, Absy> incarnationOriginMap)
{
Contract.Requires(cmd != null);
@@ -3570,16 +3354,7 @@ namespace VC { Contract.Ensures(Contract.Result<Counterexample>() != null);
List<string> relatedInformation = new List<string>();
- if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {
- if (cmd.OrigExpr != null && cmd.IncarnationMap != null && errModel != null) {
-
- // get all possible information first
- Dictionary<Expr, object> exprToPrintableValue = new Dictionary<Expr, object>();
- GetValuesFromModel(cmd.OrigExpr, cmd.IncarnationMap, errModel, exprToPrintableValue);
- // then apply the strategies
- ApplyEnhancedErrorPrintingStrategy(cmd.OrigExpr, cmd.IncarnationMap, cmd.ErrorDataEnhanced, errModel, exprToPrintableValue, relatedInformation, true, incarnationOriginMap);
- }
- }
+
// See if it is a special assert inserted in translation
if (cmd is AssertRequiresCmd)
@@ -3606,16 +3381,6 @@ namespace VC { }
}
- // static void EmitImpl(Implementation! impl, bool printDesugarings) {
- // int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
- // CommandLineOptions.Clo.PrintUnstructured = 2; // print only the unstructured program
- // bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings;
- // CommandLineOptions.Clo.PrintDesugarings = printDesugarings;
- // impl.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
- // CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;
- // CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
- // }
-
static VCExpr LetVC(Block startBlock,
Variable controlFlowVariable,
Hashtable/*<int, Absy!>*/ label2absy,
@@ -3631,6 +3396,73 @@ namespace VC { return proverCtxt.ExprGen.Let(bindings, startCorrect);
}
+ static VCExpr LetVCIterative(List<Block> blocks,
+ Variable controlFlowVariable,
+ Hashtable label2absy,
+ ProverContext proverCtxt) {
+ Contract.Requires(blocks != null);
+ Contract.Requires(proverCtxt != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ Graph<Block> dag = new Graph<Block>();
+ dag.AddSource(blocks[0]);
+ foreach (Block b in blocks) {
+ GotoCmd gtc = b.TransferCmd as GotoCmd;
+ if (gtc != null) {
+ Contract.Assume(gtc.labelTargets != null);
+ foreach (Block dest in gtc.labelTargets) {
+ Contract.Assert(dest != null);
+ dag.AddEdge(dest, b);
+ }
+ }
+ }
+ IEnumerable sortedNodes = dag.TopologicalSort();
+ Contract.Assert(sortedNodes != null);
+
+ Dictionary<Block, VCExprVar> blockVariables = new Dictionary<Block, VCExprVar>();
+ List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
+ VCExpressionGenerator gen = proverCtxt.ExprGen;
+ Contract.Assert(gen != null);
+ foreach (Block block in sortedNodes) {
+ VCExpr SuccCorrect;
+ GotoCmd gotocmd = block.TransferCmd as GotoCmd;
+ if (gotocmd == null) {
+ ReturnExprCmd re = block.TransferCmd as ReturnExprCmd;
+ if (re == null) {
+ SuccCorrect = VCExpressionGenerator.True;
+ }
+ else {
+ SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr);
+ }
+ }
+ else {
+ Contract.Assert(gotocmd.labelTargets != null);
+ List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);
+ foreach (Block successor in gotocmd.labelTargets) {
+ Contract.Assert(successor != null);
+ VCExpr s = blockVariables[successor];
+ if (controlFlowVariable != null) {
+ VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(block.UniqueId)));
+ VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successor.UniqueId)));
+ s = gen.Implies(controlTransferExpr, s);
+ }
+ SuccCorrectVars.Add(s);
+ }
+ SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);
+ }
+
+ VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);
+ VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+
+ VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
+ bindings.Add(gen.LetBinding(v, vc));
+ blockVariables.Add(block, v);
+ }
+
+ return proverCtxt.ExprGen.Let(bindings, blockVariables[blocks[0]]);
+ }
+
static VCExpr LetVC(Block block,
Variable controlFlowVariable,
Hashtable/*<int, Absy!>*/ label2absy,
|