diff options
40 files changed, 2963 insertions, 341 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 4531b9bb..c12ba47d 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -651,15 +651,49 @@ namespace Microsoft.Boogie { {
if (CommandLineOptions.Clo.AbstractHoudini != null)
{
- CommandLineOptions.Clo.PrintErrorModel = 1;
+ //CommandLineOptions.Clo.PrintErrorModel = 1;
+ CommandLineOptions.Clo.UseProverEvaluate = true;
+ CommandLineOptions.Clo.ModelViewFile = "z3model";
CommandLineOptions.Clo.UseArrayTheory = true;
CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
- CommandLineOptions.Clo.ProverCCLimit = 1;
+ // Declare abstract domains
+ var domains = new List<System.Tuple<string, Houdini.IAbstractDomain>>(new System.Tuple<string, Houdini.IAbstractDomain>[] {
+ System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain),
+ System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain),
+ System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain),
+ System.Tuple.Create("PredicateAbs", new Houdini.PredicateAbsElem() as Houdini.IAbstractDomain),
+ System.Tuple.Create("IA[HoudiniConst]", new Houdini.IndependentAttribute<Houdini.HoudiniConst>() as Houdini.IAbstractDomain),
+ System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute<Houdini.ConstantProp>() as Houdini.IAbstractDomain),
+ System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute<Houdini.Intervals>() as Houdini.IAbstractDomain)
+ });
+
+ domains.Iter(tup => Houdini.AbstractDomainFactory.Register(tup.Item2));
+
+ // Find the abstract domain
+ Houdini.IAbstractDomain domain = null;
+ foreach (var tup in domains)
+ {
+ if (tup.Item1 == CommandLineOptions.Clo.AbstractHoudini)
+ {
+ domain = tup.Item2;
+ break;
+ }
+ }
+ if (domain == null)
+ {
+ Console.WriteLine("Domain {0} not found", CommandLineOptions.Clo.AbstractHoudini);
+ Console.WriteLine("Supported domains are:");
+ domains.Iter(tup => Console.WriteLine(" {0}", tup.Item1));
+ throw new Houdini.AbsHoudiniInternalError("Domain not found");
+ }
// Run Abstract Houdini
- Houdini.PredicateAbs.Initialize(program);
- var abs = new Houdini.AbstractHoudini(program);
- abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
+ var abs = new Houdini.AbsHoudini(program, domain);
+ abs.ComputeSummaries();
+
+ //Houdini.PredicateAbs.Initialize(program);
+ //var abs = new Houdini.AbstractHoudini(program);
+ //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
return PipelineOutcome.Done;
}
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index e62a98cb..5149f69c 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1798,6 +1798,19 @@ namespace Microsoft.Boogie { this.Outs = outs;
}
+ public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs, QKeyValue kv, bool IsAsync)
+ : base(tok, kv)
+ {
+ Contract.Requires(outs != null);
+ Contract.Requires(ins != null);
+ Contract.Requires(callee != null);
+ Contract.Requires(tok != null);
+ this.callee = callee;
+ this.Ins = ins;
+ this.Outs = outs;
+ this.IsAsync = IsAsync;
+ }
+
public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs, QKeyValue kv, CallCmd inParallelWith)
: base(tok, kv)
{
@@ -1816,6 +1829,9 @@ namespace Microsoft.Boogie { if (IsFree) {
stream.Write("free ");
}
+ if (IsAsync) {
+ stream.Write("async ");
+ }
stream.Write("call ");
EmitAttributes(stream, Attributes);
string sep = "";
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index cb7b01a3..8cd3a2ea 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -200,6 +200,11 @@ namespace Microsoft.Boogie { moreProcessingRequired = true;
modSets[localProc].Add(var);
}
+ public override Expr VisitCodeExpr(CodeExpr node) {
+ // don't go into the code expression, since it can only modify variables local to the code expression,
+ // and the mod-set analysis is interested in global variables
+ return node;
+ }
}
public class VariableCollector : StandardVisitor {
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 1f8caff0..57910775 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -74,7 +74,7 @@ namespace Microsoft.Boogie { this.inlineCallback = cb;
}
- private static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) {
+ protected static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Requires(impl.Proc != null);
@@ -162,6 +162,12 @@ namespace Microsoft.Boogie { impl.Typecheck(tc);
}
+ // Redundant for this class; but gives a chance for other classes to
+ // override this and implement their own inlining policy
+ protected virtual int GetInlineCount(CallCmd callCmd, Implementation impl)
+ {
+ return GetInlineCount(impl);
+ }
// returns true if it is ok to further unroll the procedure
// otherwise, the procedure is not inlined at the call site
@@ -202,7 +208,7 @@ namespace Microsoft.Boogie { }
}
- private List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,
+ protected virtual List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,
VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies,
ref bool inlinedSomething) {
Contract.Requires(cce.NonNullElements(blocks));
@@ -237,7 +243,7 @@ namespace Microsoft.Boogie { continue;
}
- int inline = inlineDepth >= 0 ? inlineDepth : GetInlineCount(impl);
+ int inline = inlineDepth >= 0 ? inlineDepth : GetInlineCount(callCmd, impl);
if (inline > 0) { // at least one block should exist
Contract.Assume(impl != null);
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index c092139d..5298e7ff 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -7,6 +7,22 @@ using Microsoft.Boogie; namespace Microsoft.Boogie
{
+ public class LinearEraser : StandardVisitor
+ {
+ private QKeyValue Remove(QKeyValue iter)
+ {
+ if (iter == null) return null;
+ iter.Next = Remove(iter.Next);
+ return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next;
+ }
+
+ public override Variable VisitVariable(Variable node)
+ {
+ node.Attributes = Remove(node.Attributes);
+ return base.VisitVariable(node);
+ }
+ }
+
public class LinearTypechecker : StandardVisitor
{
public int errorCount;
@@ -25,9 +41,15 @@ namespace Microsoft.Boogie errorCount++;
}
private Dictionary<Variable, string> scope;
+ private HashSet<Variable> frame;
public override Implementation VisitImplementation(Implementation node)
{
scope = new Dictionary<Variable, string>();
+ frame = new HashSet<Variable>();
+ foreach (IdentifierExpr ie in node.Proc.Modifies)
+ {
+ frame.Add(ie.Decl);
+ }
for (int i = 0; i < node.OutParams.Length; i++)
{
string domainName = QKeyValue.FindStringAttribute(node.Proc.OutParams[i].Attributes, "linear");
@@ -97,7 +119,7 @@ namespace Microsoft.Boogie if (rhs == null)
{
Error(node, "Only variable can be assigned to a linear variable");
- continue;
+ continue;
}
string rhsDomainName = FindDomainName(rhs.Decl);
if (rhsDomainName == null)
@@ -116,6 +138,10 @@ namespace Microsoft.Boogie continue;
}
rhsVars.Add(rhs.Decl);
+ if (!CommandLineOptions.Clo.DoModSetAnalysis && rhs.Decl is GlobalVariable && !frame.Contains(rhs.Decl))
+ {
+ Error(node, "A linear variable on the right hand side of an assignment must be in the modifies set");
+ }
}
return base.VisitAssignCmd(node);
}
@@ -355,9 +381,8 @@ namespace Microsoft.Boogie foreach (var decl in program.TopLevelDeclarations)
{
- Implementation impl = decl as Implementation;
- if (impl == null) continue;
- Procedure proc = impl.Proc;
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
foreach (Variable v in program.GlobalVariables())
@@ -392,12 +417,7 @@ namespace Microsoft.Boogie {
proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInParams[domainName])));
}
- }
- foreach (var decl in program.TopLevelDeclarations)
- {
- Procedure proc = decl as Procedure;
- if (proc == null) continue;
- HashSet<string> domainNamesForOutParams = new HashSet<string>();
+ Dictionary<string, HashSet<Variable>> domainNameToOutParams = new Dictionary<string, HashSet<Variable>>();
foreach (Variable v in proc.OutParams)
{
var domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");
@@ -406,15 +426,57 @@ namespace Microsoft.Boogie {
linearDomains[domainName] = new LinearDomain(program, v, domainName);
}
- if (domainNamesForOutParams.Contains(domainName)) continue;
- domainNamesForOutParams.Add(domainName);
- proc.Modifies.Add(new IdentifierExpr(Token.NoToken, linearDomains[domainName].allocator));
+ if (!domainNameToOutParams.ContainsKey(domainName))
+ {
+ domainNameToOutParams[domainName] = new HashSet<Variable>();
+ }
+ domainNameToOutParams[domainName].Add(v);
+ }
+ foreach (string domainName in linearDomains.Keys)
+ {
+ LinearDomain domain = linearDomains[domainName];
+ var allocator = domain.allocator;
+ proc.Modifies.Add(new IdentifierExpr(Token.NoToken, allocator));
+ Expr oldExpr = new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, allocator));
+ Expr newExpr = new IdentifierExpr(Token.NoToken, allocator);
+ if (domainNameToScope.ContainsKey(domainName))
+ {
+ foreach (Variable v in domainNameToScope[domainName])
+ {
+ Expr oldVarExpr = new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v));
+ Expr newVarExpr = new IdentifierExpr(Token.NoToken, v);
+ oldExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? oldVarExpr : Singleton(oldVarExpr, domainName), oldExpr));
+ newExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? newVarExpr : Singleton(newVarExpr, domainName), newExpr));
+ }
+ }
+ if (domainNameToOutParams.ContainsKey(domainName))
+ {
+ foreach (Variable v in domainNameToOutParams[domainName])
+ {
+ Expr newVarExpr = new IdentifierExpr(Token.NoToken, v);
+ newExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? newVarExpr : Singleton(newVarExpr, domainName), newExpr));
+ }
+ }
+ proc.Ensures.Add(new Ensures(true, Expr.Binary(BinaryOperator.Opcode.Eq, oldExpr, newExpr)));
}
}
+
foreach (LinearDomain domain in linearDomains.Values)
{
program.TopLevelDeclarations.Add(domain.allocator);
+ program.TopLevelDeclarations.Add(domain.mapConstBool);
+ program.TopLevelDeclarations.Add(domain.mapConstInt);
+ program.TopLevelDeclarations.Add(domain.mapEqInt);
+ program.TopLevelDeclarations.Add(domain.mapImpBool);
+ program.TopLevelDeclarations.Add(domain.mapOrBool);
+ foreach (Axiom axiom in domain.axioms)
+ {
+ program.TopLevelDeclarations.Add(axiom);
+ }
}
+
+ var eraser = new LinearEraser();
+ eraser.VisitProgram(program);
}
private Expr Singleton(Expr e, string domainName)
@@ -460,18 +522,18 @@ namespace Microsoft.Boogie Variable v = ie.Decl;
if (!varToDomainName.ContainsKey(v)) continue;
var domainName = varToDomainName[v];
- if (!domainNameToHavocVars.ContainsKey(domainName))
- {
- domainNameToHavocVars[domainName] = new HashSet<Variable>();
- }
- domainNameToHavocVars[domainName].Add(v);
var allocator = linearDomains[domainName].allocator;
if (!copies.ContainsKey(allocator))
{
copies[allocator] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", allocator.Name), allocator.TypedIdent.Type));
}
- lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[allocator])));
- rhss.Add(new IdentifierExpr(Token.NoToken, allocator));
+ if (!domainNameToHavocVars.ContainsKey(domainName))
+ {
+ domainNameToHavocVars[domainName] = new HashSet<Variable>();
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[allocator])));
+ rhss.Add(new IdentifierExpr(Token.NoToken, allocator));
+ }
+ domainNameToHavocVars[domainName].Add(v);
}
if (lhss.Count > 0)
{
@@ -596,6 +658,7 @@ namespace Microsoft.Boogie public Function mapOrBool;
public Function mapImpBool;
public Function mapConstBool;
+ public List<Axiom> axioms;
public LinearDomain(Program program, Variable var, string domainName)
{
@@ -606,6 +669,7 @@ namespace Microsoft.Boogie this.elementType = mapType.Arguments[0];
}
this.allocator = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("allocator_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool)));
+ this.axioms = new List<Axiom>();
MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool);
MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Int);
@@ -613,29 +677,127 @@ namespace Microsoft.Boogie new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapOrBool.AddAttribute("builtin", "MapOr");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapOrBool.AddAttribute("builtin", "MapOr");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new ExprSeq(aie, bie));
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new VariableSeq(a, b), null,
+ new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)),
+ new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapImpBool = new Function(Token.NoToken, "linear@MapImp",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapImpBool.AddAttribute("builtin", "MapImp");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapImpBool.AddAttribute("builtin", "MapImp");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new ExprSeq(aie, bie));
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new VariableSeq(a, b), null,
+ new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)),
+ new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapConstBool = new Function(Token.NoToken, "linear@MapConstBool",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapConstBool.AddAttribute("builtin", "MapConst");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstBool.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.True)), xie));
+ var trueAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), trueTerm);
+ trueAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr));
+ var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.False)), xie));
+ var falseAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));
+ falseAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));
+ }
this.mapEqInt = new Function(Token.NoToken, "linear@MapEq",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapEqInt.AddAttribute("builtin", "MapEq");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapEqInt.AddAttribute("builtin", "MapEq");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new ExprSeq(aie, bie));
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new VariableSeq(a, b), null,
+ new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)),
+ new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapConstInt = new Function(Token.NoToken, "linear@MapConstInt",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));
- this.mapConstInt.AddAttribute("builtin", "MapConst");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstInt.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new ExprSeq(aie)), xie));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
}
}
}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index f11ff45a..f0c115d8 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -22,18 +22,12 @@ namespace Microsoft.Boogie public bool isAtomic;
// inParallelCall is true iff this procedure is involved in some parallel call
public bool inParallelCall;
- public Procedure yieldCheckerProc;
- public Implementation yieldCheckerImpl;
- public Procedure dummyAsyncTargetProc;
public ProcedureInfo()
{
containsYield = false;
isThreadStart = false;
isAtomic = true;
inParallelCall = false;
- yieldCheckerProc = null;
- yieldCheckerImpl = null;
- dummyAsyncTargetProc = null;
}
}
@@ -80,7 +74,6 @@ namespace Microsoft.Boogie {
procNameToInfo[currentImpl.Name].containsYield = true;
procNameToInfo[currentImpl.Name].isAtomic = false;
- CreateYieldCheckerProcedure(currentImpl.Proc);
return base.VisitYieldCmd(node);
}
public override Cmd VisitCallCmd(CallCmd node)
@@ -92,13 +85,6 @@ namespace Microsoft.Boogie if (node.IsAsync)
{
procNameToInfo[node.Proc.Name].isThreadStart = true;
- CreateYieldCheckerProcedure(node.Proc);
- if (procNameToInfo[node.Proc.Name].dummyAsyncTargetProc == null)
- {
- var dummyAsyncTargetName = string.Format("DummyAsyncTarget_{0}", node.Proc.Name);
- var dummyAsyncTargetProc = new Procedure(Token.NoToken, dummyAsyncTargetName, node.Proc.TypeParameters, node.Proc.InParams, node.Proc.OutParams, node.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());
- procNameToInfo[node.Proc.Name].dummyAsyncTargetProc = dummyAsyncTargetProc;
- }
}
if (node.InParallelWith != null)
{
@@ -110,21 +96,12 @@ namespace Microsoft.Boogie procNameToInfo[iter.Proc.Name] = new ProcedureInfo();
}
procNameToInfo[iter.Proc.Name].isThreadStart = true;
- CreateYieldCheckerProcedure(iter.Proc);
procNameToInfo[iter.Proc.Name].inParallelCall = true;
iter = iter.InParallelWith;
}
}
return base.VisitCallCmd(node);
}
- private void CreateYieldCheckerProcedure(Procedure proc)
- {
- if (procNameToInfo[proc.Name].yieldCheckerProc != null) return;
- var yieldCheckerName = string.Format("YieldChecker_{0}", proc.Name);
- var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, proc.TypeParameters, new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
- yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- procNameToInfo[proc.Name].yieldCheckerProc = yieldCheckerProc;
- }
}
class AtomicTraverser : StandardVisitor
@@ -169,7 +146,10 @@ namespace Microsoft.Boogie IdentifierExprSeq globalMods;
Hashtable ogOldGlobalMap;
Program program;
- Dictionary<string, Procedure> parallelCallDesugarings;
+ Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
+ List<Procedure> yieldCheckerProcs;
+ List<Implementation> yieldCheckerImpls;
+ Procedure yieldProc;
public OwickiGriesTransform(Program program)
{
@@ -180,24 +160,22 @@ namespace Microsoft.Boogie globalMods = new IdentifierExprSeq();
foreach (Variable g in program.GlobalVariables())
{
- var oldg = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og@global_old_{0}", g.Name), g.TypedIdent.Type));
+ var oldg = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type));
ogOldGlobalMap[g] = new IdentifierExpr(Token.NoToken, oldg);
globalMods.Add(new IdentifierExpr(Token.NoToken, g));
}
- parallelCallDesugarings = new Dictionary<string, Procedure>();
+ asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();
+ yieldCheckerProcs = new List<Procedure>();
+ yieldCheckerImpls = new List<Implementation>();
+ yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
}
- private void AddCallsToYieldCheckers(CmdSeq newCmds)
+ private void AddCallToYieldProc(CmdSeq newCmds)
{
- foreach (ProcedureInfo info in procNameToInfo.Values)
- {
- if (info.yieldCheckerProc != null)
- {
- CallCmd yieldCallCmd = new CallCmd(Token.NoToken, info.yieldCheckerProc.Name, new ExprSeq(), new IdentifierExprSeq());
- yieldCallCmd.Proc = info.yieldCheckerProc;
- newCmds.Add(yieldCallCmd);
- }
- }
+ CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, new ExprSeq(), new IdentifierExprSeq());
+ yieldCallCmd.Proc = yieldProc;
+ newCmds.Add(yieldCallCmd);
}
private void AddUpdatesToOldGlobalVars(CmdSeq newCmds)
@@ -214,7 +192,7 @@ namespace Microsoft.Boogie private void DesugarYield(CmdSeq cmds, CmdSeq newCmds)
{
- AddCallsToYieldCheckers(newCmds);
+ AddCallToYieldProc(newCmds);
newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
@@ -244,10 +222,10 @@ namespace Microsoft.Boogie string procName = "og";
foreach (string calleeName in parallelCalleeNames)
{
- procName = procName + "@" + calleeName;
+ procName = procName + "_" + calleeName;
}
- if (parallelCallDesugarings.ContainsKey(procName))
- return parallelCallDesugarings[procName];
+ if (asyncAndParallelCallDesugarings.ContainsKey(procName))
+ return asyncAndParallelCallDesugarings[procName];
VariableSeq inParams = new VariableSeq();
VariableSeq outParams = new VariableSeq();
@@ -260,13 +238,13 @@ namespace Microsoft.Boogie Hashtable map = new Hashtable();
foreach (Variable x in callCmd.Proc.InParams)
{
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og@" + count + x.Name, x.TypedIdent.Type), true);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true);
inParams.Add(y);
map[x] = new IdentifierExpr(Token.NoToken, y);
}
foreach (Variable x in callCmd.Proc.OutParams)
{
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og@" + count + x.Name, x.TypedIdent.Type), false);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false);
outParams.Add(y);
map[x] = new IdentifierExpr(Token.NoToken, y);
}
@@ -289,249 +267,342 @@ namespace Microsoft.Boogie }
Procedure proc = new Procedure(Token.NoToken, procName, new TypeVariableSeq(), inParams, outParams, requiresSeq, ieSeq, ensuresSeq);
- parallelCallDesugarings[procName] = proc;
+ asyncAndParallelCallDesugarings[procName] = proc;
return proc;
}
- public void Transform()
+ private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, VariableSeq locals, Hashtable map, Hashtable assumeMap, Hashtable ogOldLocalMap)
{
- foreach (var decl in program.TopLevelDeclarations)
- {
- Implementation impl = decl as Implementation;
- if (impl == null) continue;
- ProcedureInfo info = procNameToInfo[impl.Name];
-
- // Add free requires
- if (!info.isAtomic || info.isEntrypoint || info.isThreadStart)
- {
- Expr freeRequiresExpr = Expr.True;
- foreach (Variable g in ogOldGlobalMap.Keys)
- {
- freeRequiresExpr = Expr.And(freeRequiresExpr, Expr.Eq(new IdentifierExpr(Token.NoToken, g), (IdentifierExpr)ogOldGlobalMap[g]));
- }
- impl.Proc.Requires.Add(new Requires(true, freeRequiresExpr));
- }
+ if (yields.Count == 0) return;
- // Create substitution maps
- Hashtable map = new Hashtable();
- VariableSeq locals = new VariableSeq();
- for (int i = 0; i < impl.Proc.InParams.Length; i++)
- {
- Variable inParam = impl.Proc.InParams[i];
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
- var ie = new IdentifierExpr(Token.NoToken, copy);
- locals.Add(copy);
- // substitute for both implementation and procedure parameters because yield predicates can be generated
- // either by assertions in the implementation or preconditions and postconditions in the procedure
- map[impl.InParams[i]] = ie;
- map[impl.Proc.InParams[i]] = ie;
- }
- for (int i = 0; i < impl.Proc.OutParams.Length; i++)
- {
- Variable outParam = impl.Proc.OutParams[i];
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);
- var ie = new IdentifierExpr(Token.NoToken, copy);
- locals.Add(copy);
- // substitute for both implementation and procedure parameters because yield predicates can be generated
- // either by assertions in the implementation or preconditions and postconditions in the procedure
- map[impl.OutParams[i]] = ie;
- map[impl.Proc.OutParams[i]] = ie;
- }
- foreach (Variable local in impl.LocVars)
+ ProcedureInfo info = procNameToInfo[decl.Name];
+ Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ List<Block> yieldCheckerBlocks = new List<Block>();
+ StringSeq labels = new StringSeq();
+ BlockSeq labelTargets = new BlockSeq();
+ Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ labels.Add(yieldCheckerBlock.Label);
+ labelTargets.Add(yieldCheckerBlock);
+ yieldCheckerBlocks.Add(yieldCheckerBlock);
+ int yieldCount = 0;
+ foreach (CmdSeq cs in yields)
+ {
+ CmdSeq newCmds = new CmdSeq();
+ foreach (Cmd cmd in cs)
{
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type), local.Attributes);
- locals.Add(copy);
- map[local] = new IdentifierExpr(Token.NoToken, copy);
+ PredicateCmd predCmd = (PredicateCmd)cmd;
+ newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
}
- Hashtable assumeMap = new Hashtable(map);
- foreach (var global in ogOldGlobalMap.Keys)
+ foreach (Cmd cmd in cs)
{
- assumeMap[global] = ogOldGlobalMap[global];
+ PredicateCmd predCmd = (PredicateCmd)cmd;
+ var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
+ if (predCmd is AssertCmd)
+ newCmds.Add(new AssertCmd(predCmd.tok, newExpr));
+ else
+ newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
}
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
+ yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
+ labels.Add(yieldCheckerBlock.Label);
+ labelTargets.Add(yieldCheckerBlock);
+ yieldCheckerBlocks.Add(yieldCheckerBlock);
+ }
+ yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets)));
- Hashtable ogOldLocalMap = new Hashtable();
- foreach (var g in program.GlobalVariables())
+ // Create the yield checker procedure
+ var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);
+ var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ yieldCheckerProcs.Add(yieldCheckerProc);
+
+ // Create the yield checker implementation
+ var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);
+ yieldCheckerImpl.Proc = yieldCheckerProc;
+ yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ yieldCheckerImpls.Add(yieldCheckerImpl);
+ }
+
+ private void TransformImpl(Implementation impl)
+ {
+ ProcedureInfo info = procNameToInfo[impl.Name];
+
+ // Add free requires
+ if (!info.isAtomic || info.isEntrypoint || info.isThreadStart)
+ {
+ Expr freeRequiresExpr = Expr.True;
+ foreach (Variable g in ogOldGlobalMap.Keys)
{
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og@local_old_{0}", g.Name), g.TypedIdent.Type));
- locals.Add(copy);
- ogOldLocalMap[g] = new IdentifierExpr(Token.NoToken, copy);
+ freeRequiresExpr = Expr.And(freeRequiresExpr, Expr.Eq(new IdentifierExpr(Token.NoToken, g), (IdentifierExpr)ogOldGlobalMap[g]));
}
+ impl.Proc.Requires.Add(new Requires(true, freeRequiresExpr));
+ }
+
+ // Create substitution maps
+ Hashtable map = new Hashtable();
+ VariableSeq locals = new VariableSeq();
+ for (int i = 0; i < impl.Proc.InParams.Length; i++)
+ {
+ Variable inParam = impl.Proc.InParams[i];
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
+ var ie = new IdentifierExpr(Token.NoToken, copy);
+ locals.Add(copy);
+ map[impl.InParams[i]] = ie;
+ }
+ for (int i = 0; i < impl.Proc.OutParams.Length; i++)
+ {
+ Variable outParam = impl.Proc.OutParams[i];
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);
+ var ie = new IdentifierExpr(Token.NoToken, copy);
+ locals.Add(copy);
+ map[impl.OutParams[i]] = ie;
+ }
+ foreach (Variable local in impl.LocVars)
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type), local.Attributes);
+ locals.Add(copy);
+ map[local] = new IdentifierExpr(Token.NoToken, copy);
+ }
+ Hashtable assumeMap = new Hashtable(map);
+ foreach (var global in ogOldGlobalMap.Keys)
+ {
+ assumeMap[global] = ogOldGlobalMap[global];
+ }
- // Collect the yield predicates and desugar yields
- HashSet<CmdSeq> yields = new HashSet<CmdSeq>();
- CmdSeq cmds = new CmdSeq();
- if (info.isThreadStart && impl.Proc.Requires.Length > 0)
+ Hashtable ogOldLocalMap = new Hashtable();
+ foreach (var g in program.GlobalVariables())
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));
+ locals.Add(copy);
+ ogOldLocalMap[g] = new IdentifierExpr(Token.NoToken, copy);
+ }
+
+ // Collect the yield predicates and desugar yields
+ List<CmdSeq> yields = new List<CmdSeq>();
+ CmdSeq cmds = new CmdSeq();
+ foreach (Block b in impl.Blocks)
+ {
+ bool insideYield = false;
+ CmdSeq newCmds = new CmdSeq();
+ for (int i = 0; i < b.Cmds.Length; i++)
{
- foreach (Requires r in impl.Proc.Requires)
+ Cmd cmd = b.Cmds[i];
+ if (cmd is YieldCmd)
{
- if (r.Free) continue;
- cmds.Add(new AssertCmd(r.tok, r.Condition));
+ insideYield = true;
+ continue;
}
- yields.Add(cmds);
- cmds = new CmdSeq();
- }
- if (info.inParallelCall && impl.Proc.Ensures.Length > 0)
- {
- foreach (Ensures e in impl.Proc.Ensures)
+ if (insideYield)
{
- if (e.Free) continue;
- cmds.Add(new AssertCmd(e.tok, e.Condition));
+ PredicateCmd pcmd = cmd as PredicateCmd;
+ if (pcmd == null)
+ {
+ DesugarYield(cmds, newCmds);
+ if (cmds.Length > 0)
+ {
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
+ insideYield = false;
+ }
+ else
+ {
+ cmds.Add(pcmd);
+ }
}
- yields.Add(cmds);
- cmds = new CmdSeq();
- }
- foreach (Block b in impl.Blocks)
- {
- bool insideYield = false;
- CmdSeq newCmds = new CmdSeq();
- for (int i = 0; i < b.Cmds.Length; i++)
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd != null)
{
- Cmd cmd = b.Cmds[i];
- if (cmd is YieldCmd)
+ if (callCmd.InParallelWith != null)
{
- insideYield = true;
- continue;
+ List<Expr> ins;
+ List<IdentifierExpr> outs;
+ Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs);
+ CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs);
+ dummyCallCmd.Proc = dummyParallelCallDesugaring;
+ newCmds.Add(dummyCallCmd);
}
- if (insideYield)
+ else if (callCmd.IsAsync)
{
- PredicateCmd pcmd = cmd as PredicateCmd;
- if (pcmd == null)
- {
- DesugarYield(cmds, newCmds);
- if (cmds.Length > 0)
- {
- yields.Add(cmds);
- cmds = new CmdSeq();
- }
- insideYield = false;
- }
- else
+ if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
{
- cmds.Add(pcmd);
+ asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());
}
+ var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
+ CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
+ dummyCallCmd.Proc = dummyAsyncTargetProc;
+ newCmds.Add(dummyCallCmd);
}
- CallCmd callCmd = cmd as CallCmd;
- if (callCmd != null)
+ else if (procNameToInfo[callCmd.callee].isAtomic)
{
- if (callCmd.InParallelWith != null)
- {
- List<Expr> ins;
- List<IdentifierExpr> outs;
- Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs);
- CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs);
- dummyCallCmd.Proc = dummyParallelCallDesugaring;
- newCmds.Add(dummyCallCmd);
- }
- else if (callCmd.IsAsync)
- {
- var dummyAsyncTargetProc = procNameToInfo[callCmd.callee].dummyAsyncTargetProc;
- CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
- dummyCallCmd.Proc = dummyAsyncTargetProc;
- newCmds.Add(dummyCallCmd);
- }
- else if (procNameToInfo[callCmd.callee].isAtomic)
- {
- newCmds.Add(callCmd);
- }
- else
- {
- AddCallsToYieldCheckers(newCmds);
- newCmds.Add(callCmd);
- AddUpdatesToOldGlobalVars(newCmds);
- }
+ newCmds.Add(callCmd);
}
else
{
- newCmds.Add(cmd);
+ AddCallToYieldProc(newCmds);
+ newCmds.Add(callCmd);
+ AddUpdatesToOldGlobalVars(newCmds);
}
}
- if (insideYield)
+ else
{
- DesugarYield(cmds, newCmds);
- if (cmds.Length > 0)
- {
- yields.Add(cmds);
- cmds = new CmdSeq();
- }
- }
- if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))
+ newCmds.Add(cmd);
+ }
+ }
+ if (insideYield)
+ {
+ DesugarYield(cmds, newCmds);
+ if (cmds.Length > 0)
{
- AddCallsToYieldCheckers(newCmds);
+ yields.Add(cmds);
+ cmds = new CmdSeq();
}
- b.Cmds = newCmds;
}
+ if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))
+ {
+ AddCallToYieldProc(newCmds);
+ }
+ b.Cmds = newCmds;
+ }
- if (!info.isAtomic)
+ if (!info.isAtomic)
+ {
+ // Loops
+ impl.PruneUnreachableBlocks();
+ impl.ComputePredecessorsForBlocks();
+ GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);
+ g.ComputeLoops();
+ if (g.Reducible)
{
- // Loops
- impl.PruneUnreachableBlocks();
- impl.ComputePredecessorsForBlocks();
- GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);
- g.ComputeLoops();
- if (g.Reducible)
+ foreach (Block header in g.Headers)
{
- foreach (Block header in g.Headers)
+ foreach (Block pred in header.Predecessors)
{
- foreach (Block pred in header.Predecessors)
- {
- AddCallsToYieldCheckers(pred.Cmds);
- AddUpdatesToOldGlobalVars(pred.Cmds);
- }
- CmdSeq newCmds = new CmdSeq();
- foreach (Variable v in ogOldGlobalMap.Keys)
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), (IdentifierExpr)ogOldGlobalMap[v])));
- }
- newCmds.AddRange(header.Cmds);
- header.Cmds = newCmds;
+ AddCallToYieldProc(pred.Cmds);
+ AddUpdatesToOldGlobalVars(pred.Cmds);
}
+ CmdSeq newCmds = new CmdSeq();
+ foreach (Variable v in ogOldGlobalMap.Keys)
+ {
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), (IdentifierExpr)ogOldGlobalMap[v])));
+ }
+ newCmds.AddRange(header.Cmds);
+ header.Cmds = newCmds;
}
}
+ }
+ CreateYieldCheckerImpl(impl, yields, locals, map, assumeMap, ogOldLocalMap);
+ }
- if (!info.containsYield && !info.isThreadStart) continue;
+ public void TransformProc(Procedure proc)
+ {
+ ProcedureInfo info = procNameToInfo[proc.Name];
+ if (!info.isThreadStart) return;
- // Create the body of the yield checker procedure
- Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
- Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- List<Block> yieldCheckerBlocks = new List<Block>();
- StringSeq labels = new StringSeq();
- BlockSeq labelTargets = new BlockSeq();
- Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- int yieldCount = 0;
- foreach (CmdSeq cs in yields)
+ // Create substitution maps
+ Hashtable map = new Hashtable();
+ VariableSeq locals = new VariableSeq();
+ for (int i = 0; i < proc.InParams.Length; i++)
+ {
+ Variable inParam = proc.InParams[i];
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
+ var ie = new IdentifierExpr(Token.NoToken, copy);
+ locals.Add(copy);
+ map[proc.InParams[i]] = ie;
+ }
+ for (int i = 0; i < proc.OutParams.Length; i++)
+ {
+ Variable outParam = proc.OutParams[i];
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);
+ var ie = new IdentifierExpr(Token.NoToken, copy);
+ locals.Add(copy);
+ map[proc.OutParams[i]] = ie;
+ }
+ Hashtable assumeMap = new Hashtable(map);
+ foreach (var global in ogOldGlobalMap.Keys)
+ {
+ assumeMap[global] = ogOldGlobalMap[global];
+ }
+
+ Hashtable ogOldLocalMap = new Hashtable();
+ foreach (var g in program.GlobalVariables())
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));
+ locals.Add(copy);
+ ogOldLocalMap[g] = new IdentifierExpr(Token.NoToken, copy);
+ }
+
+ // Collect the yield predicates and desugar yields
+ List<CmdSeq> yields = new List<CmdSeq>();
+ CmdSeq cmds = new CmdSeq();
+ if (proc.Requires.Length > 0)
+ {
+ foreach (Requires r in proc.Requires)
{
- CmdSeq newCmds = new CmdSeq();
- foreach (Cmd cmd in cs)
- {
- PredicateCmd predCmd = (PredicateCmd)cmd;
- newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
- }
- foreach (Cmd cmd in cs)
- {
- PredicateCmd predCmd = (PredicateCmd)cmd;
- var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
- if (predCmd is AssertCmd)
- newCmds.Add(new AssertCmd(predCmd.tok, newExpr));
- else
- newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
- }
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
- yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
+ if (r.Free) continue;
+ cmds.Add(new AssertCmd(r.tok, r.Condition));
+ }
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
+ if (info.inParallelCall && proc.Ensures.Length > 0)
+ {
+ foreach (Ensures e in proc.Ensures)
+ {
+ if (e.Free) continue;
+ cmds.Add(new AssertCmd(e.tok, e.Condition));
+ }
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
+ CreateYieldCheckerImpl(proc, yields, locals, map, assumeMap, ogOldLocalMap);
+ }
+
+ private void AddYieldProcAndImpl()
+ {
+ List<Block> blocks = new List<Block>();
+ TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
+ if (yieldCheckerProcs.Count > 0)
+ {
+ BlockSeq blockTargets = new BlockSeq();
+ StringSeq labelTargets = new StringSeq();
+ int labelCount = 0;
+ foreach (Procedure proc in yieldCheckerProcs)
+ {
+ CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, new ExprSeq(), new IdentifierExprSeq());
+ callCmd.Proc = proc;
+ string label = string.Format("L_{0}", labelCount++);
+ Block block = new Block(Token.NoToken, label, new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));
+ labelTargets.Add(label);
+ blockTargets.Add(block);
+ blocks.Add(block);
}
- yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets)));
-
- // Create the yield checker implementation
- var yieldCheckerImpl = new Implementation(Token.NoToken, info.yieldCheckerProc.Name, impl.TypeParameters, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);
- yieldCheckerImpl.Proc = info.yieldCheckerProc;
- yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- info.yieldCheckerImpl = yieldCheckerImpl;
+ transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);
+ }
+ blocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), transferCmd));
+ var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), blocks);
+ yieldImpl.Proc = yieldProc;
+ yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ program.TopLevelDeclarations.Add(yieldProc);
+ program.TopLevelDeclarations.Add(yieldImpl);
+ }
+
+ public void Transform()
+ {
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ TransformProc(proc);
+ }
+
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ TransformImpl(impl);
}
foreach (Variable v in ogOldGlobalMap.Keys)
@@ -539,19 +610,20 @@ namespace Microsoft.Boogie IdentifierExpr ie = (IdentifierExpr) ogOldGlobalMap[v];
program.TopLevelDeclarations.Add(ie.Decl);
}
- foreach (ProcedureInfo info in procNameToInfo.Values)
+ foreach (Procedure proc in yieldCheckerProcs)
{
- if (info.yieldCheckerProc != null)
- {
- Debug.Assert(info.yieldCheckerImpl != null);
- program.TopLevelDeclarations.Add(info.yieldCheckerProc);
- program.TopLevelDeclarations.Add(info.yieldCheckerImpl);
- }
- if (info.dummyAsyncTargetProc != null)
- {
- program.TopLevelDeclarations.Add(info.dummyAsyncTargetProc);
- }
+ program.TopLevelDeclarations.Add(proc);
+ }
+ foreach (Implementation impl in yieldCheckerImpls)
+ {
+ program.TopLevelDeclarations.Add(impl);
+ }
+ foreach (Procedure proc in asyncAndParallelCallDesugarings.Values)
+ {
+ program.TopLevelDeclarations.Add(proc);
}
+ AddYieldProcAndImpl();
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
}
}
}
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 98667bec..a730ec8f 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -13,6 +13,1121 @@ using Microsoft.Boogie.GraphUtil; namespace Microsoft.Boogie.Houdini {
+ public class AbsHoudini
+ {
+ // An element of the abstract domain
+ IAbstractDomain domainElement;
+ Dictionary<string, Function> existentialFunctions;
+ Program program;
+ Dictionary<string, Implementation> name2Impl;
+ Dictionary<string, VCExpr> impl2VC;
+ Dictionary<string, List<Tuple<string, Constant, NAryExpr>>> impl2FuncCalls;
+ // constant -> the naryexpr that it replaced
+ Dictionary<string, NAryExpr> constant2FuncCall;
+
+ // function -> its abstract value
+ Dictionary<string, IAbstractDomain> function2Value;
+
+ // impl -> functions assumed/asserted
+ Dictionary<string, HashSet<string>> impl2functionsAsserted, impl2functionsAssumed;
+
+ // funtions -> impls where assumed/asserted
+ Dictionary<string, HashSet<string>> function2implAssumed, function2implAsserted;
+
+ // impl -> handler, collector
+ Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>> impl2ErrorHandler;
+
+ // Essentials: VCGen, Prover
+ VCGen vcgen;
+ ProverInterface prover;
+
+ // Stats
+ TimeSpan proverTime;
+ int numProverQueries;
+
+ public AbsHoudini(Program program, IAbstractDomain elem)
+ {
+ this.program = program;
+ this.domainElement = elem;
+ this.impl2VC = new Dictionary<string, VCExpr>();
+ this.impl2FuncCalls = new Dictionary<string, List<Tuple<string, Constant, NAryExpr>>>();
+ this.existentialFunctions = new Dictionary<string, Function>();
+ this.name2Impl = new Dictionary<string, Implementation>();
+ this.impl2functionsAsserted = new Dictionary<string, HashSet<string>>();
+ this.impl2functionsAssumed = new Dictionary<string, HashSet<string>>();
+ this.function2implAsserted = new Dictionary<string, HashSet<string>>();
+ this.function2implAssumed = new Dictionary<string, HashSet<string>>();
+ this.impl2ErrorHandler = new Dictionary<string, Tuple<ProverInterface.ErrorHandler, AbsHoudiniCounterexampleCollector>>();
+ this.constant2FuncCall = new Dictionary<string, NAryExpr>();
+
+ // Find the existential functions
+ foreach (var func in program.TopLevelDeclarations.OfType<Function>()
+ .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential")))
+ existentialFunctions.Add(func.Name, func);
+
+ this.function2Value = new Dictionary<string, IAbstractDomain>();
+ existentialFunctions.Keys.Iter(f => function2Value.Add(f, domainElement.Bottom()));
+ existentialFunctions.Keys.Iter(f => function2implAssumed.Add(f, new HashSet<string>()));
+ existentialFunctions.Keys.Iter(f => function2implAsserted.Add(f, new HashSet<string>()));
+
+ // type check
+ existentialFunctions.Values.Iter(func =>
+ {
+ if (func.OutParams.Length != 1 || !func.OutParams[0].TypedIdent.Type.IsBool)
+ throw new AbsHoudiniInternalError(string.Format("Existential function {0} must return bool", func.Name));
+ if(func.Body != null)
+ throw new AbsHoudiniInternalError(string.Format("Existential function {0} should not have a body", func.Name));
+ });
+
+ //if (CommandLineOptions.Clo.ProverKillTime > 0)
+ // CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
+
+ Inline();
+
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
+
+ this.proverTime = TimeSpan.Zero;
+ this.numProverQueries = 0;
+
+ program.TopLevelDeclarations.OfType<Implementation>()
+ .Where(impl => !impl.SkipVerification)
+ .Iter(impl => name2Impl.Add(impl.Name, impl));
+
+ // Let's do VC Gen (and also build dependencies)
+ name2Impl.Values.Iter(GenVC);
+ }
+
+ public void ComputeSummaries()
+ {
+ // Compute SCCs and determine a priority order for impls
+ var Succ = new Dictionary<string, HashSet<string>>();
+ var Pred = new Dictionary<string, HashSet<string>>();
+ name2Impl.Keys.Iter(s => Succ[s] = new HashSet<string>());
+ name2Impl.Keys.Iter(s => Pred[s] = new HashSet<string>());
+
+ foreach(var impl in name2Impl.Keys) {
+ Succ[impl] = new HashSet<string>();
+ impl2functionsAsserted[impl].Iter(f =>
+ function2implAssumed[f].Iter(succ =>
+ {
+ Succ[impl].Add(succ);
+ Pred[succ].Add(impl);
+ }));
+ }
+
+ var sccs = new StronglyConnectedComponents<string>(name2Impl.Keys,
+ new Adjacency<string>(n => Pred[n]),
+ new Adjacency<string>(n => Succ[n]));
+ sccs.Compute();
+
+ // impl -> priority
+ var impl2Priority = new Dictionary<string, int>();
+ int p = 0;
+ foreach (var scc in sccs)
+ {
+ foreach (var impl in scc)
+ {
+ impl2Priority.Add(impl, p);
+ p++;
+ }
+ }
+
+ var worklist = new SortedSet<Tuple<int, string>>();
+ name2Impl.Keys.Iter(k => worklist.Add(Tuple.Create(impl2Priority[k], k)));
+
+ while (worklist.Any())
+ {
+ var impl = worklist.First().Item2;
+ worklist.Remove(worklist.First());
+
+ var gen = prover.VCExprGen;
+ Expr env = Expr.True;
+
+ foreach (var tup in impl2FuncCalls[impl])
+ {
+ var controlVar = tup.Item2;
+ var exprVars = tup.Item3;
+ var varList = new List<Expr>();
+ exprVars.Args.OfType<Expr>().Iter(v => varList.Add(v));
+
+ env = Expr.And(env,
+ Expr.Eq(Expr.Ident(controlVar), function2Value[tup.Item1].Gamma(varList)));
+ }
+
+ env.Typecheck(new TypecheckingContext((IErrorSink)null));
+ var envVC = prover.Context.BoogieExprTranslator.Translate(env);
+
+ var vc = gen.Implies(envVC, impl2VC[impl]);
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Verifying {0}: ", impl);
+ //Console.WriteLine("env: {0}", envVC);
+ var envFuncs = new HashSet<string>();
+ impl2FuncCalls[impl].Iter(tup => envFuncs.Add(tup.Item1));
+ envFuncs.Iter(f => PrintFunction(existentialFunctions[f]));
+ }
+
+ var handler = impl2ErrorHandler[impl].Item1;
+ var collector = impl2ErrorHandler[impl].Item2;
+ collector.Reset(impl);
+
+ var start = DateTime.Now;
+
+ prover.Push();
+ prover.Assert(gen.Not(vc), true);
+ prover.FlushAxiomsToTheoremProver();
+ prover.Check();
+ ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);
+
+ //prover.BeginCheck(impl, vc, handler);
+ //ProverInterface.Outcome proverOutcome = prover.CheckOutcomeCore(handler);
+
+ var inc = (DateTime.Now - start);
+ proverTime += inc;
+ numProverQueries++;
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Time taken = " + inc.TotalSeconds.ToString());
+
+ if (proverOutcome == ProverInterface.Outcome.TimeOut || proverOutcome == ProverInterface.Outcome.OutOfMemory)
+ throw new AbsHoudiniInternalError("Timeout/Spaceout while verifying " + impl);
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine(collector.numErrors > 0 ? "SAT" : "UNSAT");
+
+ if (collector.numErrors > 0)
+ {
+ var funcsChanged = collector.funcsChanged;
+
+ // propagate dependent guys back into the worklist, including self
+ var deps = new HashSet<string>();
+ deps.Add(impl);
+ funcsChanged.Iter(f => deps.UnionWith(function2implAssumed[f]));
+
+ deps.Iter(s => worklist.Add(Tuple.Create(impl2Priority[s], s)));
+ }
+
+ prover.Pop();
+ }
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Prover time = {0}", proverTime.TotalSeconds.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + numProverQueries);
+ }
+
+ if (CommandLineOptions.Clo.PrintAssignment)
+ {
+ // Print the answer
+ existentialFunctions.Values.Iter(PrintFunction);
+ }
+ }
+
+ private void PrintFunction(Function function)
+ {
+ var tt = new TokenTextWriter(Console.Out);
+ var invars = new List<Expr>(function.InParams.OfType<Variable>().Select(v => Expr.Ident(v)));
+ function.Body = function2Value[function.Name].Gamma(invars);
+ function.Emit(tt, 0);
+ tt.Close();
+ }
+
+ public HashSet<string> HandleCounterExample(string impl, Counterexample error)
+ {
+ var funcsChanged = new HashSet<string>();
+ // Find the failing assert -- need to do a join there
+ // return the set of functions whose definition has changed
+ var cex = ExtractState(impl, error);
+ foreach (var tup in cex)
+ {
+ function2Value[tup.Item1] = function2Value[tup.Item1].Join(tup.Item2);
+ funcsChanged.Add(tup.Item1);
+ }
+ return funcsChanged;
+ }
+
+ private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Counterexample error)
+ {
+ var lastBlock = error.Trace.Last() as Block;
+ AssertCmd failingAssert = null;
+
+ CallCounterexample callCounterexample = error as CallCounterexample;
+ if (callCounterexample != null)
+ {
+ Procedure failingProcedure = callCounterexample.FailingCall.Proc;
+ Requires failingRequires = callCounterexample.FailingRequires;
+ failingAssert = lastBlock.Cmds.OfType<AssertRequiresCmd>().FirstOrDefault(ac => ac.Requires == failingRequires);
+ }
+ ReturnCounterexample returnCounterexample = error as ReturnCounterexample;
+ if (returnCounterexample != null)
+ {
+ Ensures failingEnsures = returnCounterexample.FailingEnsures;
+ failingAssert = lastBlock.Cmds.OfType<AssertEnsuresCmd>().FirstOrDefault(ac => ac.Ensures == failingEnsures);
+ }
+ AssertCounterexample assertCounterexample = error as AssertCounterexample;
+ if (assertCounterexample != null)
+ {
+ failingAssert = lastBlock.Cmds.OfType<AssertCmd>().FirstOrDefault(ac => ac == assertCounterexample.FailingAssert);
+ }
+
+ Debug.Assert(failingAssert != null);
+ return ExtractState(impl, failingAssert.Expr, error.Model);
+ }
+
+ private List<Tuple<string, List<Model.Element>>> ExtractState(string impl, Expr expr, Model model)
+ {
+ var collect = new VariableCollector();
+ collect.VisitExpr(expr);
+
+ var ret = new List<Tuple<string, List<Model.Element>>>();
+
+ foreach (var constant in collect.usedVars.OfType<Constant>().Where(c => constant2FuncCall.ContainsKey(c.Name)))
+ {
+ var func = constant2FuncCall[constant.Name];
+ var funcName = (func.Fun as FunctionCall).FunctionName;
+ var vals = new List<Model.Element>();
+ prover.Context.BoogieExprTranslator.Translate(func.Args).Iter(ve => vals.Add(getValue(ve, model)));
+
+ ret.Add(Tuple.Create(funcName, vals));
+ }
+
+ return ret;
+ }
+
+ private Model.Element getValue(VCExpr arg, Model model)
+ {
+
+ if (arg is VCExprLiteral)
+ {
+ //return model.GetElement(arg.ToString());
+ return model.MkElement(arg.ToString());
+ }
+ else if (arg is VCExprVar)
+ {
+ var el = model.TryGetFunc(prover.Context.Lookup(arg as VCExprVar));
+ if (el != null)
+ {
+ Debug.Assert(el.Arity == 0 && el.AppCount == 1);
+ return el.Apps.First().Result;
+ }
+ else
+ {
+ // Variable not defined; assign arbitrary value
+ if (arg.Type.IsBool)
+ return model.MkElement("false");
+ else if (arg.Type.IsInt)
+ return model.MkIntElement(0);
+ else
+ return null;
+ }
+ }
+ else
+ {
+ var val = prover.Evaluate(arg);
+ if (val is int || val is bool || val is Microsoft.Basetypes.BigNum)
+ {
+ return model.MkElement(val.ToString());
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ return null;
+ }
+ }
+
+ class AbsHoudiniCounterexampleCollector : VerifierCallback
+ {
+ public HashSet<string> funcsChanged;
+ public string currImpl;
+ public int numErrors;
+
+ AbsHoudini container;
+
+ public AbsHoudiniCounterexampleCollector(AbsHoudini container)
+ {
+ this.container = container;
+ Reset(null);
+ }
+
+ public void Reset(string impl)
+ {
+ funcsChanged = new HashSet<string>();
+ currImpl = impl;
+ numErrors = 0;
+ }
+
+ public override void OnCounterexample(Counterexample ce, string reason)
+ {
+ numErrors++;
+
+ funcsChanged.UnionWith(
+ container.HandleCounterExample(currImpl, ce));
+ }
+ }
+
+ private void GenVC(Implementation impl)
+ {
+ ModelViewInfo mvInfo;
+ System.Collections.Hashtable label2absy;
+ var collector = new AbsHoudiniCounterexampleCollector(this);
+ collector.OnProgress("HdnVCGen", 0, 0, 0.0);
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Generating VC of {0}", impl.Name);
+ }
+
+ vcgen.ConvertCFG2DAG(impl);
+ var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
+
+ //CommandLineOptions.Clo.PrintInstrumented = true;
+ //var tt = new TokenTextWriter(Console.Out);
+ //impl.Emit(tt, 0);
+ //tt.Close();
+
+ // Intercept the FunctionCalls of the existential functions, and replace them with Boolean constants
+ var existentialFunctionNames = new HashSet<string>(existentialFunctions.Keys);
+ var fv = new ReplaceFunctionCalls(existentialFunctionNames);
+ fv.VisitBlockList(impl.Blocks);
+
+ impl2functionsAsserted.Add(impl.Name, fv.functionsAsserted);
+ impl2functionsAssumed.Add(impl.Name, fv.functionsAssumed);
+
+ fv.functionsAssumed.Iter(f => function2implAssumed[f].Add(impl.Name));
+ fv.functionsAsserted.Iter(f => function2implAsserted[f].Add(impl.Name));
+
+ impl2FuncCalls.Add(impl.Name, fv.functionsUsed);
+ fv.functionsUsed.Iter(tup => constant2FuncCall.Add(tup.Item2.Name, tup.Item3));
+
+ var gen = prover.VCExprGen;
+ VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : gen.Integer(Microsoft.Basetypes.BigNum.ZERO);
+
+ var vcexpr = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, prover.Context);
+ if (!CommandLineOptions.Clo.UseLabels)
+ {
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(Microsoft.Basetypes.BigNum.ZERO), gen.Integer(Microsoft.Basetypes.BigNum.ZERO));
+ VCExpr eqExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(Microsoft.Basetypes.BigNum.FromInt(impl.Blocks[0].UniqueId)));
+ vcexpr = gen.Implies(eqExpr, vcexpr);
+ }
+
+ ProverInterface.ErrorHandler handler = null;
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
+ handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);
+ else
+ handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, prover.Context, program);
+
+ impl2ErrorHandler.Add(impl.Name, Tuple.Create(handler, collector));
+
+ //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr);
+
+ // Create a macro so that the VC can sit with the theorem prover
+ Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));
+ prover.DefineMacro(macro, vcexpr);
+
+ // Store VC
+ impl2VC.Add(impl.Name, gen.Function(macro));
+
+ // HACK: push the definitions of constants involved in function calls
+ // It is possible that some constants only appear in function calls. Thus, when
+ // they are replaced by Boolean constants, it is possible that (get-value) will
+ // fail if the expression involves such constants. All we need to do is make sure
+ // these constants are declared, because otherwise, semantically we are doing
+ // the right thing.
+ foreach (var tup in fv.functionsUsed)
+ {
+ var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);
+ tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);
+ prover.Assert(tt, true);
+ }
+ }
+
+ private void Inline()
+ {
+ if (CommandLineOptions.Clo.InlineDepth < 0)
+ return;
+
+ var callGraph = BuildCallGraph();
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
+ inlineRequiresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
+ freeRequiresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
+ inlineEnsuresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining;
+ CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec;
+ Inliner.ProcessImplementationForHoudini(program, impl);
+ CommandLineOptions.Clo.ProcedureInlining = savedOption;
+ }
+ foreach (Implementation impl in callGraph.Nodes)
+ {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+
+ Graph<Implementation> oldCallGraph = callGraph;
+ callGraph = new Graph<Implementation>();
+ foreach (Implementation impl in oldCallGraph.Nodes)
+ {
+ callGraph.AddSource(impl);
+ }
+ foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges)
+ {
+ callGraph.AddEdge(edge.Item1, edge.Item2);
+ }
+ int count = CommandLineOptions.Clo.InlineDepth;
+ while (count > 0)
+ {
+ foreach (Implementation impl in oldCallGraph.Nodes)
+ {
+ List<Implementation> newNodes = new List<Implementation>();
+ foreach (Implementation succ in callGraph.Successors(impl))
+ {
+ newNodes.AddRange(oldCallGraph.Successors(succ));
+ }
+ foreach (Implementation newNode in newNodes)
+ {
+ callGraph.AddEdge(impl, newNode);
+ }
+ }
+ count--;
+ }
+ }
+
+ private Graph<Implementation> BuildCallGraph()
+ {
+ Graph<Implementation> callGraph = new Graph<Implementation>();
+ Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ procToImpls[proc] = new HashSet<Implementation>();
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null || impl.SkipVerification) continue;
+ callGraph.AddSource(impl);
+ procToImpls[impl.Proc].Add(impl);
+ }
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null || impl.SkipVerification) continue;
+ foreach (Block b in impl.Blocks)
+ {
+ foreach (Cmd c in b.Cmds)
+ {
+ CallCmd cc = c as CallCmd;
+ if (cc == null) continue;
+ foreach (Implementation callee in procToImpls[cc.Proc])
+ {
+ callGraph.AddEdge(impl, callee);
+ }
+ }
+ }
+ }
+ return callGraph;
+ }
+
+ }
+
+ class ReplaceFunctionCalls : StandardVisitor
+ {
+ public List<Tuple<string, Constant, NAryExpr>> functionsUsed;
+ public List<Constant> boolConstants;
+
+ public HashSet<string> functionsAssumed;
+ public HashSet<string> functionsAsserted;
+ HashSet<string> functionsToReplace;
+
+ private bool inAssume;
+ private bool inAssert;
+ private static int IdCounter = 0;
+
+ public ReplaceFunctionCalls(HashSet<string> functionsToReplace)
+ {
+ this.functionsUsed = new List<Tuple<string, Constant, NAryExpr>>();
+ this.functionsToReplace = functionsToReplace;
+ this.functionsAsserted = new HashSet<string>();
+ this.functionsAssumed = new HashSet<string>();
+ this.boolConstants = new List<Constant>();
+
+ inAssume = false;
+ inAssert = false;
+ }
+
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ inAssert = true;
+ var ret = base.VisitAssertCmd(node);
+ inAssert = false;
+ return ret;
+ }
+
+ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)
+ {
+ return this.VisitAssertCmd(node);
+ }
+
+ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)
+ {
+ return this.VisitAssertCmd(node);
+ }
+
+ public override Cmd VisitAssumeCmd(AssumeCmd node)
+ {
+ inAssume = true;
+ var ret = base.VisitAssumeCmd(node);
+ inAssume = false;
+ return ret;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (node.Fun is FunctionCall && functionsToReplace.Contains((node.Fun as FunctionCall).FunctionName))
+ {
+ found((node.Fun as FunctionCall).FunctionName);
+ // create boolean constant to replace this guy
+ var constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "AbsHoudiniConstant" + IdCounter, Microsoft.Boogie.Type.Bool), false);
+ IdCounter++;
+
+ functionsUsed.Add(Tuple.Create((node.Fun as FunctionCall).FunctionName, constant, node));
+ boolConstants.Add(constant);
+ return Expr.Ident(constant);
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+ private void found(string func)
+ {
+ if (inAssume) functionsAssumed.Add(func);
+ if (inAssert) functionsAsserted.Add(func);
+ }
+
+ }
+
+ public class Intervals : IAbstractDomain
+ {
+ // [lower, upper]
+ int upper;
+ int lower;
+ // or: \bot
+ bool isBottom;
+ // number of times join has been performed
+ int nJoin;
+ // number of times before we widen
+ readonly static int maxJoin = 5;
+
+ public Intervals()
+ {
+ this.upper = 0;
+ this.lower = 0;
+ this.nJoin = 0;
+ this.isBottom = true;
+ }
+
+ private Intervals(int lower, int upper, int nJoin)
+ {
+ this.upper = upper;
+ this.lower = lower;
+ this.nJoin = nJoin;
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return new Intervals();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> states)
+ {
+ Debug.Assert(states.Count == 1);
+ var state = states[0] as Model.Integer;
+ if (state == null)
+ throw new AbsHoudiniInternalError("Incorrect type, expected int");
+ var intval = state.AsInt();
+
+ if (isBottom)
+ {
+ return new Intervals(intval, intval, 1);
+ }
+
+ if(intval >= lower && intval <= upper)
+ return this;
+
+ if (nJoin > maxJoin)
+ {
+ // widen
+ if (intval > upper)
+ return new Intervals(lower, Int32.MaxValue, 1);
+ if(intval < lower)
+ return new Intervals(Int32.MinValue, upper, 1);
+
+ Debug.Assert(false);
+ }
+
+ if (intval > upper)
+ return new Intervals(lower, intval, nJoin + 1);
+ if (intval < lower)
+ return new Intervals(intval, upper, nJoin + 1);
+
+ Debug.Assert(false);
+ return null;
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ Debug.Assert(vars.Count == 1);
+ var v = vars[0];
+ if (isBottom) return Expr.False;
+ Expr ret = Expr.True;
+ if (lower != Int32.MinValue)
+ ret = Expr.And(ret, Expr.Ge(v, Expr.Literal(lower)));
+ if (upper != Int32.MaxValue)
+ ret = Expr.And(ret, Expr.Le(v, Expr.Literal(upper)));
+ return ret;
+ }
+
+ }
+
+ public class PredicateAbsElem : IAbstractDomain
+ {
+ public static class ExprExt
+ {
+ public static Expr AndSimp(Expr e1, Expr e2)
+ {
+ if (e1 == Expr.True) return e2;
+ if (e2 == Expr.True) return e1;
+ if (e1 == Expr.False || e2 == Expr.False) return Expr.False;
+ return Expr.And(e1, e2);
+ }
+
+ public static Expr OrSimp(Expr e1, Expr e2)
+ {
+ if (e1 == Expr.False) return e2;
+ if (e2 == Expr.False) return e1;
+ if (e1 == Expr.True || e2 == Expr.True) return Expr.True;
+ return Expr.Or(e1, e2);
+ }
+ }
+
+ class Disjunct
+ {
+ public static int DisjunctBound = 3;
+ HashSet<int> pos;
+ HashSet<int> neg;
+ bool isTrue;
+
+ public Disjunct()
+ {
+ isTrue = true;
+ pos = new HashSet<int>();
+ neg = new HashSet<int>();
+ }
+
+ public Disjunct(IEnumerable<int> pos, IEnumerable<int> neg)
+ {
+ this.isTrue = false;
+ this.pos = new HashSet<int>(pos);
+ this.neg = new HashSet<int>(neg);
+ if (this.pos.Overlaps(this.neg))
+ {
+ this.isTrue = true;
+ this.pos = new HashSet<int>();
+ this.neg = new HashSet<int>();
+ }
+ if (this.pos.Count + this.neg.Count > DisjunctBound)
+ {
+ // Set to true
+ this.isTrue = true;
+ this.pos = new HashSet<int>();
+ this.neg = new HashSet<int>();
+ }
+
+ }
+
+ public Disjunct OR(Disjunct that)
+ {
+ if (isTrue)
+ return this;
+ if (that.isTrue)
+ return that;
+
+ return new Disjunct(this.pos.Concat(that.pos), this.neg.Concat(that.neg));
+ }
+
+ public bool Implies(Disjunct that)
+ {
+ if (isTrue) return that.isTrue;
+ if (that.isTrue) return true;
+
+ return pos.IsSubsetOf(that.pos) && neg.IsSubsetOf(that.neg);
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isTrue) return Expr.True;
+ Expr ret = Expr.False;
+ pos.Iter(i => ret = ExprExt.OrSimp(ret, vars[i]));
+ neg.Iter(i => ret = ExprExt.OrSimp(ret, Expr.Not(vars[i])));
+ return ret;
+ }
+ }
+
+ // Conjunction of Disjuncts
+ List<Disjunct> conjuncts;
+ bool isFalse;
+
+ public PredicateAbsElem()
+ {
+ this.conjuncts = new List<Disjunct>();
+ this.isFalse = true;
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return new PredicateAbsElem();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> state)
+ {
+ if (state.Any(me => !(me is Model.Boolean)))
+ throw new AbsHoudiniInternalError("Predicate Abstraction requires that each argument be of type bool");
+
+ // quick return if this == true
+ if (!this.isFalse && conjuncts.Count == 0)
+ return this;
+
+ var ret = new PredicateAbsElem();
+ ret.isFalse = false;
+
+ for (int i = 0; i < state.Count; i++)
+ {
+ var b = (state[i] as Model.Boolean).Value;
+ Disjunct d = null;
+ if (b) d = new Disjunct(new int[] { i }, new int[] { });
+ else d = new Disjunct(new int[] { }, new int[] { i });
+
+ if (isFalse)
+ ret.AddDisjunct(d);
+ else
+ {
+ conjuncts.Iter(c => ret.AddDisjunct(c.OR(d)));
+ }
+ }
+
+ return ret;
+
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isFalse) return Expr.False;
+ Expr ret = Expr.True;
+
+ foreach (var c in conjuncts)
+ {
+ ret = ExprExt.AndSimp(ret, c.Gamma(vars));
+ }
+
+ return ret;
+ }
+
+ private void AddDisjunct(Disjunct d)
+ {
+ if (conjuncts.Any(c => c.Implies(d)))
+ return;
+
+ conjuncts.RemoveAll(c => d.Implies(c));
+ conjuncts.Add(d);
+ }
+ }
+
+ // [false -- (x == true) -- true]
+ public class HoudiniConst : IAbstractDomain
+ {
+ bool isBottom;
+ bool isTop;
+
+ private HoudiniConst(bool isTop, bool isBottom)
+ {
+ this.isBottom = isBottom;
+ this.isTop = isTop;
+ Debug.Assert(!(isTop && isBottom));
+ }
+
+ public static HoudiniConst GetExtObj()
+ {
+ return new HoudiniConst(false, false);
+ }
+
+ public static HoudiniConst GetTop()
+ {
+ return new HoudiniConst(true, false);
+ }
+
+ public static HoudiniConst GetBottom()
+ {
+ return new HoudiniConst(false, true);
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return GetBottom();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> states)
+ {
+ Debug.Assert(states.Count == 1);
+ var state = states[0];
+
+ if (isTop) return this;
+
+ if (state is Model.Boolean)
+ {
+ if ((state as Model.Boolean).Value)
+ return GetExtObj();
+ }
+
+ return GetTop();
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ Debug.Assert(vars.Count == 1);
+ var v = vars[0];
+ if (isBottom) return Expr.False;
+ if (isTop) return Expr.True;
+ return v;
+ }
+ }
+
+
+ public class ConstantProp : IAbstractDomain
+ {
+ object val;
+ bool isBottom;
+ bool isTop;
+
+ private ConstantProp(object val, bool isTop, bool isBottom)
+ {
+ this.val = val;
+ this.isBottom = isBottom;
+ this.isTop = isTop;
+ Debug.Assert(!(isTop && isBottom));
+ Debug.Assert(val == null || (val is int) || (val is bool));
+ }
+
+ public static ConstantProp GetExtObj(object val)
+ {
+ Debug.Assert(val != null);
+ return new ConstantProp(val, false, false);
+ }
+
+ public static ConstantProp GetTop()
+ {
+ return new ConstantProp(null, true, false);
+ }
+
+ public static ConstantProp GetBottom()
+ {
+ return new ConstantProp(null, false, true);
+ }
+
+ private ConstantProp Join(ConstantProp that)
+ {
+ if (isBottom) return that;
+ if (isTop) return this;
+ if (that.isBottom) return this;
+ if (that.isTop) return that;
+
+ if ((val is int) && !(that.val is int))
+ throw new AbsHoudiniInternalError("Type mismatch in ExtObj");
+
+ if ((val is bool) && !(that.val is bool))
+ throw new AbsHoudiniInternalError("Type mismatch in ExtObj");
+
+ if (val is int)
+ {
+ var v1 = (int)val;
+ var v2 = (int)that.val;
+ if (v1 != v2) return GetTop();
+ return this;
+ }
+ else if (val is bool)
+ {
+ var v1 = (bool)val;
+ var v2 = (bool)that.val;
+ if (v1 != v2) return GetTop();
+ return this;
+ }
+ throw new AbsHoudiniInternalError("Illegal val type in ExtObj");
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return GetBottom();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> states)
+ {
+ Debug.Assert(states.Count == 1);
+ var state = states[0];
+ ConstantProp that = null;
+
+ if (state is Model.Integer)
+ {
+ that = GetExtObj((state as Model.Integer).AsInt());
+ }
+ else if (state is Model.Boolean)
+ {
+ that = GetExtObj((state as Model.Boolean).Value);
+ }
+ else
+ {
+ throw new AbsHoudiniInternalError("Illegal type " + state.GetType().ToString());
+ }
+
+ return Join(that);
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ Debug.Assert(vars.Count == 1);
+ var v = vars[0];
+ if (isBottom) return Expr.False;
+ if (isTop) return Expr.True;
+ if (val is int)
+ return Expr.Eq(v, Expr.Literal((int)val));
+ if (val is bool && (bool)val)
+ return v;
+ if (val is bool && !(bool)val)
+ return Expr.Not(v);
+
+ return null;
+ }
+ }
+
+
+ public class IndependentAttribute<T> : IAbstractDomain where T : class, IAbstractDomain
+ {
+ bool isBottom;
+ int numVars;
+ List<T> varVal;
+ T underlyingInstance;
+
+ public IndependentAttribute()
+ {
+ isBottom = true;
+ numVars = 0;
+ varVal = new List<T>();
+ underlyingInstance = null;
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return new IndependentAttribute<T>();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> state)
+ {
+ SetUnderlyingInstance();
+
+ if (!isBottom && numVars != state.Count)
+ {
+ throw new AbsHoudiniInternalError(
+ string.Format("Got illegal number of arguments ({0}), expected {1}", state.Count, numVars));
+ }
+
+ var ret = new IndependentAttribute<T>();
+ ret.isBottom = false;
+ ret.numVars = state.Count;
+ for(int i = 0; i < state.Count; i++)
+ {
+ var sl = new List<Model.Element>();
+ sl.Add(state[i]);
+ T prev = isBottom ? underlyingInstance.Bottom() as T : varVal[i];
+ ret.varVal.Add(prev.Join(sl) as T);
+ }
+
+ return ret;
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ if (isBottom) return Expr.False;
+ if (numVars != vars.Count)
+ throw new AbsHoudiniInternalError(
+ string.Format("Got illegal number of arguments ({0}), expected {1}", vars.Count, numVars));
+
+ Expr ret = Expr.True;
+ for (int i = 0; i < numVars; i++)
+ {
+ var sl = new List<Expr>(); sl.Add(vars[i]);
+ ret = Expr.And(ret, varVal[i].Gamma(sl));
+ }
+
+ return ret;
+ }
+
+ private void SetUnderlyingInstance()
+ {
+ if (underlyingInstance != null) return;
+ var tt = typeof(T);
+ underlyingInstance = AbstractDomainFactory.GetInstance(tt) as T;
+ }
+ }
+
+ public class AbstractDomainFactory
+ {
+ // Type name -> Instance
+ private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>();
+
+ public static void Register(IAbstractDomain instance)
+ {
+ var Name = instance.GetType().FullName;
+ Debug.Assert(!abstractDomainInstances.ContainsKey(Name));
+ abstractDomainInstances.Add(Name, instance);
+ }
+
+ public static IAbstractDomain GetInstance(System.Type type)
+ {
+ var Name = type.FullName;
+ Debug.Assert(abstractDomainInstances.ContainsKey(Name));
+ return abstractDomainInstances[Name] as IAbstractDomain;
+ }
+ }
+
+ public interface IAbstractDomain
+ {
+ IAbstractDomain Bottom();
+ IAbstractDomain Join(List<Model.Element> state);
+ Expr Gamma(List<Expr> vars);
+ }
+
public class AbstractHoudini
{
// Input Program
@@ -200,6 +1315,9 @@ namespace Microsoft.Boogie.Houdini { var s = tup.Value as PredicateAbs;
if (s == null) continue;
ret.UnionWith(s.GetPredicates(program, prover.VCExprGen, prover));
+ // debug output
+ //Console.WriteLine("Summary of {0}:", tup.Key);
+ //Console.WriteLine("{0}", tup.Value);
}
prover.Close();
@@ -516,10 +1634,8 @@ namespace Microsoft.Boogie.Houdini { //Console.WriteLine("Checking: {0}", vc);
if (CommandLineOptions.Clo.Trace)
- {
Console.WriteLine("Verifying {0} ({1}): {2}", impl.Name, usedLower ? "lower" : "ac", query);
- }
-
+
if (usedLower && lowerTime.TotalMilliseconds >= iterTimeLimit && iterTimeLimit >= 0)
{
if (UseBilateralAlgo)
@@ -1772,7 +2888,6 @@ namespace Microsoft.Boogie.Houdini { var ret = "";
if (isFalse) return "false";
var first = true;
- Simplify();
for(int i = 0; i < PostPreds[procName].Count; i++)
{
@@ -2158,7 +3273,7 @@ namespace Microsoft.Boogie.Houdini { public class PredicateAbsConjunct
{
- static int ConjunctBound = 2;
+ static int ConjunctBound = 3;
public bool isFalse { get; private set; }
HashSet<int> posPreds;
@@ -2279,8 +3394,10 @@ namespace Microsoft.Boogie.Houdini { {
if (isFalse) return Expr.False;
Expr ret = Expr.True;
- posPreds.Iter(p => ret = Expr.And(ret, predToExpr(p)));
- negPreds.Iter(p => ret = Expr.And(ret, Expr.Not(predToExpr(p))));
+ var pp = posPreds.ToList(); pp.Sort();
+ var np = negPreds.ToList(); np.Sort();
+ pp.Iter(p => ret = Expr.And(ret, predToExpr(p)));
+ np.Iter(p => ret = Expr.And(ret, Expr.Not(predToExpr(p))));
return ret;
}
@@ -2377,6 +3494,54 @@ namespace Microsoft.Boogie.Houdini { }
+ class FindExistentialFunctions : MutatingVCExprVisitor<bool>
+ {
+ public List<Tuple<string, VCExprVar, VCExprNAry>> funcCalls;
+ private HashSet<string> existentialFunctions;
+ private static int CounterId = 0;
+
+ public FindExistentialFunctions(VCExpressionGenerator gen, HashSet<string> existentialFunctions)
+ : base(gen)
+ {
+ funcCalls = new List<Tuple<string, VCExprVar, VCExprNAry>>();
+ this.existentialFunctions = existentialFunctions;
+ }
+
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ bool arg)
+ {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprNAry retnary = ret as VCExprNAry;
+ if (retnary == null) return ret;
+ var op = retnary.Op as VCExprBoogieFunctionOp;
+ if (op == null) return ret;
+
+ string calleeName = op.Func.Name;
+
+ if (!existentialFunctions.Contains(calleeName))
+ return ret;
+
+ var controlConst = Gen.Variable("AbsHoudiniControl" + CounterId, Microsoft.Boogie.Type.Bool);
+ CounterId++;
+
+ funcCalls.Add(Tuple.Create(calleeName, controlConst, retnary));
+
+ return controlConst;
+ }
+
+ }
+
class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler
{
public Model model;
@@ -2394,6 +3559,9 @@ namespace Microsoft.Boogie.Houdini { }
}
+ public class AbsHoudiniAssemblyLocator
+ {
+ }
public class AbsHoudiniInternalError : System.ApplicationException
{
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 23bbb1f9..16dec8b0 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -143,13 +143,9 @@ namespace Microsoft.Boogie public override ElementKind Kind { get { return ElementKind.DataValue; } }
public override string ToString() {
StringBuilder builder = new StringBuilder();
- builder.Append(ConstructorName + "(");
- int count = 0;
+ builder.Append("(").Append(ConstructorName);
foreach (Element arg in Arguments) {
- count++;
- builder.Append(arg);
- if (count < Arguments.Length)
- builder.Append(", ");
+ builder.Append(" ").Append(arg);
}
builder.Append(")");
return builder.ToString();
@@ -401,10 +397,9 @@ namespace Microsoft.Boogie public override string ToString()
{
var res = new StringBuilder();
- res.Append(Func.Name).Append("(");
+ res.Append("(").Append(Func.Name);
for (int i = 0; i < Args.Length; ++i) {
- if (i != 0) res.Append(", ");
- res.Append(Args[i]);
+ res.Append(" ").Append(Args[i]);
}
res.Append(") -> ").Append(Result);
return res.ToString();
@@ -729,6 +724,7 @@ namespace Microsoft.Boogie static Regex bv = new Regex(@"\(_ BitVec (\d+)\)");
+ /*
List<object> GetFunctionTuple(string newLine) {
if (newLine == null)
return null;
@@ -748,27 +744,25 @@ namespace Microsoft.Boogie line = line.Replace("(", " ( ");
line = line.Replace(")", " ) ");
+ line = line.Replace(",", " ");
var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
List<object> newTuple = new List<object>();
- Stack<List<object>> wordStack = new Stack<List<object>>();
+ Stack<int> wordStack = new Stack<int>();
for (int i = 0; i < tuple.Length; i++) {
string elem = tuple[i];
if (elem == "(") {
- List<object> ls = new List<object>();
- wordStack.Push(ls);
+ wordStack.Push(newTuple.Count - 1);
}
else if (elem == ")") {
- List<object> ls = wordStack.Pop();
- if (wordStack.Count > 0) {
- wordStack.Peek().Add(ls);
- }
- else {
- newTuple.Add(ls);
+ int openParenIndex = wordStack.Pop();
+ List<object> ls = new List<object>();
+ for (int j = openParenIndex; j < newTuple.Count; j++)
+ {
+ ls.Add(newTuple[j]);
}
- }
- else if (wordStack.Count > 0) {
- wordStack.Peek().Add(elem);
+ newTuple.RemoveRange(openParenIndex, newTuple.Count - openParenIndex);
+ newTuple.Add(ls);
}
else {
newTuple.Add(elem);
@@ -776,7 +770,67 @@ namespace Microsoft.Boogie }
return newTuple;
}
+ */
+
+ List<object> GetFunctionTuple(string newLine)
+ {
+ if (newLine == null)
+ return null;
+ newLine = bv.Replace(newLine, "bv${1}");
+ string line = newLine;
+ int openParenCounter = CountOpenParentheses(newLine, 0);
+ if (!newLine.Contains("}"))
+ {
+ while (openParenCounter > 0)
+ {
+ newLine = ReadLine();
+ if (newLine == null)
+ {
+ return null;
+ }
+ line += newLine;
+ openParenCounter = CountOpenParentheses(newLine, openParenCounter);
+ }
+ }
+
+ line = line.Replace("(", " ( ");
+ line = line.Replace(")", " ) ");
+ var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
+ List<object> newTuple = new List<object>();
+ Stack<List<object>> wordStack = new Stack<List<object>>();
+ for (int i = 0; i < tuple.Length; i++)
+ {
+ string elem = tuple[i];
+ if (elem == "(")
+ {
+ List<object> ls = new List<object>();
+ wordStack.Push(ls);
+ }
+ else if (elem == ")")
+ {
+ List<object> ls = wordStack.Pop();
+ if (wordStack.Count > 0)
+ {
+ wordStack.Peek().Add(ls);
+ }
+ else
+ {
+ newTuple.Add(ls);
+ }
+ }
+ else if (wordStack.Count > 0)
+ {
+ wordStack.Peek().Add(elem);
+ }
+ else
+ {
+ newTuple.Add(elem);
+ }
+ }
+ return newTuple;
+ }
+
string[] GetWords(string line)
{
if (line == null)
@@ -856,11 +910,17 @@ namespace Microsoft.Boogie for (; ; ) {
var tmpline = ReadLine();
if (tmpline == "*** END_STATE") break;
- var tuple = GetWords(tmpline);
+ var tuple = GetFunctionTuple(tmpline);
if (tuple == null) BadModel("EOF in state table");
- if (tuple.Length == 0) continue;
- if (tuple.Length != 3 || tuple[1] != "->") BadModel("invalid state tuple definition");
- cs.AddBinding(tuple[0], GetElt(tuple[2]));
+ if (tuple.Count == 0) continue;
+ if (tuple.Count == 3 && tuple[0] is string && tuple[1] is string && ((string) tuple[1]) == "->")
+ {
+ cs.AddBinding((string)tuple[0], GetElt(tuple[2]));
+ }
+ else
+ {
+ BadModel("invalid state tuple definition");
+ }
}
continue;
}
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index cf125c76..da73dea1 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -709,15 +709,19 @@ namespace Microsoft.Boogie.SMTLib var builtin = ExtractBuiltin(op.Func);
var datatype = ExtractDatatype(op.Func);
if (builtin != null)
- printedName = builtin;
+ {
+ printedName = CheckMapApply(builtin, node);
+ }
else if (datatype != null)
- printedName = datatype;
+ {
+ printedName = datatype;
+ }
else
- printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ {
+ printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ }
Contract.Assert(printedName != null);
- printedName = CheckMapApply(printedName, node);
-
WriteApplication(printedName, node, options);
return true;
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer index d2418bd4..2ba2eed3 100644 --- a/Test/AbsHoudini/Answer +++ b/Test/AbsHoudini/Answer @@ -1,11 +1,379 @@ --------------------- f1.bpl --------------------
-Summary of foo:
-g == old(g) + 1
-Summary of main:
-(old(g) == 0 ==> g == old(g) + 1)
-Prover time = 0.0260026
-Number of prover queries = 6
-Witness written to absHoudiniWitness.bpl
+-------------------- houd1.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+ true
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd2.bpl --------------------
+function {:existential true} {:inline} Assert(x: bool) : bool
+{
+ true
+}
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+ true
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd3.bpl --------------------
+function {:existential true} {:inline} Assert(x: bool) : bool
+{
+ x
+}
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+ true
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+ true
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd4.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+function {:existential true} {:inline} b1() : bool
+{
+ false
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+ false
+}
+function {:existential true} {:inline} b3(x: bool) : bool
+{
+ false
+}
+function {:existential true} {:inline} b4(x: bool) : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd5.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+ !x
+}
+function {:existential true} {:inline} b2(x: bool) : bool
+{
+ x
+}
+function {:existential true} {:inline} b3(x: bool) : bool
+{
+ !x
+}
+function {:existential true} {:inline} b4(x: bool) : bool
+{
+ x
+}
+function {:existential true} {:inline} b5() : bool
+{
+ false
+}
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd6.bpl --------------------
+function {:existential true} {:inline} b1() : bool
+{
+ true
+}
+function {:existential true} {:inline} b2() : bool
+{
+ true
+}
+function {:existential true} {:inline} b3() : bool
+{
+ true
+}
+function {:existential true} {:inline} b4() : bool
+{
+ true
+}
+function {:existential true} {:inline} b5() : bool
+{
+ true
+}
+function {:existential true} {:inline} b6() : bool
+{
+ true
+}
+function {:existential true} {:inline} b7() : bool
+{
+ true
+}
+function {:existential true} {:inline} b8() : bool
+{
+ true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd7.bpl --------------------
+function {:existential true} {:inline} b1() : bool
+{
+ false
+}
+function {:existential true} {:inline} b2() : bool
+{
+ true
+}
+function {:existential true} {:inline} b3() : bool
+{
+ true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd8.bpl --------------------
+function {:existential true} {:inline} b1() : bool
+{
+ false
+}
+function {:existential true} {:inline} b2() : bool
+{
+ true
+}
+function {:existential true} {:inline} b3() : bool
+{
+ true
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd9.bpl --------------------
+Error opening file "houd9.bpl": Could not find file 'C:\Users\akashl\Documents\work\boogie\Test\AbsHoudini\houd9.bpl'.
+
+-------------------- houd10.bpl --------------------
+function {:existential true} {:inline} b1() : bool
+{
+ true
+}
+function {:existential true} {:inline} b2() : bool
+{
+ false
+}
+function {:existential true} {:inline} b3() : bool
+{
+ true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+ true
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd11.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+ true
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+
+-------------------- houd12.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+function {:existential true} {:inline} b1() : bool
+{
+ true
+}
+function {:existential true} {:inline} b2() : bool
+{
+ false
+}
+function {:existential true} {:inline} b3() : bool
+{
+ false
+}
+function {:existential true} {:inline} b4() : bool
+{
+ false
+}
+function {:existential true} {:inline} b5() : bool
+{
+ false
+}
+function {:existential true} {:inline} b6() : bool
+{
+ true
+}
+function {:existential true} {:inline} b7() : bool
+{
+ true
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+.
+-------------------- test1.bpl --------------------
+function {:existential true} {:inline} b0() : bool
+{
+ false
+}
+function {:existential true} {:inline} b1() : bool
+{
+ true
+}
+function {:existential true} {:inline} b2() : bool
+{
+ true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+.
+-------------------- test2.bpl --------------------
+function {:existential true} {:inline} b0() : bool
+{
+ false
+}
+function {:existential true} {:inline} b1() : bool
+{
+ true
+}
+function {:existential true} {:inline} b2() : bool
+{
+ true
+}
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+.
+-------------------- test7.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+.
+-------------------- test8.bpl --------------------
+function {:existential true} {:inline} Assert() : bool
+{
+ false
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+.
+-------------------- test9.bpl --------------------
+function {:existential true} {:inline} b1() : bool
+{
+ true
+}
+function {:existential true} {:inline} b2() : bool
+{
+ true
+}
+function {:existential true} {:inline} b3() : bool
+{
+ true
+}
+function {:existential true} {:inline} b4() : bool
+{
+ false
+}
+function {:existential true} {:inline} b5() : bool
+{
+ true
+}
+function {:existential true} {:inline} b6() : bool
+{
+ false
+}
+function {:existential true} {:inline} b7() : bool
+{
+ true
+}
+function {:existential true} {:inline} b8() : bool
+{
+ true
+}
+function {:existential true} {:inline} b9() : bool
+{
+ true
+}
+function {:existential true} {:inline} b10() : bool
+{
+ false
+}
+function {:existential true} {:inline} b11() : bool
+{
+ true
+}
+function {:existential true} {:inline} b12() : bool
+{
+ false
+}
+function {:existential true} {:inline} b13() : bool
+{
+ true
+}
+function {:existential true} {:inline} b14() : bool
+{
+ true
+}
+function {:existential true} {:inline} b15() : bool
+{
+ true
+}
+function {:existential true} {:inline} b16() : bool
+{
+ true
+}
+
+Boogie program verifier finished with 0 verified, 0 errors
+.
+-------------------- test10.bpl --------------------
+function {:existential true} {:inline} b1() : bool
+{
+ false
+}
+function {:existential true} {:inline} b2() : bool
+{
+ false
+}
+function {:existential true} {:inline} b3() : bool
+{
+ false
+}
+function {:existential true} {:inline} b4() : bool
+{
+ false
+}
Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl new file mode 100644 index 00000000..fc3d5713 --- /dev/null +++ b/Test/AbsHoudini/houd1.bpl @@ -0,0 +1,17 @@ +function {:existential true} b1(x: bool) : bool;
+
+var myVar: int;
+
+procedure foo (i:int)
+modifies myVar;
+// comment
+ensures b1(myVar>0);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected end assigment: b1(x) = true
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl new file mode 100644 index 00000000..bb0c65e7 --- /dev/null +++ b/Test/AbsHoudini/houd10.bpl @@ -0,0 +1,22 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var fooVar: int;
+var xVar: int;
+
+procedure foo()
+modifies fooVar;
+modifies xVar;
+ensures b1() || fooVar==0;
+ensures b3() || xVar<0;
+{
+ fooVar:=5;
+ call bar();
+}
+
+procedure bar();
+modifies xVar;
+requires Assert() || fooVar!=5;
+
+// expected assigment: Assert->true,b1->True,b2->false,b3->True
diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl new file mode 100644 index 00000000..78087744 --- /dev/null +++ b/Test/AbsHoudini/houd11.bpl @@ -0,0 +1,13 @@ +function {:existential true} Assert() : bool;
+
+var fooVar: int;
+
+procedure foo()
+modifies fooVar;
+{
+ fooVar:=5;
+ assert Assert() || (fooVar==4);
+ assert Assert() || (fooVar==3);
+}
+
+// expected assigment: Assert -> true
diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl new file mode 100644 index 00000000..b3a1a6db --- /dev/null +++ b/Test/AbsHoudini/houd12.bpl @@ -0,0 +1,58 @@ +// Example to test candidate annotations on loops
+
+function {:existential true} Assert(): bool;
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {:existential true} b7():bool;
+
+var x: int;
+var y: int;
+
+
+procedure foo()
+modifies x;
+modifies y;
+ensures (b4() || x == 0);
+ensures (b5() || y == 10);
+ensures (b6() || x == 10);
+ensures (b7() || y == 11);
+
+{
+ x := 10;
+ y := 0;
+
+ goto Head;
+
+Head:
+
+ //loop invariants
+ assert (b1() || x < 0);
+ assert (b2() || x >= 0);
+ assert (b3() || x + y == 10);
+ goto Body, Exit;
+
+Body:
+ assume x > 0;
+ x := x - 1;
+ y := y + 1;
+
+
+ goto Head;
+
+Exit:
+ assume !(x > 0);
+ return;
+}
+
+// expected assigment: Assert -> false, b1->true,b2->false,b3->false,b4->false, b5->false, b6->true,b7->true
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl new file mode 100644 index 00000000..fd2611e2 --- /dev/null +++ b/Test/AbsHoudini/houd2.bpl @@ -0,0 +1,27 @@ +function {:existential true} Assert(x:bool) : bool;
+function {:existential true} b1 (x:bool):bool;
+function {:existential true} b2 (x:bool):bool;
+
+
+var myVar: int;
+
+procedure bar(i:int)
+modifies myVar;
+ensures Assert(myVar>0);
+{
+ call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+ensures Assert(myVar!=-1);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected end assigment: Assert(x) = true, b1(x) = true, b2(x) = false
diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl new file mode 100644 index 00000000..81f11018 --- /dev/null +++ b/Test/AbsHoudini/houd3.bpl @@ -0,0 +1,27 @@ +function {:existential true} Assert(x: bool) : bool;
+function {:existential true} b1(x: bool) : bool;
+function {:existential true} b2(x: bool) : bool;
+
+
+var myVar: int;
+
+procedure bar(i:int)
+modifies myVar;
+ensures b2(myVar>0);
+{
+ call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+ensures Assert(myVar!=-1);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected end assigment: Assert(x) = x, b1(x) = True, b2(x) = True
diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl new file mode 100644 index 00000000..01ee6707 --- /dev/null +++ b/Test/AbsHoudini/houd4.bpl @@ -0,0 +1,27 @@ +function {:existential true} Assert() : bool;
+function {:existential true} b1():bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b2(i > 0);
+ensures b3(array[i] > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+ array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b4(j > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} (!b1() && x == j) || array[x] == old(array)[x]);
+{
+ call foo(j);
+ result := array[j];
+}
+
+// expected assignment: Assert = false, b1(x) = false, b2(x) = false, b3(x) = false, b4(x) = false
diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl new file mode 100644 index 00000000..afbaa81c --- /dev/null +++ b/Test/AbsHoudini/houd5.bpl @@ -0,0 +1,29 @@ +function {:existential true} b1(x:bool):bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+function {:existential true} b5():bool;
+function {:existential true} Assert():bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b1(i == 0);
+requires b2(i > 0);
+requires b3(i < 0);
+ensures b4(array[i] > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+ array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b5() || (j > 0);
+modifies array;
+{
+ call foo(j);
+ result := array[j];
+}
+
+// expected assigment: assert = false, b1(x) = !x, b2(x) = x, b3(x) = !x, b4(x) = x, b5() = false
diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl new file mode 100644 index 00000000..e4927901 --- /dev/null +++ b/Test/AbsHoudini/houd6.bpl @@ -0,0 +1,44 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {:existential true} b7():bool;
+function {:existential true} b8():bool;
+function {:existential true} Assert(): bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b6() || i < 0;
+requires b5() || i == 0;
+requires b2() || i > 0;
+ensures b3() || array[i] > 0;
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+ array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b8() || j < 0;
+requires b7() || j == 0;
+requires b4() || j > 0;
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} (x == j) || array[x] == old(array)[x]);
+ensures b1() || array[j] == old(array)[j];
+{
+ call foo(j);
+ result := array[j];
+}
+
+var p:int;
+
+procedure main() returns (result: int)
+modifies array;
+{
+ call result:= bar(p);
+}
+
+// expected assigment: Assert -> false, bi->true forall i
diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl new file mode 100644 index 00000000..ef3293db --- /dev/null +++ b/Test/AbsHoudini/houd7.bpl @@ -0,0 +1,35 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var myVar: int;
+
+procedure foo(i:int)
+requires b1() || i>0;
+requires b2() || i==0;
+requires b3() || i<0;
+modifies myVar;
+ensures Assert() || myVar>0;
+{
+ myVar:=5;
+}
+
+procedure bar(i:int)
+modifies myVar;
+{
+ call foo(5);
+}
+// expected outcome: Correct
+// expected Assigment: Assert = false, b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl new file mode 100644 index 00000000..8be7f3db --- /dev/null +++ b/Test/AbsHoudini/houd8.bpl @@ -0,0 +1,29 @@ +function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+
+var myVar: int;
+
+procedure foo(i:int)
+modifies myVar;
+ensures b1() || myVar>0;
+ensures b2() || myVar==0;
+ensures b3() || myVar<0;
+{
+ myVar:=5;
+}
+
+// expected assigment: b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/int1.bpl b/Test/AbsHoudini/int1.bpl new file mode 100644 index 00000000..0ee0f1b9 --- /dev/null +++ b/Test/AbsHoudini/int1.bpl @@ -0,0 +1,26 @@ +function {:existential true} b0(x:int): bool;
+function {:existential true} b1(x:int): bool;
+
+var g: int;
+
+procedure foo()
+modifies g;
+requires b0(g);
+ensures b1(g);
+{
+ if(*) {
+ g := g + 1;
+ call foo();
+ }
+}
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ if(*) { g := 5; }
+ call foo();
+}
+
+
+// Expected: b0(x) = [0,\infty], b1(x) = [0, \infty]
diff --git a/Test/AbsHoudini/pred1.bpl b/Test/AbsHoudini/pred1.bpl new file mode 100644 index 00000000..fc37a15b --- /dev/null +++ b/Test/AbsHoudini/pred1.bpl @@ -0,0 +1,23 @@ +function {:existential true} b0(x:bool, y:bool): bool;
+function {:existential true} b1(x:bool, y:bool): bool;
+function {:existential true} b2(x:bool, y:bool): bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+ensures b0(g == 0, g == 5);
+{
+ g := 0;
+ if(*) { g := 5; }
+ call foo();
+}
+
+procedure foo()
+ modifies g;
+ requires b1(g == 0, g == 5);
+ ensures b2(g == 0, g == 5);
+{
+ assume g != 5;
+}
+
diff --git a/Test/AbsHoudini/pred2.bpl b/Test/AbsHoudini/pred2.bpl new file mode 100644 index 00000000..3ce948ce --- /dev/null +++ b/Test/AbsHoudini/pred2.bpl @@ -0,0 +1,12 @@ +function {:existential true} b0(x:bool): bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+ensures b0(g == old(g));
+{
+ if(*) { g := 5; }
+ assume g != 5;
+}
+
diff --git a/Test/AbsHoudini/pred3.bpl b/Test/AbsHoudini/pred3.bpl new file mode 100644 index 00000000..450efde4 --- /dev/null +++ b/Test/AbsHoudini/pred3.bpl @@ -0,0 +1,24 @@ +function {:existential true} b0(x:bool, y:bool): bool;
+function {:existential true} b1(x:bool, y:bool): bool;
+function {:existential true} b2(x:bool, y:bool): bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+ensures b0(g == 0, g == 5);
+{
+ assume 0 == old(g) || 1 == old(g);
+ g := 0;
+ if(*) { g := 5; }
+ call foo();
+}
+
+procedure foo()
+ modifies g;
+ requires b1(g == 0, g == 5);
+ ensures b2(old(g) == 0, old(g) == 5);
+{
+ assume g != 5;
+}
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat index 34308e4e..88ac1fd5 100644 --- a/Test/AbsHoudini/runtest.bat +++ b/Test/AbsHoudini/runtest.bat @@ -3,9 +3,14 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (f1.bpl) do (
+for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer /abstractHoudini:PredicateAbs %%f
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f
)
+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
+ echo .
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:IA[ConstantProp] %%f
+)
diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl new file mode 100644 index 00000000..5884cf7b --- /dev/null +++ b/Test/AbsHoudini/test1.bpl @@ -0,0 +1,38 @@ +var g: bool;
+
+procedure foo()
+modifies g;
+ensures b0() || (!old(g) ==> old(g) == g);
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g;
+ensures b1() || old(g) == g;
+{
+ g := true;
+}
+
+procedure ReleaseLock()
+modifies g;
+ensures b2() || old(g) == g;
+{
+ g := false;
+}
+
+procedure main()
+modifies g;
+{
+ g := false;
+ call foo();
+ assert Assert() || !g;
+}
+
+function {:existential true} b0(): bool;
+function {:existential true} b1(): bool;
+function {:existential true } b2(): bool;
+function {:existential true} Assert(): bool;
+
+// Expected: b0 = false, b1 = true, b2 = true, Assert = false
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl new file mode 100644 index 00000000..a30c3159 --- /dev/null +++ b/Test/AbsHoudini/test10.bpl @@ -0,0 +1,50 @@ +var sdv_7: int;
+var sdv_21: int;
+function {:existential true} b1(): bool;
+function{:existential true} b2(): bool;
+function{:existential true} b3(): bool;
+function{:existential true} b4(): bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+ sdv_21 := sdv_7;
+ sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := sdv_21;
+ havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1() || (sdv_7 == 0);
+ensures{:candidate} b2() || (sdv_7 == old(sdv_7));
+{
+ call push(2);
+ call pop();
+ call bar();
+}
+
+procedure bar()
+requires{:candidate} b3() || (sdv_7 == 0);
+ensures{:candidate} b4() || (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+ call push(1);
+ call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := 0;
+ call foo();
+}
+
+// Expected: All false
+
+
diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl new file mode 100644 index 00000000..bfd78363 --- /dev/null +++ b/Test/AbsHoudini/test2.bpl @@ -0,0 +1,40 @@ +var g: int;
+var h: int;
+
+procedure foo()
+modifies g, h;
+ensures b0() || old(g) == g;
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g, h;
+ensures b1() || old(g) == g;
+{
+ h := g;
+ g := 1;
+}
+
+procedure ReleaseLock()
+modifies g, h;
+ensures b2() || old(g) == g;
+{
+ g := h;
+}
+
+procedure main()
+modifies g, h;
+{
+ g := 0;
+ call foo();
+ assert Assert() || g == 0;
+}
+
+function {:existential true} b0(): bool;
+function {:existential true} b1(): bool;
+function {:existential true} b2(): bool;
+function {:existential true} Assert(): bool;
+
+// Expected: Assert = false, b0 = false, b1 = true, b2 = true
diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl new file mode 100644 index 00000000..bfe8a32d --- /dev/null +++ b/Test/AbsHoudini/test7.bpl @@ -0,0 +1,19 @@ +function {:existential true} Assert() : bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert Assert() || g == 1;
+}
+
+procedure foo()
+modifies g;
+{
+ g := g + 1;
+}
+
+// Expected: Assert = false
diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl new file mode 100644 index 00000000..6c55016a --- /dev/null +++ b/Test/AbsHoudini/test8.bpl @@ -0,0 +1,25 @@ +function {:existential true} Assert(): bool;
+
+var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert Assert() || g == 1;
+}
+
+procedure {:inline 1} foo()
+modifies g;
+{
+ call bar();
+}
+
+procedure bar()
+modifies g;
+{
+ g := g + 1;
+}
+
+// Expected: Assert = false
diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl new file mode 100644 index 00000000..c08edf6b --- /dev/null +++ b/Test/AbsHoudini/test9.bpl @@ -0,0 +1,90 @@ +var v1: int;
+var v2: int;
+var v3: int;
+function{:existential true} b1(): bool;
+function{:existential true} b2(): bool;
+function{:existential true} b3(): bool;
+function{:existential true} b4(): bool;
+function{:existential true} b5(): bool;
+function{:existential true} b6(): bool;
+function{:existential true} b7(): bool;
+function{:existential true} b8(): bool;
+function{:existential true} b9(): bool;
+function{:existential true} b10(): bool;
+function{:existential true} b11(): bool;
+function{:existential true} b12(): bool;
+function{:existential true} b13(): bool;
+function{:existential true} b14(): bool;
+function{:existential true} b15(): bool;
+function{:existential true} b16(): bool;
+
+procedure push()
+requires {:candidate} b1() || v1 == 0;
+requires {:candidate} b2() || v1 == 1;
+ensures {:candidate} b3() || v1 == 0;
+ensures {:candidate} b4() || v1 == 1;
+modifies v1,v2;
+{
+ v2 := v1;
+ v1 := 1;
+}
+
+procedure pop()
+modifies v1,v2;
+requires {:candidate} b5() || v1 == 0;
+requires {:candidate} b6() || v1 == 1;
+ensures {:candidate} b7() || v1 == 0;
+ensures {:candidate} b8() || v1 == 1;
+{
+ v1 := v2;
+ havoc v2;
+}
+
+procedure foo()
+modifies v1,v2;
+requires {:candidate} b9() || v1 == 0;
+requires {:candidate} b10() || v1 == 1;
+ensures {:candidate} b11() || v1 == 0;
+ensures {:candidate} b12() || v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure bar()
+modifies v1,v2;
+requires {:candidate} b13() || v1 == 0;
+requires {:candidate} b14() || v1 == 1;
+ensures {:candidate} b15() || v1 == 0;
+ensures {:candidate} b16() || v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure main()
+modifies v1,v2;
+{
+ v1 := 1;
+ call foo();
+ havoc v1;
+ call bar();
+}
+
+// Expected:
+//b1 = true
+//b2 = true
+//b3 = true
+//b4 = false
+//b5 = true
+//b6 = false
+//b7 = true
+//b8 = true
+//b9 = true
+//b10 = false
+//b11 = true
+//b12 = false
+//b13 = true
+//b14 = true
+//b15 = true
+//b16 = true
diff --git a/Test/linear/Answer b/Test/linear/Answer index 69caec25..680f9895 100644 --- a/Test/linear/Answer +++ b/Test/linear/Answer @@ -14,6 +14,7 @@ typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter
typecheck.bpl(61,4): Error: A linear set can occur only once as an in parameter
typecheck.bpl(66,6): Error: Only linear variable can be assigned to another linear variable
+typecheck.bpl(75,4): Error: A linear variable on the right hand side of an assignment must be in the modifies set
0 type checking errors detected in typecheck.bpl
-------------------- list.bpl --------------------
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat index d054b097..5681784a 100644 --- a/Test/linear/runtest.bat +++ b/Test/linear/runtest.bat @@ -3,7 +3,13 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (typecheck.bpl list.bpl allocator.bpl) do (
+for %%f in (typecheck.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
+)
+
+for %%f in (list.bpl allocator.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index c188d5b5..ff2d7da4 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -66,4 +66,11 @@ procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, c := a;
}
-procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);
\ No newline at end of file +procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);
+
+var{:linear "x"} g:int;
+
+procedure G(i:int) returns({:linear "x"} r:int)
+{
+ r := g;
+}
diff --git a/Test/og/Answer b/Test/og/Answer index 154b0193..5a3142c5 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -3,7 +3,7 @@ foo.bpl(13,3): Error BP5001: This assertion might not hold.
Execution trace:
foo.bpl(5,5): anon0
- (0,0): inline$YieldChecker_PC$0$L1
+ (0,0): inline$Impl_YieldChecker_PC$0$L0
Boogie program verifier finished with 3 verified, 1 error
@@ -11,11 +11,11 @@ Boogie program verifier finished with 3 verified, 1 error bar.bpl(12,3): Error BP5001: This assertion might not hold.
Execution trace:
bar.bpl(5,5): anon0
- (0,0): inline$YieldChecker_PC$0$L1
+ (0,0): inline$Impl_YieldChecker_PC$0$L0
bar.bpl(12,3): Error BP5001: This assertion might not hold.
Execution trace:
bar.bpl(17,5): anon0
- (0,0): inline$YieldChecker_PC$0$L1
+ (0,0): inline$Impl_YieldChecker_PC$0$L0
Boogie program verifier finished with 2 verified, 2 errors
@@ -27,11 +27,11 @@ Boogie program verifier finished with 2 verified, 0 errors parallel1.bpl(9,3): Error BP5001: This assertion might not hold.
Execution trace:
parallel1.bpl(5,5): anon0
- (0,0): inline$YieldChecker_PC$0$L1
+ (0,0): inline$Proc_YieldChecker_PC$0$L0
parallel1.bpl(13,3): Error BP5001: This assertion might not hold.
Execution trace:
parallel1.bpl(5,5): anon0
- (0,0): inline$YieldChecker_PC$0$L2
+ (0,0): inline$Impl_YieldChecker_PC$0$L0
Boogie program verifier finished with 3 verified, 2 errors
@@ -63,12 +63,19 @@ Boogie program verifier finished with 4 verified, 0 errors parallel4.bpl(14,3): Error BP5001: This assertion might not hold.
Execution trace:
parallel4.bpl(12,3): anon0
- (0,0): inline$YieldChecker_t$0$enter
- (0,0): inline$YieldChecker_t$0$exit
- parallel4.bpl(12,3): anon0$2
+ (0,0): inline$og_yield$0$Return
+ parallel4.bpl(12,3): anon0$1
Boogie program verifier finished with 2 verified, 1 error
-------------------- parallel5.bpl --------------------
Boogie program verifier finished with 4 verified, 0 errors
+
+-------------------- parallel6.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- parallel7.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl new file mode 100644 index 00000000..aff53a48 --- /dev/null +++ b/Test/og/houd1.bpl @@ -0,0 +1,21 @@ +const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true} b2: bool;
+
+var x:int;
+
+procedure A()
+{
+ x := x + 1;
+ yield;
+}
+
+procedure B()
+{
+ x := 5;
+ yield;
+ assert b0 ==> (x == 5);
+ assert b1 ==> (x >= 5);
+ assert b2 ==> (x >= 6);
+}
+
diff --git a/Test/og/parallel6.bpl b/Test/og/parallel6.bpl new file mode 100644 index 00000000..dba3eb2b --- /dev/null +++ b/Test/og/parallel6.bpl @@ -0,0 +1,2 @@ +procedure A();
+procedure C() { async call A(); }
diff --git a/Test/og/parallel7.bpl b/Test/og/parallel7.bpl new file mode 100644 index 00000000..79c92196 --- /dev/null +++ b/Test/og/parallel7.bpl @@ -0,0 +1,3 @@ +procedure A();
+procedure B();
+procedure C() { call A() | B(); }
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 64c21618..4009b62f 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
|