From d335ace6437fb1639bea6f425811b9b54936d141 Mon Sep 17 00:00:00 2001 From: akashlal Date: Wed, 24 Sep 2014 15:04:51 +0530 Subject: Simple VC generation for SI --- Source/VCGeneration/StratifiedVC.cs | 254 +++++++++++++++++++++++++++++++----- 1 file changed, 223 insertions(+), 31 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index a9745b3c..184a2225 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -195,7 +195,8 @@ namespace VC { public Implementation impl; public Function function; public Variable controlFlowVariable; - public AssertCmd exitAssertCmd; + public Dictionary blockToControlVar; + public Cmd exitAssertCmd; public VCExpr vcexpr; public List interfaceExprVars; public List privateExprVars; @@ -252,8 +253,148 @@ namespace VC { initialized = false; } + public void GenerateVCBoolControl() + { + Debug.Assert(!initialized); + Debug.Assert(CommandLineOptions.Clo.SIBoolControlVC); + + // fix names for exit variables + var outputVariables = new List(); + var assertConjuncts = new List(); + foreach (Variable v in impl.OutParams) + { + Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type)); + outputVariables.Add(c); + Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v)); + assertConjuncts.Add(eqExpr); + } + foreach (IdentifierExpr e in impl.Proc.Modifies) + { + if (e.Decl == null) continue; + Variable v = e.Decl; + Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type)); + outputVariables.Add(c); + Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v)); + assertConjuncts.Add(eqExpr); + } + exitAssertCmd = new AssumeCmd(Token.NoToken, Expr.BinaryTreeAnd(assertConjuncts)); + (exitAssertCmd as AssumeCmd).Attributes = new QKeyValue(Token.NoToken, "exitAssert", new List(), null); + + // no need for label2absy + label2absy = new Dictionary(); + + // Passify + Program program = vcgen.program; + ProverInterface proverInterface = vcgen.prover; + vcgen.ConvertCFG2DAG(impl); + vcgen.PassifyImpl(impl, out mvInfo); + + VCExpressionGenerator gen = proverInterface.VCExprGen; + var exprGen = proverInterface.Context.ExprGen; + var translator = proverInterface.Context.BoogieExprTranslator; + + // add a boolean variable at each call site + vcgen.InstrumentCallSites(impl); + + // typecheck + var tc = new TypecheckingContext(null); + impl.Typecheck(tc); + + /////////////////// + // Generate the VC + /////////////////// + + // block -> bool variable + blockToControlVar = new Dictionary(); + foreach (var b in impl.Blocks) + blockToControlVar.Add(b, gen.Variable(b.Label + "_holds", Bpl.Type.Bool)); + + vcexpr = VCExpressionGenerator.True; + foreach (var b in impl.Blocks) + { + // conjoin all assume cmds + VCExpr c = VCExpressionGenerator.True; + foreach (var cmd in b.Cmds) + { + var acmd = cmd as AssumeCmd; + if (acmd == null) + { + Debug.Assert(cmd is AssertCmd && (cmd as AssertCmd).Expr is LiteralExpr && + ((cmd as AssertCmd).Expr as LiteralExpr).IsTrue); + continue; + } + var expr = translator.Translate(acmd.Expr); + // Label the assume if it is a procedure call + NAryExpr naryExpr = acmd.Expr as NAryExpr; + if (naryExpr != null && naryExpr.Fun is FunctionCall) + { + var id = acmd.UniqueId; + label2absy[id] = acmd; + expr = gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), expr); + } + + c = gen.AndSimp(c, expr); + } + vcexpr = gen.AndSimp(vcexpr, gen.Eq(blockToControlVar[b], c)); + + // block implies a disjunction of successors + Debug.Assert(!(b.TransferCmd is ReturnExprCmd), "Not supported"); + var gc = b.TransferCmd as GotoCmd; + if (gc != null) + { + VCExpr succ = VCExpressionGenerator.False; + foreach (var sb in gc.labelTargets) + succ = gen.OrSimp(succ, blockToControlVar[sb]); + vcexpr = gen.AndSimp(vcexpr, succ); + } + else + { + // nothing to do + } + } + // assert start block + vcexpr = gen.AndSimp(vcexpr, blockToControlVar[impl.Blocks[0]]); + + //Console.WriteLine("VC of {0}: {1}", impl.Name, vcexpr); + // Collect other information + callSites = vcgen.CollectCallSites(impl); + recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl); + + // record interface variables + privateExprVars = new List(); + foreach (Variable v in impl.LocVars) + { + privateExprVars.Add(translator.LookupVariable(v)); + } + foreach (Variable v in impl.OutParams) + { + privateExprVars.Add(translator.LookupVariable(v)); + } + privateExprVars.AddRange(blockToControlVar.Values); + + interfaceExprVars = new List(); + foreach (Variable v in program.GlobalVariables()) + { + interfaceExprVars.Add(translator.LookupVariable(v)); + } + foreach (Variable v in impl.InParams) + { + interfaceExprVars.Add(translator.LookupVariable(v)); + } + foreach (Variable v in outputVariables) + { + interfaceExprVars.Add(translator.LookupVariable(v)); + } + } + public void GenerateVC() { if (initialized) return; + if (CommandLineOptions.Clo.SIBoolControlVC) + { + GenerateVCBoolControl(); + initialized = true; + return; + } List outputVariables = new List(); List assertConjuncts = new List(); foreach (Variable v in impl.OutParams) { @@ -464,9 +605,8 @@ namespace VC { // Used inside PassifyImpl protected override void addExitAssert(string implName, Block exitBlock) { if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) { - AssertCmd exitAssertCmd = implName2StratifiedInliningInfo[implName].exitAssertCmd; - Contract.Assert(exitAssertCmd != null); - exitBlock.Cmds.Add(exitAssertCmd); + var exitAssertCmd = implName2StratifiedInliningInfo[implName].exitAssertCmd; + if(exitAssertCmd != null) exitBlock.Cmds.Add(exitAssertCmd); } } @@ -1075,7 +1215,12 @@ namespace VC { reporter.SetCandidateHandler(calls); calls.id2VC.Add(0, vc); calls.extraRecursion = extraRecBound; - + if (CommandLineOptions.Clo.SIBoolControlVC) + { + calls.candiate2block2controlVar.Add(0, new Dictionary()); + implName2StratifiedInliningInfo[impl.Name].blockToControlVar.Iter(tup => + calls.candiate2block2controlVar[0].Add(tup.Key, tup.Value)); + } // Identify summary candidates: Match ensure clauses with the appropriate call site if (useSummary) calls.matchSummaries(); @@ -1468,6 +1613,16 @@ namespace VC { prover.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null); substExistsDict.Add(v, prover.VCExprGen.Variable(newName, v.Type)); } + if (CommandLineOptions.Clo.SIBoolControlVC) + { + // record the mapping for control booleans (for tracing the path later) + calls.candiate2block2controlVar[id] = new Dictionary(); + foreach (var tup in info.blockToControlVar) + { + calls.candiate2block2controlVar[id].Add(tup.Key, + substExistsDict[tup.Value]); + } + } if (CommandLineOptions.Clo.ModelViewFile != null) { SaveSubstitution(vState, id, substForallDict, substExistsDict); } @@ -1550,6 +1705,8 @@ namespace VC { public Dictionary/*!*/ id2ControlVar; public Dictionary id2VC; public Dictionary/*!*/ label2Id; + // candidate to block to Bool Control variable + public Dictionary> candiate2block2controlVar; // Stores the candidate from which this one originated public Dictionary candidateParent; // Mapping from candidate Id to the "si_unique_call" id that led to @@ -1630,6 +1787,7 @@ namespace VC { recentlyAddedCandidates = new HashSet(); argExprMap = new Dictionary(); recordExpr2Var = new Dictionary(); + candiate2block2controlVar = new Dictionary>(); forcedCandidates = new HashSet(); extraRecursion = new Dictionary(); @@ -1884,6 +2042,8 @@ namespace VC { int candidateId = GetNewId(callExpr); boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId; candidateParent[candidateId] = currInlineCount; + candiate2block2controlVar[candidateId] = new Dictionary(); + string label = GetLabel(candidateId); var unique_call_id = QKeyValue.FindIntAttribute(acmd.Attributes, "si_unique_call", -1); if (unique_call_id != -1) @@ -2049,7 +2209,6 @@ namespace VC { FCallHandler calls; StratifiedInliningInfo mainInfo; StratifiedVC mainVC; - Counterexample CexTrace; public bool underapproximationMode; public List candidatesToExpand; @@ -2079,7 +2238,6 @@ namespace VC { this.underapproximationMode = false; this.calls = null; this.candidatesToExpand = new List(); - this.CexTrace = null; } public StratifiedInliningErrorReporter(Dictionary implName2StratifiedInliningInfo, @@ -2095,7 +2253,6 @@ namespace VC { this.mainVC = mainVC; this.underapproximationMode = false; this.candidatesToExpand = new List(); - this.CexTrace = null; } public void SetCandidateHandler(FCallHandler calls) { @@ -2256,25 +2413,56 @@ namespace VC { Hashtable traceNodes = new Hashtable(); - foreach (string s in labels) { - Contract.Assert(s != null); - var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId); - - if (absylabel == null) continue; - - Absy absy; - - if (candidateId == 0) { - absy = Label2Absy(absylabel); - } - else { - absy = Label2Absy(procImpl.Name, absylabel); - } - - if (traceNodes.ContainsKey(absy)) - System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes"); - else - traceNodes.Add(absy, null); + if (!CommandLineOptions.Clo.SIBoolControlVC) + { + foreach (string s in labels) + { + Contract.Assert(s != null); + var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId); + + if (absylabel == null) continue; + + Absy absy; + + if (candidateId == 0) + { + absy = Label2Absy(absylabel); + } + else + { + absy = Label2Absy(procImpl.Name, absylabel); + } + + if (traceNodes.ContainsKey(absy)) + System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes"); + else + traceNodes.Add(absy, null); + } + } + else + { + Debug.Assert(CommandLineOptions.Clo.UseProverEvaluate, "Must use prover evaluate option with boolControlVC"); + var block = procImpl.Blocks[0]; + traceNodes.Add(block, null); + while (true) + { + var gc = block.TransferCmd as GotoCmd; + if (gc == null) break; + Block next = null; + foreach (var succ in gc.labelTargets) + { + var succtaken = (bool) theoremProver.Evaluate(calls.candiate2block2controlVar[candidateId][succ]); + if (succtaken) + { + next = succ; + traceNodes.Add(succ, null); + break; + } + } + Debug.Assert(next != null, "Must find a successor"); + Debug.Assert(traceNodes.ContainsKey(next), "CFG cannot be cyclic"); + block = next; + } } List trace = new List(); @@ -2307,10 +2495,14 @@ namespace VC { Cmd cmd = cce.NonNull(cmds[i]); // Skip if 'cmd' not contained in the trace or not an assert - if (cmd is AssertCmd && traceNodes.Contains(cmd)) { - Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, theoremProver.Context); - newCounterexample.AddCalleeCounterexample(calleeCounterexamples); - return newCounterexample; + if ((cmd is AssertCmd && traceNodes.Contains(cmd)) || + (cmd is AssumeCmd && QKeyValue.FindBoolAttribute((cmd as AssumeCmd).Attributes, "exitAssert"))) + { + var acmd = cmd as AssertCmd; + if (acmd == null) { acmd = new AssertCmd(Token.NoToken, Expr.True); } + Counterexample newCounterexample = AssertCmdToCounterexample(acmd, transferCmd, trace, errModel, mvInfo, theoremProver.Context); + newCounterexample.AddCalleeCounterexample(calleeCounterexamples); + return newCounterexample; } // Counterexample generation for inlined procedures -- cgit v1.2.3