summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/CommandLineOptions.cs2
-rw-r--r--Source/ModelViewer/VccProvider.cs2
-rw-r--r--Source/Provers/SMTLib/Z3.cs5
-rw-r--r--Source/Provers/Z3/Prover.cs6
-rw-r--r--Source/VCGeneration/VC.cs197
5 files changed, 36 insertions, 176 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c6b8e493..f0e325e8 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -353,7 +353,7 @@ namespace Microsoft.Boogie {
public bool PrintInlined = false;
public bool ExtractLoops = false;
public int LazyInlining = 0;
- public int ProcedureCopyBound = 1;
+ public int ProcedureCopyBound = 0;
public int StratifiedInlining = 0;
public int StratifiedInliningOption = 0;
public bool UseUnsatCoreForInlining = false;
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 1fe322b4..a11199f6 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -901,7 +901,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
} else if (kind == DataKind.Map) {
var elTp = tpl.Args[1];
foreach (var sel in model.Functions)
- if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {
+ if (elt != null && sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {
foreach (var app in sel.AppsWithArg(0, elt)) {
var val = WrapForUse(app.Result, elTp);
var edgname = new EdgeName(this, "[%0]", app.Args[1]);
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index da9e8faa..9b90b12a 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -152,11 +152,6 @@ namespace Microsoft.Boogie.SMTLib
options.AddWeakSmtOption("TYPE_CHECK", "true");
options.AddWeakSmtOption("BV_REFLECT", "true");
- if (CommandLineOptions.Clo.LazyInlining == 2) {
- options.AddWeakSmtOption("MACRO_EXPANSION", "true");
- options.AddWeakSmtOption("WARNING", "false");
- }
-
if (options.TimeLimit > 0) {
options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 640f98ae..8929e732 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -84,9 +84,6 @@ namespace Microsoft.Boogie.Z3
StringBuilder cmdLineArgsBldr = new StringBuilder();
AppendCmdLineOption(cmdLineArgsBldr, "si");
- if (CommandLineOptions.Clo.LazyInlining == 2)
- AppendCmdLineOption(cmdLineArgsBldr, "nw");
-
if (CommandLineOptions.Clo.z3AtFlag)
AppendCmdLineOption(cmdLineArgsBldr, "@");
@@ -165,9 +162,6 @@ namespace Microsoft.Boogie.Z3
AddOption(result, "BV_REFLECT", "true");
}
- if (CommandLineOptions.Clo.LazyInlining == 2)
- AddOption(result, "MACRO_EXPANSION", "true");
-
foreach (string opt in CommandLineOptions.Clo.Z3Options) {
Contract.Assert(opt != null);
int eq = opt.IndexOf("=");
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 576ce080..79fdaaa2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -27,7 +27,6 @@ namespace VC {
[NotDelayed]
public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
: base(program)
- // throws ProverException
{
Contract.Requires(program != null);
this.appendLogFile = appendLogFile;
@@ -36,10 +35,6 @@ namespace VC {
if (CommandLineOptions.Clo.LazyInlining > 0) {
this.GenerateVCsForLazyInlining(program);
- if (CommandLineOptions.Clo.LazyInlining == 3)
- {
- CreateCopiesForLazyInlining(CommandLineOptions.Clo.ProcedureCopyBound, program);
- }
}
}
@@ -85,9 +80,9 @@ namespace VC {
public Function function;
public Variable controlFlowVariable;
public List<Variable> interfaceVars;
+ public List<List<Variable>> interfaceVarCopies;
public Expr assertExpr;
public VCExpr vcexpr;
- public VCExpr inside_vc; // (without the quantifiers)
public List<VCExprVar> privateVars;
public Dictionary<Incarnation, Absy> incarnationOriginMap;
public Hashtable /*Variable->Expr*/ exitIncarnationMap;
@@ -163,6 +158,17 @@ namespace VC {
Contract.Assert(returnVar != null);
this.function = new Function(Token.NoToken, proc.Name, functionInterfaceVars, returnVar);
ctxt.DeclareFunction(this.function, "");
+
+ interfaceVarCopies = new List<List<Variable>>();
+ int temp = 0;
+ for (int i = 0; i < CommandLineOptions.Clo.ProcedureCopyBound; i++) {
+ interfaceVarCopies.Add(new List<Variable>());
+ foreach (Variable v in interfaceVars) {
+ Constant constant = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type));
+ interfaceVarCopies[i].Add(constant);
+ //program.TopLevelDeclarations.Add(constant);
+ }
+ }
}
}
[ContractInvariantMethod]
@@ -217,6 +223,25 @@ namespace VC {
}
Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);
proc.Ensures.Add(new Ensures(true, freePostExpr));
+
+ if (CommandLineOptions.Clo.ProcedureCopyBound > 0) {
+ Expr ret = new LiteralExpr(Token.NoToken, false);
+ for (int k = 0; k < CommandLineOptions.Clo.ProcedureCopyBound; k++) {
+ var iv = info.interfaceVarCopies[k];
+ Contract.Assert(info.function.InParams.Length == iv.Count);
+
+ Expr conj = new LiteralExpr(Token.NoToken, true);
+ for (int i = 0; i < iv.Count; i++) {
+ Expr eqExpr = new NAryExpr(
+ Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Eq), new ExprSeq(exprs[i], Expr.Ident(iv[i])));
+ conj =
+ new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.And), new ExprSeq(conj, eqExpr));
+ }
+ ret =
+ new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Or), new ExprSeq(ret, conj));
+ }
+ proc.Ensures.Add(new Ensures(true, ret));
+ }
}
}
@@ -226,145 +251,6 @@ namespace VC {
}
}
- // proc name -> k -> interface variables
- public static Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;
- // proc name -> k -> VCExpr
- Dictionary<string, List<VCExpr>> procVcCopies;
-
- private void CreateCopiesForLazyInlining(int K, Program program)
- {
- interfaceVarCopies = new Dictionary<string, List<List<VCExprVar>>>();
- procVcCopies = new Dictionary<string, List<VCExpr>>();
-
- // Duplicate VCs of each procedure K times and remove quantifiers
- Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);
- foreach (LazyInliningInfo info in implName2LazyInliningInfo.Values)
- {
- Contract.Assert(info != null);
- CreateCopyForLazyInlining(K, program, info, checker);
- }
-
- // Change the procedure calls in each VC
- // Push all to the theorem prover
- var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies);
- foreach (var kvp in procVcCopies)
- {
- for (int i = 0; i < kvp.Value.Count; i++)
- {
- kvp.Value[i] = bm.Mutate(kvp.Value[i], true);
- checker.TheoremProver.PushVCExpression(kvp.Value[i]);
- }
- }
- }
-
- public class BoundingVCMutator : MutatingVCExprVisitor<bool>
- {
- // proc name -> k -> interface variables
- Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;
-
- public BoundingVCMutator(VCExpressionGenerator gen, Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies)
- : base(gen)
- {
- Contract.Requires(gen != null);
- this.interfaceVarCopies = interfaceVarCopies;
- }
-
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- bool arg)
- {
- //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr node;
- if (changed)
- node = Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- node = originalNode;
-
- var expr = node as VCExprNAry;
- if (expr == null) return node;
- var op = expr.Op as VCExprBoogieFunctionOp;
- if (op == null) return node;
- if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return node;
-
- // substitute
- var K = interfaceVarCopies[op.Func.Name].Count;
-
-
- VCExpr ret = VCExpressionGenerator.False;
- for (int k = 0; k < K; k++)
- {
- var iv = interfaceVarCopies[op.Func.Name][k];
- Contract.Assert(op.Arity == iv.Count);
-
- VCExpr conj = VCExpressionGenerator.True;
- for (int i = 0; i < iv.Count; i++)
- {
- var c = Gen.Eq(expr[i], iv[i]);
- conj = Gen.And(conj, c);
- }
- ret = Gen.Or(conj, ret);
- }
-
- return ret;
- }
-
- } // end BoundingVCMutator
-
- private static int newVarCnt = 0;
-
- private void CreateCopyForLazyInlining(int K, Program program, LazyInliningInfo info, Checker checker)
- {
- var translator = checker.TheoremProver.Context.BoogieExprTranslator;
- interfaceVarCopies.Add(info.impl.Name, new List<List<VCExprVar>>());
- procVcCopies.Add(info.impl.Name, new List<VCExpr>());
-
- for (int k = 0; k < K; k++)
- {
- var expr = info.inside_vc;
- // Instantiate the "forall" variables
- Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();
- var ls = new List<VCExprVar>();
- for (int i = 0; i < info.interfaceVars.Count; i++)
- {
- var v = translator.LookupVariable(info.interfaceVars[i]);
- string newName = v.Name + "_fa_" + k.ToString() + "_" + newVarCnt.ToString();
- newVarCnt++;
- //checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
- var vp = checker.VCExprGen.Variable(newName, v.Type);
- substForallDict.Add(v, vp);
- ls.Add(vp);
- }
- interfaceVarCopies[info.impl.Name].Add(ls);
- VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
-
- SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen);
- Contract.Assert(subst != null);
- expr = subst.Mutate(expr, substForall);
-
- // Instantiate and declare the "exists" variables
- Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();
- foreach (VCExprVar v in info.privateVars)
- {
- Contract.Assert(v != null);
- string newName = v.Name + "_te_" + k.ToString() + "_" + newVarCnt.ToString();
- newVarCnt++;
- checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
- substExistsDict.Add(v, checker.VCExprGen.Variable(newName, v.Type));
- }
- VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
-
- subst = new SubstitutingVCExprVisitor(checker.VCExprGen);
- expr = subst.Mutate(expr, substExists);
-
- procVcCopies[info.impl.Name].Add(expr);
- }
- }
-
private void GenerateVCForLazyInlining(Program program, LazyInliningInfo info, Checker checker) {
Contract.Requires(program != null);
Contract.Requires(info != null);
@@ -389,7 +275,7 @@ namespace VC {
ResetPredecessors(impl.Blocks);
VCExpr reachvcexpr = GenerateReachVC(impl, info, checker);
vcexpr = gen.And(vcexpr, reachvcexpr);
-
+
List<VCExprVar> privateVars = new List<VCExprVar>();
foreach (Variable v in impl.LocVars) {
Contract.Assert(v != null);
@@ -401,7 +287,6 @@ namespace VC {
}
info.privateVars = privateVars;
- info.inside_vc = vcexpr;
if (privateVars.Count > 0) {
vcexpr = gen.Exists(new List<TypeVariable>(), privateVars, new List<VCTrigger>(),
@@ -421,12 +306,7 @@ namespace VC {
Function function = cce.NonNull(info.function);
VCExpr expr = gen.Function(function, interfaceExprs);
Contract.Assert(expr != null);
- if (CommandLineOptions.Clo.LazyInlining == 1) {
- vcexpr = gen.Implies(expr, vcexpr);
- } else {
- //Contract.Assert(CommandLineOptions.Clo.LazyInlining == 2);
- vcexpr = gen.Eq(expr, vcexpr);
- }
+ vcexpr = gen.Implies(expr, vcexpr);
List<VCTrigger> triggers = new List<VCTrigger>();
List<VCExpr> exprs = new List<VCExpr>();
@@ -442,10 +322,7 @@ namespace VC {
new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr);
info.vcexpr = vcexpr;
- if (CommandLineOptions.Clo.LazyInlining != 3)
- {
- checker.TheoremProver.PushVCExpression(vcexpr);
- }
+ checker.TheoremProver.PushVCExpression(vcexpr);
}
protected VCExpr GenerateReachVC(Implementation impl, LazyInliningInfo info, Checker ch) {
@@ -1662,12 +1539,6 @@ namespace VC {
VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);
Contract.Assert(vc != null);
- if (CommandLineOptions.Clo.LazyInlining == 3)
- {
- var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies);
- vc = bm.Mutate(vc, true);
- }
-
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);
} else {
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 14:06:42 +0000