diff options
| author |  Unknown <kenmcmil@A3539013.redmond.corp.microsoft.com> | 2013-05-07 18:26:25 -0700 |
|---|---|---|
| committer | Unknown <kenmcmil@A3539013.redmond.corp.microsoft.com> | 2013-05-07 18:26:25 -0700 |
| commit | 429608680e4b6b65c9a75e9f1ca72963778983ed (patch) | |
| tree | 16ce1a4131d1ef6da057b2d2778caf9726742632 | |
| parent | 993c115277bcf6c23c9a8982e97bf1d63c6182a9 (diff) | |
new files for fixedpoint engine backend
| -rw-r--r-- | Source/VCGeneration/ExprExtensions.cs | 203 | ||||
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 1643 | ||||
| -rw-r--r-- | Source/VCGeneration/RPFP.cs | 558 |
3 files changed, 2404 insertions, 0 deletions
diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs new file mode 100644 index 00000000..67837833 --- /dev/null +++ b/Source/VCGeneration/ExprExtensions.cs @@ -0,0 +1,203 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) 2012 Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using Term = Microsoft.Boogie.VCExprAST.VCExpr;
+using FuncDecl = Microsoft.Boogie.VCExprAST.VCExprOp;
+using Sort = Microsoft.Boogie.Type;
+using Microsoft.Boogie.VCExprAST;
+
+
+/** This namespace contains some extensions to allow VCExpr to provide the
+ * interface needed by RPFP and FixedpointVC. */
+
+namespace Microsoft.Boogie.ExprExtensions
+{
+
+ public enum TermKind { App, Other };
+
+ public enum DeclKind { Uninterpreted, And, Implies, Label, Other };
+
+ public static class MyExtensions
+ {
+ public static Term[] GetAppArgs(this Term t)
+ {
+ Microsoft.Boogie.VCExprAST.VCExprNAry tn = t as Microsoft.Boogie.VCExprAST.VCExprNAry;
+ return tn.ToArray();
+ }
+
+ public static FuncDecl GetAppDecl(this Term t)
+ {
+ Microsoft.Boogie.VCExprAST.VCExprNAry tn = t as Microsoft.Boogie.VCExprAST.VCExprNAry;
+ return tn.Op;
+ }
+
+ public static string GetDeclName(this FuncDecl f)
+ {
+ return (f as VCExprBoogieFunctionOp).Func.Name; //TODO
+ }
+
+ public static DeclKind GetKind(this FuncDecl f)
+ {
+ if (f is VCExprBoogieFunctionOp)
+ return DeclKind.Uninterpreted;
+ if (f == VCExpressionGenerator.AndOp)
+ return DeclKind.And;
+ if (f == VCExpressionGenerator.ImpliesOp)
+ return DeclKind.Implies;
+ if (f is VCExprLabelOp)
+ return DeclKind.Label;
+ return DeclKind.Other;
+ }
+
+ public static bool IsLabel(this Term t)
+ {
+ return (t is VCExprNAry) && (GetAppDecl(t) is VCExprLabelOp);
+ }
+
+ public static string LabelName(this Term t)
+ {
+ return (GetAppDecl(t) as VCExprLabelOp).label;
+ }
+
+ public static Sort GetSort(this Term t)
+ {
+ return t.Type;
+ }
+
+ public static TermKind GetKind(this Term t)
+ {
+ if (t is Microsoft.Boogie.VCExprAST.VCExprNAry)
+ return TermKind.App;
+ return TermKind.Other;
+ }
+
+ public static bool IsFunctionApp(this Term t)
+ {
+ return t.GetKind() == TermKind.App && t.GetAppDecl().GetKind() == DeclKind.Uninterpreted;
+ }
+
+ public static bool IsFalse(this Term t)
+ {
+ return t == VCExpressionGenerator.False;
+ }
+
+ public static Term VCExprToTerm(this Microsoft.Boogie.ProverContext ctx, VCExpr e, LineariserOptions lin){
+ return e;
+ }
+
+ }
+
+ public class Context : Microsoft.Boogie.VCExpressionGenerator
+ {
+ public Term MkTrue()
+ {
+ return VCExpressionGenerator.True;
+ }
+
+ public Term MkFalse()
+ {
+ return VCExpressionGenerator.False;
+ }
+
+
+ public List<Term> axioms = new List<Term>();
+
+ public void AddAxiom(Term ax)
+ {
+ axioms.Add(ax);
+ }
+
+ public void RemoveAxiom(Term ax)
+ {
+ axioms.Remove(ax);
+ }
+
+ public FuncDecl MkFuncDecl(string name, FuncDecl f)
+ {
+ Function h = (f as VCExprBoogieFunctionOp).Func;
+ Function g = new Function(Token.NoToken, name, h.InParams, h.OutParams[0]);
+ return BoogieFunctionOp(g);
+ }
+
+ public FuncDecl MkFuncDecl(string name, Sort rng)
+ {
+ Function g = new Function(Token.NoToken, name, new VariableSeq(), new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "dummy",rng)));
+ return BoogieFunctionOp(g);
+ }
+
+ public Term MkApp(FuncDecl f, Term[] args)
+ {
+ return Function(f, args);
+ }
+
+ public Term MkApp(FuncDecl f, Term arg)
+ {
+ return Function(f, arg);
+ }
+
+ public Term MkAnd(Term[] args)
+ {
+ if (args.Length == 0) return True;
+ Term res = args[0];
+ for (int i = 1; i < args.Length; i++)
+ res = And(res, args[i]);
+ return res;
+ }
+
+ public Term MkAnd(Term arg1, Term arg2)
+ {
+ return And(arg1, arg2);
+ }
+
+
+ public Term MkNot(Term arg1)
+ {
+ return Not(arg1);
+ }
+
+ public Term MkImplies(Term arg1, Term arg2)
+ {
+ return Implies(arg1, arg2);
+ }
+
+ public Term MkEq(Term arg1, Term arg2)
+ {
+ return Eq(arg1, arg2);
+ }
+
+ public Sort MkBoolSort()
+ {
+ return Type.Bool;
+ }
+
+ public Term MkConst(string name, Sort sort)
+ {
+ return Variable(name, sort);
+ }
+
+ public Term MkForall(Term[] bounds, Term body)
+ {
+ List<VCExprVar> vbs = new List<VCExprVar>();
+ foreach(var v in bounds)
+ vbs.Add(v as VCExprVar);
+ return Forall(vbs,new List<VCTrigger>(), body);
+ }
+
+ public Term MkExists(Term[] bounds, Term body)
+ {
+ List<VCExprVar> vbs = new List<VCExprVar>();
+ foreach (var v in bounds)
+ vbs.Add(v as VCExprVar);
+ return Exists(vbs, new List<VCTrigger>(), body);
+ }
+ };
+}
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs new file mode 100644 index 00000000..adc801d5 --- /dev/null +++ b/Source/VCGeneration/FixedpointVC.cs @@ -0,0 +1,1643 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) 2012 Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.IO;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+
+
+using Term = Microsoft.Boogie.VCExprAST.VCExpr;
+using FuncDecl = Microsoft.Boogie.VCExprAST.VCExprOp;
+using Sort = Microsoft.Boogie.Type;
+using Microsoft.Boogie.ExprExtensions;
+
+
+namespace Microsoft.Boogie
+{
+ public class FixedpointVC : VC.VCGen
+ {
+
+ public class AnnotationInfo
+ {
+ public enum AnnotationType { LoopInvariant, ProcedureSummary };
+ public string filename;
+ public int lineno;
+ public string[] argnames;
+ public AnnotationType type;
+ };
+
+ static bool NoLabels = false;
+
+ // options
+ bool largeblock = false;
+
+ public bool SetOption(string option, string value)
+ {
+ if (option == "LargeBlock")
+ {
+ largeblock = true;
+ return true;
+ }
+ return false;
+ }
+
+ Context ctx;
+ RPFP rpfp;
+ Program program;
+ Microsoft.Boogie.ProverContext boogieContext;
+ Microsoft.Boogie.VCExpressionGenerator gen;
+ public readonly static string recordProcName = "boogie_si_record"; // TODO: this really needed?
+ private Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo
+ = new Dictionary<string, StratifiedInliningInfo>();
+ Checker checker;
+ // Microsoft.Boogie.Z3.Z3InstanceOptions options = new Microsoft.Boogie.Z3.Z3InstanceOptions(); // TODO: what?
+ LineariserOptions linOptions;
+ Dictionary<FuncDecl, StratifiedInliningInfo> relationToProc = new Dictionary<FuncDecl, StratifiedInliningInfo>();
+ Dictionary<string, Term> labels = new Dictionary<string, Term> ();
+ List<Term> DualityVCs = new List<Term>();
+ Dictionary<string, bool> summaries = new Dictionary<string, bool>();
+ string main_proc_name = "main";
+
+
+
+ public enum Mode { Corral, OldCorral, Boogie};
+ public enum AnnotationStyle { Flat, Procedure, Call };
+
+ Mode mode;
+ AnnotationStyle style;
+
+ public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile)
+ : base(_program, logFilePath, appendLogFile)
+ {
+ switch (CommandLineOptions.Clo.FixedPointMode)
+ {
+ case CommandLineOptions.FixedPointInferenceMode.Corral:
+ mode = Mode.Corral;
+ style = AnnotationStyle.Procedure;
+ break;
+ case CommandLineOptions.FixedPointInferenceMode.OldCorral:
+ mode = Mode.OldCorral;
+ style = AnnotationStyle.Procedure;
+ break;
+ case CommandLineOptions.FixedPointInferenceMode.Flat:
+ mode = Mode.Boogie;
+ style = AnnotationStyle.Flat;
+ break;
+ case CommandLineOptions.FixedPointInferenceMode.Procedure:
+ mode = Mode.Boogie;
+ style = AnnotationStyle.Procedure;
+ break;
+ case CommandLineOptions.FixedPointInferenceMode.Call:
+ mode = Mode.Boogie;
+ style = AnnotationStyle.Call;
+ break;
+ }
+ ctx = new Context(); // TODO is this right?
+ rpfp = new RPFP(RPFP.CreateLogicSolver(ctx));
+ program = _program;
+ gen = ctx;
+ checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);
+ boogieContext = checker.TheoremProver.Context;
+ linOptions = null; // new Microsoft.Boogie.Z3.Z3LineariserOptions(false, options, new List<VCExprVar>());
+ }
+
+ Dictionary<string, AnnotationInfo> annotationInfo = new Dictionary<string, AnnotationInfo>();
+
+ public void AnnotateLoops(Implementation impl, ProverContext ctxt)
+ {
+ Contract.Requires(impl != null);
+
+ CurrentLocalVariables = impl.LocVars;
+ variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ incarnationOriginMap = new Dictionary<Incarnation, Absy>();
+
+ ResetPredecessors(impl.Blocks);
+
+ #region Create the graph by adding the source node and each edge
+ GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);
+ #endregion
+
+ //Graph<Block> g = program.ProcessLoops(impl);
+
+ g.ComputeLoops(); // this is the call that does all of the processing
+ if (!g.Reducible)
+ {
+ throw new System.Exception("Irreducible flow graphs are unsupported.");
+ }
+
+ #region add a symbolic annoation to every loop head
+ foreach (Block header in cce.NonNull(g.Headers))
+ AnnotateBlock(impl, ctxt, header);
+ #endregion
+ }
+
+ private void AnnotateCallSites(Implementation impl, ProverContext ctxt, Dictionary<string, bool> impls){
+ foreach (var b in impl.Blocks)
+ {
+ foreach (var cmd in b.Cmds)
+ {
+ if (cmd is CallCmd)
+ {
+ string name = (cmd as CallCmd).callee;
+ if(impls.ContainsKey(name))
+ goto annotate;
+ }
+ }
+ continue;
+ annotate:
+ AnnotateBlock(impl, ctxt, b);
+ }
+ }
+
+
+ private void AnnotateBlock(Implementation impl, ProverContext ctxt, Block header)
+ {
+ Contract.Assert(header != null);
+
+ string name = impl.Name + "_" + header.Label + "_invar";
+ if (annotationInfo.ContainsKey(name))
+ return;
+
+ // collect the variables needed in the invariant
+ ExprSeq exprs = new ExprSeq();
+ VariableSeq vars = new VariableSeq();
+ List<string> names = new List<string>();
+
+ if (style == AnnotationStyle.Flat)
+ {
+ // in flat mode, all live globals should be in live set
+#if false
+ foreach (Variable v in program.GlobalVariables())
+ {
+ vars.Add(v);
+ names.Add(v.ToString());
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+#endif
+ foreach (Variable v in /* impl.LocVars */ header.liveVarsBefore)
+ {
+ vars.Add(v);
+ names.Add(v.ToString());
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ }
+ else
+ {
+ foreach (Variable v in program.GlobalVariables())
+ {
+ vars.Add(v);
+ names.Add("@old_" + v.ToString());
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ }
+ foreach (IdentifierExpr ie in impl.Proc.Modifies)
+ {
+ if (ie.Decl == null)
+ continue;
+ vars.Add(ie.Decl);
+ names.Add(ie.Decl.ToString());
+ exprs.Add(ie);
+ }
+ foreach (Variable v in impl.Proc.InParams)
+ {
+ Contract.Assert(v != null);
+ vars.Add(v);
+ names.Add("@old_" + v.ToString());
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ }
+ foreach (Variable v in impl.LocVars)
+ {
+ vars.Add(v);
+ names.Add(v.ToString());
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ }
+
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);
+ Contract.Assert(ti != null);
+ Formal returnVar = new Formal(Token.NoToken, ti, false);
+ Contract.Assert(returnVar != null);
+ var function = new Function(Token.NoToken, name, vars, returnVar);
+ ctxt.DeclareFunction(function, "");
+
+ Expr invarExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
+ var invarAssertion = new AssertCmd(Token.NoToken, invarExpr);
+ CmdSeq newCmds = new CmdSeq();
+ newCmds.Add(invarAssertion);
+
+ // make a record in annotationInfo;
+ var info = new AnnotationInfo();
+ info.filename = header.tok.filename;
+ info.lineno = header.Line;
+ info.argnames = names.ToArray();
+ info.type = AnnotationInfo.AnnotationType.LoopInvariant;
+ annotationInfo.Add(name, info);
+ // get file and line info from havoc, if there is...
+ if (header.Cmds.Length > 0)
+ {
+ PredicateCmd bif = header.Cmds[0] as PredicateCmd;
+ if (bif != null)
+ {
+ string foo = QKeyValue.FindStringAttribute(bif.Attributes, "sourcefile");
+ if (foo != null)
+ info.filename = foo;
+ int bar = QKeyValue.FindIntAttribute(bif.Attributes, "sourceline", -1);
+ if (bar != -1)
+ info.lineno = bar;
+ }
+ }
+ var thing = header;
+ foreach (Cmd c in header.Cmds)
+ {
+ newCmds.Add(c);
+ }
+ header.Cmds = newCmds;
+ }
+
+#if true
+
+ public void AnnotateProcEnsures(Procedure proc, Implementation impl, ProverContext ctxt)
+ {
+ Contract.Requires(impl != null);
+
+ CurrentLocalVariables = impl.LocVars;
+
+ // collect the variables needed in the invariant
+ ExprSeq exprs = new ExprSeq();
+ VariableSeq vars = new VariableSeq();
+ List<string> names = new List<string>();
+
+ foreach (Variable v in program.GlobalVariables())
+ {
+ vars.Add(v);
+ exprs.Add(new OldExpr(Token.NoToken,new IdentifierExpr(Token.NoToken, v)));
+ names.Add(v.Name);
+ }
+ foreach (IdentifierExpr ie in proc.Modifies)
+ {
+ if (ie.Decl == null)
+ continue;
+ vars.Add(ie.Decl);
+ exprs.Add(ie);
+ names.Add(ie.Decl.Name + "_out");
+ }
+ foreach (Variable v in proc.InParams)
+ {
+ Contract.Assert(v != null);
+ vars.Add(v);
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ names.Add(v.Name);
+ }
+ foreach (Variable v in proc.OutParams)
+ {
+ Contract.Assert(v != null);
+ vars.Add(v);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ names.Add(v.Name);
+ }
+ string name = impl.Name + "_summary";
+ summaries.Add(name, true);
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);
+ Contract.Assert(ti != null);
+ Formal returnVar = new Formal(Token.NoToken, ti, false);
+ Contract.Assert(returnVar != null);
+ var function = new Function(Token.NoToken, name, vars, returnVar);
+ ctxt.DeclareFunction(function, "");
+
+ Expr invarExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
+
+ proc.Ensures.Add(new Ensures(Token.NoToken, false, invarExpr, "", null));
+
+ var info = new AnnotationInfo();
+ info.filename = proc.tok.filename;
+ info.lineno = proc.Line;
+ info.argnames = names.ToArray();
+ info.type = AnnotationInfo.AnnotationType.ProcedureSummary;
+ annotationInfo.Add(name, info);
+ }
+#endif
+
+ void InlineAll()
+ {
+ foreach (var d in program.TopLevelDeclarations)
+ {
+ var impl = d as Implementation;
+ if (impl != null)
+ {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ if(impl.Name != main_proc_name)
+ if(impl.FindExprAttribute("inline") == null)
+ impl.AddAttribute("inline", Expr.Literal(100));
+ }
+ }
+ foreach (var d in program.TopLevelDeclarations)
+ {
+ var impl = d as Implementation;
+ if (impl != null && !impl.SkipVerification)
+ {
+ Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (var d in program.TopLevelDeclarations)
+ {
+ var impl = d as Implementation;
+ if (impl != null)
+ {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+
+ public class LazyInliningInfo
+ {
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(impl != null);
+ Contract.Invariant(function != null);
+ Contract.Invariant(controlFlowVariable != null);
+ Contract.Invariant(assertExpr != null);
+ Contract.Invariant(cce.NonNullElements(interfaceVars));
+ Contract.Invariant(incarnationOriginMap == null || cce.NonNullDictionaryAndValues(incarnationOriginMap));
+ }
+
+ public Implementation impl;
+ public int uniqueId;
+ public Function function;
+ public Variable controlFlowVariable;
+ public List<Variable> interfaceVars;
+ public List<List<Variable>> interfaceVarCopies;
+ public Expr assertExpr;
+ public VCExpr vcexpr;
+ public List<VCExprVar> privateVars;
+ public Dictionary<Incarnation, Absy> incarnationOriginMap;
+ public Hashtable /*Variable->Expr*/ exitIncarnationMap;
+ public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins;
+ public Hashtable/*<int, Absy!>*/ label2absy;
+ public VC.ModelViewInfo mvInfo;
+
+ public Dictionary<Block, VCExprVar> reachVars;
+ public List<VCExprLetBinding> reachVarBindings;
+ public Variable inputErrorVariable;
+ public Variable outputErrorVariable;
+
+
+
+ public LazyInliningInfo(Implementation impl, Program program, ProverContext ctxt, int uniqueId, GlobalVariable errorVariable)
+ {
+ Contract.Requires(impl != null);
+ Contract.Requires(program != null);
+ Procedure proc = cce.NonNull(impl.Proc);
+
+ this.impl = impl;
+ this.uniqueId = uniqueId;
+ this.controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "cfc", Microsoft.Boogie.Type.Int));
+ impl.LocVars.Add(controlFlowVariable);
+
+ List<Variable> interfaceVars = new List<Variable>();
+ Expr assertExpr = new LiteralExpr(Token.NoToken, true);
+ Contract.Assert(assertExpr != null);
+ foreach (Variable v in program.GlobalVariables())
+ {
+ Contract.Assert(v != null);
+ interfaceVars.Add(v);
+ if (v.Name == "error")
+ inputErrorVariable = v;
+ }
+ // InParams must be obtained from impl and not proc
+ foreach (Variable v in impl.InParams)
+ {
+ Contract.Assert(v != null);
+ interfaceVars.Add(v);
+ }
+ // OutParams must be obtained from impl and not proc
+ foreach (Variable v in impl.OutParams)
+ {
+ Contract.Assert(v != null);
+ Constant c = new Constant(Token.NoToken,
+ new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
+ interfaceVars.Add(c);
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertExpr = Expr.And(assertExpr, eqExpr);
+ }
+ if (errorVariable != null)
+ {
+ proc.Modifies.Add(new IdentifierExpr(Token.NoToken, errorVariable));
+ }
+ foreach (IdentifierExpr e in proc.Modifies)
+ {
+ Contract.Assert(e != null);
+ 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));
+ interfaceVars.Add(c);
+ if (v.Name == "error")
+ {
+ outputErrorVariable = c;
+ continue;
+ }
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertExpr = Expr.And(assertExpr, eqExpr);
+ }
+
+ this.interfaceVars = interfaceVars;
+ this.assertExpr = Expr.Not(assertExpr);
+ VariableSeq functionInterfaceVars = new VariableSeq();
+ foreach (Variable v in interfaceVars)
+ {
+ Contract.Assert(v != null);
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true));
+ }
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);
+ Contract.Assert(ti != null);
+ Formal returnVar = new Formal(Token.NoToken, ti, false);
+ 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 */ 0; 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);
+ }
+ }
+ }
+ }
+
+ public class StratifiedInliningInfo : LazyInliningInfo
+ {
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(cce.NonNullElements(privateVars));
+ Contract.Invariant(cce.NonNullElements(interfaceExprVars));
+ Contract.Invariant(cce.NonNullElements(interfaceExprVars));
+ }
+
+ // public StratifiedVCGenBase vcgen;
+ //public Implementation impl;
+ //public Program program;
+ //public ProverContext ctxt;
+ //public int uniqueid;
+ //public Function function;
+ //public Variable controlFlowVariable;
+ //public Expr assertExpr;
+ //public VCExpr vcexpr;
+ //public List<VCExprVar> interfaceExprVars;
+ //public List<VCExprVar> privateExprVars;
+ //public Hashtable/*<int, Absy!>*/ label2absy;
+ //public VC.ModelViewInfo mvInfo;
+ //public Dictionary<Block, List<CallSite>> callSites;
+ //public Dictionary<Block, List<CallSite>> recordProcCallSites;
+ //public IEnumerable<Block> sortedBlocks;
+ //public bool initialized { get; private set; }
+
+
+ public List<VCExprVar> interfaceExprVars;
+ public List<VCExprVar> privateVars;
+ public VCExpr funcExpr;
+ public VCExpr falseExpr;
+ public RPFP.Transformer F;
+ public RPFP.Node node;
+ public RPFP.Edge edge;
+ public bool isMain = false;
+ public Dictionary<Absy, string> label2absyInv;
+ public ProverContext ctxt;
+ public Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
+ public List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
+
+ public StratifiedInliningInfo(Implementation _impl, Program _program, ProverContext _ctxt, int _uniqueid)
+ : base(_impl,_program,_ctxt,_uniqueid,null){
+ Contract.Requires(_impl != null);
+ Contract.Requires(_program != null);
+ privateVars = new List<VCExprVar>();
+ interfaceExprVars = new List<VCExprVar>();
+ ctxt = _ctxt;
+ }
+
+ }
+
+ protected override void addExitAssert(string implName, Block exitBlock)
+ {
+ if (implName2StratifiedInliningInfo != null
+ && implName2StratifiedInliningInfo.ContainsKey(implName)
+ && !implName2StratifiedInliningInfo[implName].isMain)
+ {
+ if (mode == Mode.Boogie) return;
+ Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;
+ Contract.Assert(assertExpr != null);
+ exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
+ }
+ }
+
+#if false
+ protected override void storeIncarnationMaps(string implName, Hashtable exitIncarnationMap)
+ {
+ if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName))
+ {
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[implName];
+ Contract.Assert(info != null);
+ info.exitIncarnationMap = exitIncarnationMap;
+ info.incarnationOriginMap = this.incarnationOriginMap;
+ }
+ }
+#endif
+
+ public void GenerateVCsForStratifiedInlining()
+ {
+ Contract.Requires(program != null);
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Contract.Assert(decl != null);
+ Implementation impl = decl as Implementation;
+ if (impl == null)
+ continue;
+ Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");
+
+ Procedure proc = cce.NonNull(impl.Proc);
+
+ {
+ StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, boogieContext, QuantifierExpr.GetNextSkolemId());
+ implName2StratifiedInliningInfo[impl.Name] = info;
+ // We don't need controlFlowVariable for stratified Inlining
+ //impl.LocVars.Add(info.controlFlowVariable);
+ ExprSeq exprs = new ExprSeq();
+
+ if (mode != Mode.Boogie && QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
+ {
+ proc.Ensures.Add(new Ensures(Token.NoToken, true, Microsoft.Boogie.Expr.False, "", null));
+ info.assertExpr = Microsoft.Boogie.Expr.False;
+ // info.isMain = true;
+ }
+ else if (mode == Mode.Corral || proc.FindExprAttribute("inline") != null || proc is LoopProcedure)
+ {
+ foreach (Variable v in program.GlobalVariables())
+ {
+ Contract.Assert(v != null);
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ }
+ foreach (Variable v in proc.InParams)
+ {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (Variable v in proc.OutParams)
+ {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (IdentifierExpr ie in proc.Modifies)
+ {
+ Contract.Assert(ie != null);
+ if (ie.Decl == null)
+ continue;
+ exprs.Add(ie);
+ }
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);
+#if false
+ if(mode == Mode.Corral || mode == Mode.OldCorral)
+ proc.Ensures.Add(new Ensures(Token.NoToken, true, freePostExpr, "", new QKeyValue(Token.NoToken, "si_fcall", new List<object>(), null)));
+#endif
+ }
+ else // not marked "inline" must be main
+ {
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);
+ info.isMain = true;
+ }
+ }
+ }
+
+ if (mode == Mode.Boogie) return;
+
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ var proc = decl as Procedure;
+ if (proc == null) continue;
+ if (!proc.Name.StartsWith(recordProcName)) continue;
+ Contract.Assert(proc.InParams.Length == 1);
+
+ // Make a new function
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);
+ Contract.Assert(ti != null);
+ Formal returnVar = new Formal(Token.NoToken, ti, false);
+ Contract.Assert(returnVar != null);
+
+ // Get record type
+ var argtype = proc.InParams[0].TypedIdent.Type;
+
+ var ins = new VariableSeq();
+ ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));
+
+ var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);
+ boogieContext.DeclareFunction(recordFunc, "");
+
+ var exprs = new ExprSeq();
+ exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));
+
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);
+ proc.Ensures.Add(new Ensures(true, freePostExpr));
+ }
+ }
+
+ private Term ExtractSmallerVCsRec(Dictionary<Term, Term> memo, Term t, List<Term> small)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ var kind = t.GetKind();
+ if (kind == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ if (f.GetKind() == DeclKind.Implies){
+ var lhs = t.GetAppArgs()[0];
+ if(lhs.GetKind() == TermKind.App){
+ var r = lhs.GetAppDecl();
+ if (r.GetKind() == DeclKind.And)
+ {
+ Term q = t.GetAppArgs()[1];
+ var lhsargs = lhs.GetAppArgs();
+ for (int i = lhsargs.Length-1; i >= 0; --i)
+ {
+ q = ctx.MkImplies(lhsargs[i], q);
+ }
+ res = ExtractSmallerVCsRec(memo, q, small);
+ goto done;
+ }
+ if (r.GetKind() == DeclKind.Label)
+ {
+ var arg = lhs;
+ arg = lhs.GetAppArgs()[0];
+ if (!(arg.GetKind() == TermKind.App && arg.GetAppDecl().GetKind() == DeclKind.Uninterpreted))
+ goto normal;
+ if (!(annotationInfo.ContainsKey(arg.GetAppDecl().GetDeclName()) && annotationInfo[arg.GetAppDecl().GetDeclName()].type == AnnotationInfo.AnnotationType.LoopInvariant))
+ goto normal;
+ var sm = ctx.MkImplies(lhs, ExtractSmallerVCsRec(memo, t.GetAppArgs()[1], small));
+ small.Add(sm);
+ res = ctx.MkTrue();
+ goto done;
+ }
+ if (r.GetKind() == DeclKind.Uninterpreted)
+ {
+ var arg = lhs;
+ if (!(annotationInfo.ContainsKey(arg.GetAppDecl().GetDeclName()) && annotationInfo[arg.GetAppDecl().GetDeclName()].type == AnnotationInfo.AnnotationType.LoopInvariant))
+ goto normal;
+ var sm = ctx.MkImplies(lhs,ExtractSmallerVCsRec(memo,t.GetAppArgs()[1],small));
+ small.Add(sm);
+ res = ctx.MkTrue();
+ goto done;
+ }
+ }
+ normal:
+ res = ctx.MkImplies(lhs,ExtractSmallerVCsRec(memo,t.GetAppArgs()[1],small));
+ }
+ else if (f.GetKind() == DeclKind.And)
+ {
+ res = ctx.MkApp(f,t.GetAppArgs().Select(x => ExtractSmallerVCsRec(memo, x, small)).ToArray());
+ }
+ else
+ res = t;
+ }
+ else
+ res = t;
+ done:
+ memo.Add(t, res);
+ return res;
+ }
+
+ private void ExtractSmallerVCs(Term t, List<Term> small){
+ Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ Term top = ExtractSmallerVCsRec(memo, t, small);
+ small.Add(top);
+ }
+
+ private Dictionary<FuncDecl, int> goalNumbering = new Dictionary<FuncDecl, int>();
+
+ private Term NormalizeGoal(Term goal, FuncDecl label)
+ {
+ var f = goal.GetAppDecl();
+ var args = goal.GetAppArgs();
+ int number;
+ if (!goalNumbering.TryGetValue(f, out number))
+ {
+ number = goalNumbering.Count;
+ goalNumbering.Add(f, number);
+ }
+ Term[] tvars = new Term[args.Length];
+ Term[] eqns = new Term[args.Length];
+ AnnotationInfo info = null;
+ annotationInfo.TryGetValue(f.GetDeclName(), out info);
+ for (int i = 0; i < args.Length; i++)
+ {
+ string pname = (info == null) ? i.ToString() : info.argnames[i];
+ tvars[i] = ctx.MkConst("@a" + number.ToString() + "_" + pname, args[i].GetSort());
+ eqns[i] = ctx.MkEq(tvars[i], args[i]);
+ }
+ return ctx.MkImplies(ctx.MkAnd(eqns), ctx.MkApp(label, ctx.MkApp(f, tvars)));
+ }
+
+ private Term MergeGoalsRec(Dictionary<Term, Term> memo, Term t)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ var kind = t.GetKind();
+ if (kind == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ var args = t.GetAppArgs();
+ if (f.GetKind() == DeclKind.Implies)
+ {
+ res = ctx.MkImplies(args[0], MergeGoalsRec(memo, args[1]));
+ goto done;
+ }
+ else if (f.GetKind() == DeclKind.And)
+ {
+ args = args.Select(x => MergeGoalsRec(memo, x)).ToArray();
+ res = ctx.MkApp(f, args);
+ goto done;
+ }
+ else if (f.GetKind() == DeclKind.Label)
+ {
+ var arg = t.GetAppArgs()[0];
+ var r = arg.GetAppDecl();
+ if (r.GetKind() == DeclKind.Uninterpreted)
+ {
+ res = NormalizeGoal(arg, f);
+ goto done;
+ }
+ }
+ }
+ res = t;
+ done:
+ memo.Add(t, res);
+ return res;
+ }
+
+ private Term MergeGoals(Term t)
+ {
+ Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ return MergeGoalsRec(memo, t);
+ }
+
+ private Term CollectGoalsRec(Dictionary<Term, Term> memo, Term t, List<Term> goals, List<Term> cruft)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ var kind = t.GetKind();
+ if (kind == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ if (f.GetKind() == DeclKind.Implies)
+ {
+ CollectGoalsRec(memo, t.GetAppArgs()[1], goals, cruft);
+ goto done;
+ }
+ else if (f.GetKind() == DeclKind.And)
+ {
+ foreach (var arg in t.GetAppArgs())
+ {
+ CollectGoalsRec(memo, arg, goals, cruft);
+ }
+ goto done;
+ }
+ else if (f.GetKind() == DeclKind.Label)
+ {
+ var arg = t.GetAppArgs()[0];
+ var r = arg.GetAppDecl();
+ if (r.GetKind() == DeclKind.Uninterpreted)
+ {
+ if (memo.TryGetValue(arg, out res))
+ goto done;
+ if (!annotationInfo.ContainsKey(r.GetDeclName()) && !arg.GetAppDecl().GetDeclName().StartsWith("_solve_"))
+ goto done;
+ goals.Add(arg);
+ memo.Add(arg, arg);
+ goto done;
+ }
+ else
+ return CollectGoalsRec(memo, arg, goals, cruft);
+ }
+ else if (f.GetKind() == DeclKind.Uninterpreted)
+ {
+ string name = f.GetDeclName();
+ if (name.StartsWith("_solve_"))
+ {
+ if (memo.TryGetValue(t, out res))
+ goto done;
+ goals.Add(t);
+ memo.Add(t, t);
+ return t;
+ }
+ }
+ }
+ // else the goal must be cruft
+ cruft.Add(t);
+ done:
+ res = t; // just to return something
+ memo.Add(t, res);
+ return res;
+ }
+
+ private void CollectGoals(Term t, List<Term> goals, List<Term> cruft)
+ {
+ Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ CollectGoalsRec(memo, t.GetAppArgs()[1], goals, cruft);
+ }
+
+ private Term SubstRec(Dictionary<Term, Term> memo, Term t)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ var kind = t.GetKind();
+ if (kind == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ var args = t.GetAppArgs().Select(x => SubstRec(memo, x)).ToArray();
+ res = ctx.MkApp(f, args);
+ }
+ else res = t;
+ memo.Add(t, res);
+ return res;
+ }
+
+ private Term SubstRecGoals(Dictionary<Term, Term> memo, Term t)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ var kind = t.GetKind();
+ if (kind == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ var args = t.GetAppArgs();
+ if (f.GetKind() == DeclKind.Implies){
+ res = SubstRecGoals(memo, args[1]);
+ if (res != ctx.MkTrue())
+ res = ctx.MkImplies(args[0],res);
+ goto done;
+ }
+ else if (f.GetKind() == DeclKind.And)
+ {
+ args = args.Select(x => SubstRecGoals(memo, x)).ToArray();
+ args = args.Where(x => x != ctx.MkTrue()).ToArray();
+ res = ctx.MkAnd(args);
+ goto done;
+ }
+ else if (f.GetKind() == DeclKind.Label)
+ {
+ var arg = t.GetAppArgs()[0];
+ var r = arg.GetAppDecl();
+ if (r.GetKind() == DeclKind.Uninterpreted)
+ {
+ if (memo.TryGetValue(arg, out res))
+ {
+ if(res != ctx.MkTrue())
+ res = ctx.MkApp(f, res);
+ goto done;
+ }
+ }
+ else
+ {
+ res = ctx.MkApp(f, SubstRecGoals(memo, arg));
+ goto done;
+ }
+
+ }
+ // what's left could be cruft!
+ if (memo.TryGetValue(t, out res))
+ {
+ goto done;
+ }
+ }
+ res = t;
+ done:
+ memo.Add(t, res);
+ return res;
+ }
+
+ private void FactorVCs(Term t, List<Term> vcs)
+ {
+ List<Term> small = new List<Term>();
+ ExtractSmallerVCs(t, small);
+ foreach (var smm in small)
+ {
+ List<Term> goals = new List<Term>();
+ List<Term> cruft = new List<Term>();
+ var sm = largeblock ? MergeGoals(smm) : smm;
+ CollectGoals(sm, goals,cruft);
+ foreach (var goal in goals)
+ {
+ Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ foreach (var othergoal in goals)
+ memo.Add(othergoal, othergoal.Equals(goal) ? ctx.MkFalse() : ctx.MkTrue());
+ foreach (var thing in cruft)
+ memo.Add(thing, ctx.MkTrue());
+ var vc = SubstRecGoals(memo, sm);
+ vc = ctx.MkImplies(ctx.MkNot(vc), goal);
+ vcs.Add(vc);
+ }
+ {
+ Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ foreach (var othergoal in goals)
+ memo.Add(othergoal, ctx.MkTrue());
+ var vc = SubstRecGoals(memo, sm);
+ if (vc != ctx.MkTrue())
+ {
+ vc = ctx.MkImplies(ctx.MkNot(vc), ctx.MkFalse());
+ vcs.Add(vc);
+ }
+ }
+ }
+ }
+
+
+
+ private void GenerateVCForStratifiedInlining(Program program, StratifiedInliningInfo info, Checker checker)
+ {
+ Contract.Requires(program != null);
+ Contract.Requires(info != null);
+ Contract.Requires(checker != null);
+ Contract.Requires(info.impl != null);
+ Contract.Requires(info.impl.Proc != null);
+
+
+
+ Implementation impl = info.impl;
+ if (mode == Mode.Boogie && style == AnnotationStyle.Flat && impl.Name != main_proc_name)
+ return;
+ Contract.Assert(impl != null);
+ ConvertCFG2DAG(impl);
+ VC.ModelViewInfo mvInfo;
+ PassifyImpl(impl, out mvInfo);
+ Hashtable/*<int, Absy!>*/ label2absy = null;
+ VCExpressionGenerator gen = checker.VCExprGen;
+ Contract.Assert(gen != null);
+ VCExpr vcexpr;
+ if(NoLabels){
+ int assertionCount = 0;
+ VCExpr startCorrect = null; /* VC.VCGen.LetVC(cce.NonNull(impl.Blocks[0]), null, null, info.blockVariables, info.bindings,
+ info.ctxt, out assertionCount); */
+ vcexpr = gen.Let(info.bindings, startCorrect);
+ }
+ else vcexpr = GenerateVC(impl, null /* info.controlFlowVariable */, out label2absy, info.ctxt);
+ if(mode != Mode.Boogie)
+ vcexpr = gen.Not(vcexpr);
+ Contract.Assert(vcexpr != null);
+ info.label2absy = label2absy;
+ info.mvInfo = mvInfo;
+ List<VCExpr> interfaceExprs = new List<VCExpr>();
+
+ if (true || !info.isMain)
+ {
+ Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
+ Contract.Assert(translator != null);
+ info.privateVars = new List<VCExprVar>();
+ foreach (Variable v in impl.LocVars)
+ {
+ Contract.Assert(v != null);
+ info.privateVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in impl.OutParams)
+ {
+ Contract.Assert(v != null);
+ info.privateVars.Add(translator.LookupVariable(v));
+ }
+
+ info.interfaceExprVars = new List<VCExprVar>();
+
+ foreach (Variable v in info.interfaceVars)
+ {
+ Contract.Assert(v != null);
+ VCExprVar ev = translator.LookupVariable(v);
+ Contract.Assert(ev != null);
+ info.interfaceExprVars.Add(ev);
+ interfaceExprs.Add(ev);
+ }
+ }
+
+ Function function = cce.NonNull(info.function);
+ Contract.Assert(function != null);
+ info.funcExpr = gen.Function(function, interfaceExprs);
+ info.vcexpr = vcexpr;
+
+ if (mode == Mode.Boogie)
+ {
+ Term z3vc = boogieContext.VCExprToTerm(vcexpr, linOptions);
+ FactorVCs(z3vc, DualityVCs);
+ }
+ else
+ {
+ // Index the procedures by relational variable
+ FuncDecl R = boogieContext.VCExprToTerm(info.funcExpr, linOptions).GetAppDecl();
+ relationToProc.Add(R, info);
+ info.node = rpfp.CreateNode(boogieContext.VCExprToTerm(info.funcExpr, linOptions));
+ if (info.isMain || QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
+ info.node.Bound.Formula = ctx.MkFalse();
+ }
+ }
+
+ // This returns a new FuncDel with same sort as top-level function
+ // of term t, but with numeric suffix appended to name.
+
+ private FuncDecl SuffixFuncDecl(Term t, int n)
+ {
+ var name = t.GetAppDecl().GetDeclName() + "_" + n.ToString();
+ return ctx.MkFuncDecl(name, t.GetAppDecl());
+ }
+
+ // Collect the relational paremeters
+
+ private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ var kind = t.GetKind();
+ if (kind == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ StratifiedInliningInfo info;
+ if (relationToProc.TryGetValue(f, out info))
+ {
+ f = SuffixFuncDecl(t, parms.Count);
+ parms.Add(f);
+ nodes.Add(info.node);
+ }
+ var args = t.GetAppArgs();
+ args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();
+ res = ctx.MkApp(f, args);
+ } // TODO: handle quantifiers
+ else res = t;
+ memo.Add(t, res);
+ return res;
+ }
+
+ public void GetTransformer(StratifiedInliningInfo info)
+ {
+ Term vcTerm = boogieContext.VCExprToTerm(info.vcexpr, linOptions);
+ Term[] paramTerms = info.interfaceExprVars.Select(x => boogieContext.VCExprToTerm(x, linOptions)).ToArray();
+ var relParams = new List<FuncDecl>();
+ var nodeParams = new List<RPFP.Node>();
+ var memo = new Dictionary<Term, Term>();
+ vcTerm = CollectParamsRec(memo, vcTerm, relParams, nodeParams);
+ // var ops = new Util.ContextOps(ctx);
+ // var foo = ops.simplify_lhs(vcTerm);
+ // vcTerm = foo.Item1;
+ info.F = rpfp.CreateTransformer(relParams.ToArray(), paramTerms, vcTerm);
+ info.edge = rpfp.CreateEdge(info.node, info.F, nodeParams.ToArray());
+ // TODO labels[info.edge.number] = foo.Item2;
+ }
+
+ public RPFP.Node GetNodeOfImpl(Implementation/*!*/ impl)
+ {
+ return implName2StratifiedInliningInfo[impl.Name].node;
+ }
+
+ public class CyclicLiveVariableAnalysis : Microsoft.Boogie.LiveVariableAnalysis
+ {
+ public static void ComputeLiveVariables(Implementation impl)
+ {
+
+ bool some_change = true;
+ List<Block> sortedNodes = new List<Block>();
+ foreach (var block in impl.Blocks)
+ {
+ sortedNodes.Add(block);
+ }
+ sortedNodes.Reverse();
+
+ while (some_change)
+ {
+ some_change = false;
+ foreach (Block/*!*/ block in sortedNodes)
+ {
+ Contract.Assert(block != null);
+ HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = (GotoCmd)block.TransferCmd;
+ if (gotoCmd.labelTargets != null)
+ {
+ foreach (Block/*!*/ succ in gotoCmd.labelTargets)
+ {
+ Contract.Assert(succ != null);
+ if (succ.liveVarsBefore != null)
+ liveVarsAfter.UnionWith(succ.liveVarsBefore);
+ }
+ }
+ }
+
+ CmdSeq cmds = block.Cmds;
+ int len = cmds.Length;
+ for (int i = len - 1; i >= 0; i--)
+ {
+ if (cmds[i] is CallCmd)
+ {
+ Procedure/*!*/ proc = cce.NonNull(cce.NonNull((CallCmd/*!*/)cmds[i]).Proc);
+ if (InterProcGenKill.HasSummary(proc.Name))
+ {
+ liveVarsAfter =
+ InterProcGenKill.PropagateLiveVarsAcrossCall(cce.NonNull((CallCmd/*!*/)cmds[i]), liveVarsAfter);
+ continue;
+ }
+ }
+ Propagate(cmds[i], liveVarsAfter);
+ }
+
+ if (block.liveVarsBefore == null)
+ block.liveVarsBefore = new HashSet<Variable>();
+ if (!liveVarsAfter.IsSubsetOf(block.liveVarsBefore))
+ {
+ block.liveVarsBefore = liveVarsAfter;
+ some_change = true;
+ }
+ }
+ }
+ }
+ }
+
+ public void Generate()
+ {
+
+
+ // Run live variable analysis (TODO: should this be here?)
+#if false
+ if (CommandLineOptions.Clo.LiveVariableAnalysis == 2)
+ {
+ Microsoft.Boogie.InterProcGenKill.ComputeLiveVars(impl, program);
+ }
+#endif
+
+ #region In Boogie mode, annotate the program
+ if (mode == Mode.Boogie)
+ {
+ // find the name of the main procedure
+ main_proc_name = "main"; // default in case no entry point defined
+ foreach (var d in program.TopLevelDeclarations)
+ {
+ var impl = d as Implementation;
+ if (impl != null)
+ {
+ if (QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
+ main_proc_name = impl.Proc.Name;
+ }
+ }
+ if (style == AnnotationStyle.Flat)
+ {
+ InlineAll();
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ foreach (var d in program.TopLevelDeclarations)
+ {
+ var impl = d as Implementation;
+ if (impl != null && main_proc_name == impl.Proc.Name)
+ {
+ Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
+ CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);
+ AnnotateLoops(impl, boogieContext);
+ }
+ }
+ }
+ else
+ {
+
+ if (style == AnnotationStyle.Procedure || style == AnnotationStyle.Call)
+ {
+ foreach (var proc in program.TopLevelDeclarations)
+ {
+ var impl = proc as Implementation;
+ if (impl != null)
+ AnnotateProcEnsures(impl.Proc, impl, boogieContext);
+ }
+ if (style == AnnotationStyle.Call)
+ {
+
+ }
+ }
+
+ // must do this after annotating procedures, else calls
+ // will be prematurely desugared
+
+ foreach (var d in program.TopLevelDeclarations)
+ {
+ var impl = d as Implementation;
+ if (impl != null)
+ {
+ Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
+ CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);
+ }
+ }
+
+
+ if (style == AnnotationStyle.Flat || style == AnnotationStyle.Call)
+ {
+ foreach (var proc in program.TopLevelDeclarations)
+ {
+ var impl = proc as Implementation;
+ if (impl != null)
+ AnnotateLoops(impl, boogieContext);
+ }
+ }
+ if (style == AnnotationStyle.Call)
+ {
+ Dictionary<string, bool> impls = new Dictionary<string, bool>();
+ foreach (var proc in program.TopLevelDeclarations)
+ {
+ var impl = proc as Implementation;
+ if (impl != null)
+ impls.Add(impl.Proc.Name, true);
+ }
+ foreach (var proc in program.TopLevelDeclarations)
+ {
+ var impl = proc as Implementation;
+ if (impl != null)
+ AnnotateCallSites(impl, boogieContext, impls);
+ }
+ }
+ if (style == AnnotationStyle.Flat)
+ InlineAll();
+ }
+ }
+ #endregion
+
+ /* Generate the VC's */
+ GenerateVCsForStratifiedInlining();
+
+ /* Generate the background axioms */
+ Term background = ctx.MkTrue(); // TODO boogieContext.VCExprToTerm(boogieContext.Axioms, linOptions);
+ rpfp.AssertAxiom(background);
+
+ int save_option = CommandLineOptions.Clo.StratifiedInlining; // need this to get funcall labels
+ CommandLineOptions.Clo.StratifiedInlining = 1;
+
+ /* Create the nodes, indexing procedures by their relational symbols. */
+ foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)
+ GenerateVCForStratifiedInlining(program, info, checker);
+
+ CommandLineOptions.Clo.StratifiedInlining = save_option;
+
+ if (mode == Mode.Boogie)
+ {
+ // var ops = new Util.ContextOps(ctx);
+ var vcs = DualityVCs;
+ DualityVCs = new List<Term>();
+ foreach (var vc in vcs)
+ {
+ // var foo = ops.simplify_lhs(vc.GetAppArgs()[0]);
+ var foo = vc.GetAppArgs()[0];
+ if (!foo.IsFalse())
+ DualityVCs.Add(ctx.MkImplies(foo, vc.GetAppArgs()[1]));
+ }
+
+ rpfp.FromClauses(DualityVCs.ToArray());
+ // TODO rpfp.HornClauses = style == AnnotationStyle.Flat;
+ }
+ else
+ {
+ /* Generate the edges. */
+ foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)
+ GetTransformer(info);
+ }
+
+ // save some information for debugging purposes
+ // TODO rpfp.ls.SetAnnotationInfo(annotationInfo);
+ }
+
+ private class ErrorHandler : ProverInterface.ErrorHandler
+ {
+ //TODO: anything we need to handle?
+ }
+
+ /** Check the RPFP, and return a counterexample if there is one. */
+
+ public RPFP.LBool Check(ref RPFP.Node cexroot)
+ {
+ var start = DateTime.Now;
+
+ ErrorHandler handler = new ErrorHandler();
+ RPFP.Node cex;
+ ProverInterface.Outcome outcome = checker.TheoremProver.CheckRPFP("name", rpfp, handler, out cex);
+ cexroot = cex;
+
+ Console.WriteLine("solve: {0}s", (DateTime.Now - start).TotalSeconds);
+
+ switch(outcome)
+ {
+ case ProverInterface.Outcome.Valid:
+ return RPFP.LBool.False;
+ case ProverInterface.Outcome.Invalid:
+ return RPFP.LBool.True;
+ default:
+ return RPFP.LBool.Undef;
+ }
+ }
+
+ public override VC.VCGen.Outcome VerifyImplementation(Implementation impl, VerifierCallback collector)
+ {
+ Procedure proc = impl.Proc;
+
+ // we verify all the impls at once, so we need to execute only once
+ // TODO: make sure needToCheck is true only once
+ bool needToCheck = false;
+ if (mode == Mode.OldCorral)
+ needToCheck = proc.FindExprAttribute("inline") == null && !(proc is LoopProcedure);
+ else if (mode == Mode.Corral)
+ needToCheck = proc.FindExprAttribute("entrypoint") != null && !(proc is LoopProcedure);
+ else
+ needToCheck = impl.Name == main_proc_name;
+
+ if (needToCheck)
+ {
+ var start = DateTime.Now;
+ Generate();
+ Console.WriteLine("generate: {0}s", (DateTime.Now - start).TotalSeconds);
+
+ Console.WriteLine("Verifying {0}...", impl.Name);
+
+ RPFP.Node cexroot = null;
+ // start = DateTime.Now;
+ var checkres = Check(ref cexroot);
+ Console.WriteLine("check: {0}s", (DateTime.Now - start).TotalSeconds);
+ switch (checkres)
+ {
+ case RPFP.LBool.True:
+ Console.WriteLine("Counterexample found.\n");
+ // start = DateTime.Now;
+ Counterexample cex = CreateBoogieCounterExample(cexroot.owner, cexroot, impl);
+ // cexroot.owner.DisposeDualModel();
+ // cex.Print(0); // TODO: just for testing
+ collector.OnCounterexample(cex, "assertion failure");
+ Console.WriteLine("cex: {0}s", (DateTime.Now - start).TotalSeconds);
+ return VC.ConditionGeneration.Outcome.Errors;
+ case RPFP.LBool.False:
+ Console.WriteLine("Procedure is correct.");
+ return Outcome.Correct;
+ case RPFP.LBool.Undef:
+ Console.WriteLine("Inconclusive result.");
+ return Outcome.ReachedBound;
+ }
+ }
+
+ return Outcome.Inconclusive;
+ }
+
+ public void FindLabelsRec(HashSet<Term> memo, Term t, Dictionary<string, Term> res)
+ {
+ if (memo.Contains(t))
+ return;
+ if (t.IsLabel())
+ {
+ string l = t.LabelName();
+ if (!res.ContainsKey(l))
+ res.Add(l, t.GetAppArgs()[0]);
+ }
+ if (t.GetKind() == TermKind.App)
+ {
+ var args = t.GetAppArgs();
+ foreach (var a in args)
+ FindLabelsRec(memo, a, res);
+ } // TODO: handle quantifiers
+
+ memo.Add(t);
+ }
+
+ public void FindLabels()
+ {
+ labels = new Dictionary<string, Term>();
+ foreach(var e in rpfp.edges){
+ int id = e.number;
+ HashSet<Term> memo = new HashSet<Term>();
+ FindLabelsRec(memo, e.F.Formula, labels);
+ }
+ }
+
+ public string CodeLabel(Absy code, StratifiedInliningInfo info, string prefix)
+ {
+ if (info.label2absyInv == null)
+ {
+ info.label2absyInv = new Dictionary<Absy, string>();
+ foreach (int foo in info.label2absy.Keys)
+ {
+ Absy bar = info.label2absy[foo] as Absy;
+ string lbl = foo.ToString();
+ info.label2absyInv.Add(bar, lbl);
+ }
+ }
+ if (info.label2absyInv.ContainsKey(code))
+ {
+ string label = info.label2absyInv[code];
+ return prefix+label;
+ }
+ return null;
+ }
+
+ public Term CodeLabeledExpr(RPFP rpfp, RPFP.Node root, Absy code, StratifiedInliningInfo info, string prefix)
+ {
+ string label = CodeLabel(code, info, prefix);
+
+ if (label != null)
+ {
+ var res = labels[label];
+ return res;
+ }
+ else return null;
+ }
+
+ public class LabelNotFound : Exception { };
+
+ public bool CodeLabelTrue(RPFP rpfp, RPFP.Node root, Absy code, StratifiedInliningInfo info, string prefix)
+ {
+ string label = CodeLabel(code, info, prefix);
+
+ if (label == null)
+ throw new LabelNotFound();
+ return root.Outgoing.labels.Contains(label);
+ }
+
+ public bool CodeLabelFalse(RPFP rpfp, RPFP.Node root, Absy code, StratifiedInliningInfo info, string prefix)
+ {
+ return CodeLabelTrue(rpfp, root, code, info, prefix);
+ }
+
+ public Counterexample CreateBoogieCounterExample(RPFP rpfp, RPFP.Node root, Implementation mainImpl)
+ {
+ FindLabels();
+ var orderedStateIds = new List<Tuple<int, int>>();
+ Counterexample newCounterexample =
+ GenerateTrace(rpfp, root, orderedStateIds, mainImpl,true);
+ return newCounterexample;
+ }
+
+ private Counterexample GenerateTrace(RPFP rpfp, RPFP.Node root,
+ List<Tuple<int, int>> orderedStateIds, Implementation procImpl, bool toplevel)
+ {
+ Contract.Requires(procImpl != null);
+
+ Contract.Assert(!rpfp.Empty(root));
+
+
+ var info = implName2StratifiedInliningInfo[procImpl.Name];
+ Block entryBlock = cce.NonNull(procImpl.Blocks[0]);
+ Contract.Assert(entryBlock != null);
+ if (!CodeLabelFalse(rpfp, root, entryBlock, info, "+"))
+ Contract.Assert(false);
+ BlockSeq trace = new BlockSeq();
+ trace.Add(entryBlock);
+
+ var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
+ Counterexample newCounterexample =
+ GenerateTraceRec(rpfp, root, orderedStateIds, entryBlock, trace, calleeCounterexamples, info, toplevel);
+
+ return newCounterexample;
+ }
+
+ // TODO: this is a bit cheesy. Rather than finding the argument position
+ // of a relational term in a transformer by linear search, better to index this
+ // somewhere, but where?
+ private int TransformerArgPosition(RPFP rpfp, RPFP.Node root, Term expr)
+ {
+ FuncDecl rel = expr.GetAppDecl();
+ string relname = rel.GetDeclName();
+ var rps = root.Outgoing.F.RelParams;
+ for (int i = 0; i < rps.Length; i++)
+ {
+ string thisname = rps[i].GetDeclName();
+ if (thisname == relname)
+ return i;
+ }
+ return -1;
+ }
+
+ private bool EvalToFalse(RPFP rpfp, RPFP.Node root, Term expr,StratifiedInliningInfo info){
+ Term res = rpfp.Eval(root.Outgoing,expr);
+ return res.Equals(ctx.MkTrue());
+ }
+
+ private Counterexample GenerateTraceRec(
+ RPFP rpfp, RPFP.Node root,
+ List<Tuple<int, int>> orderedStateIds,
+ Block/*!*/ b, BlockSeq/*!*/ trace,
+ Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples,
+ StratifiedInliningInfo info,
+ bool toplevel)
+ {
+ Contract.Requires(b != null);
+ Contract.Requires(trace != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
+ // After translation, all potential errors come from asserts.
+ while (true)
+ {
+ CmdSeq cmds = b.Cmds;
+ TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
+ for (int i = 0; i < cmds.Length; i++)
+ {
+ Cmd cmd = cce.NonNull(cmds[i]);
+
+ // Skip if 'cmd' not contained in the trace or not an assert
+ if (cmd is AssertCmd)
+ {
+ bool is_failed_assertion = false;
+ if (NoLabels)
+ is_failed_assertion = true; // we assume only assertions on
+ else
+ is_failed_assertion = CodeLabelTrue(rpfp, root, cmd, info, "@");
+
+ Counterexample newCounterexample =
+ AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, new Microsoft.Boogie.Model(), info.mvInfo,
+ boogieContext);
+ newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
+ return newCounterexample;
+ }
+
+ // Counterexample generation for inlined procedures
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ if (assumeCmd == null)
+ continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null)
+ continue;
+ string calleeName = naryExpr.Fun.FunctionName;
+ Contract.Assert(calleeName != null);
+
+ // what is this crap???
+ BinaryOperator binOp = naryExpr.Fun as BinaryOperator;
+ if (binOp != null && binOp.Op == BinaryOperator.Opcode.And)
+ {
+ Expr expr = naryExpr.Args[0];
+ NAryExpr mvStateExpr = expr as NAryExpr;
+ if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == VC.ModelViewInfo.MVState_FunctionDef.Name)
+ {
+ LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;
+ // Debug.Assert(x != null);
+ int foo = x.asBigNum.ToInt;
+ orderedStateIds.Add(new Tuple<int, int>(root.number, foo));
+ }
+ }
+
+ if (calleeName.EndsWith("_summary"))
+ calleeName = calleeName.Substring(0, calleeName.Length - 8);
+
+ if (!implName2StratifiedInliningInfo.ContainsKey(calleeName) && !calleeName.EndsWith("_summary"))
+ continue;
+
+ {
+ Term code = CodeLabeledExpr(rpfp, root, cmd, info, "+si_fcall_");
+ int pos = TransformerArgPosition(rpfp,root,code);
+ if(pos >= 0)
+ {
+ RPFP.Node callee = root.Outgoing.Children[pos];
+ orderedStateIds.Add(new Tuple<int, int>(callee.number, VC.StratifiedVCGen.StratifiedInliningErrorReporter.CALL));
+ calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ new CalleeCounterexampleInfo(
+ cce.NonNull(GenerateTrace(rpfp, callee, orderedStateIds,
+ implName2StratifiedInliningInfo[calleeName].impl,false)),
+ new List<object>());
+ orderedStateIds.Add(new Tuple<int, int>(root.number, VC.StratifiedVCGen.StratifiedInliningErrorReporter.RETURN));
+ }
+ }
+ }
+
+ GotoCmd gotoCmd = transferCmd as GotoCmd;
+ if (gotoCmd != null)
+ {
+ b = null;
+ foreach (Block bb in cce.NonNull(gotoCmd.labelTargets))
+ {
+ Contract.Assert(bb != null);
+ if (CodeLabelFalse(rpfp,root,bb,info,"+"))
+ {
+ trace.Add(bb);
+ b = bb;
+ break;
+ }
+ }
+ if (b != null) continue;
+ }
+ return null;
+ }
+
+
+ }
+
+ }
+
+
+}
diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs new file mode 100644 index 00000000..96fdec97 --- /dev/null +++ b/Source/VCGeneration/RPFP.cs @@ -0,0 +1,558 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) 2012 Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using Term = Microsoft.Boogie.VCExprAST.VCExpr;
+using FuncDecl = Microsoft.Boogie.VCExprAST.VCExprOp;
+using Sort = Microsoft.Boogie.Type;
+using Microsoft.Boogie.VCExprAST;
+
+
+using Microsoft.Boogie.ExprExtensions;
+
+
+namespace Microsoft.Boogie
+{
+
+
+
+
+ /** This class represents a relation post-fixed point (RPFP) problem as
+ * a "problem graph". The graph consists of Nodes and hyper-edges.
+ *
+ * A node consists of
+ * - Annotation, a symbolic relation
+ * - Bound, a symbolic relation giving an upper bound on Annotation
+ *
+ *
+ * A hyper-edge consists of:
+ * - Children, a sequence of children Nodes,
+ * - F, a symbolic relational transformer,
+ * - Parent, a single parent Node.
+ *
+ * The graph is "solved" when:
+ * - For every Node n, n.Annotation subseteq n.Bound
+ * - For every hyperedge e, e.F(e.Children.Annotation) subseteq e.Parent.Annotation
+ *
+ * where, if x is a sequence of Nodes, x.Annotation is the sequences
+ * of Annotations of the nodes in the sequence.
+ *
+ * A symbolic Transformer consists of
+ * - RelParams, a sequence of relational symbols
+ * - IndParams, a sequence of individual symbols
+ * - Formula, a formula over RelParams and IndParams
+ *
+ * A Transformer t represents a function that takes sequence R of relations
+ * and yields the relation lambda (t.Indparams). Formula(R/RelParams).
+ *
+ * As a special case, a nullary Transformer (where RelParams is the empty sequence)
+ * represents a fixed relation.
+ *
+ * An RPFP consists of
+ * - Nodes, a set of Nodes
+ * - Edges, a set of hyper-edges
+ * - Context, a prover context that contains formula AST's
+ *
+ * Multiple RPFP's can use the same Context, but you should be careful
+ * that only one RPFP asserts constraints in the context at any time.
+ *
+ * */
+ public class RPFP
+ {
+ /** Symbolic representation of a relational transformer */
+ public class Transformer
+ {
+ public FuncDecl[] RelParams;
+ public Term[] IndParams;
+ public Term Formula;
+ public RPFP owner;
+
+ public Transformer Clone()
+ {
+ return (Transformer)this.MemberwiseClone();
+ }
+ }
+
+ /** Create a symbolic transformer. */
+ public Transformer CreateTransformer(FuncDecl[] _RelParams, Term[] _IndParams, Term _Formula)
+ {
+ Transformer t = new Transformer();
+ t.RelParams = _RelParams;
+ t.IndParams = _IndParams;
+ t.Formula = _Formula;
+ t.owner = this;
+ return t;
+ }
+
+ /** Create a relation (nullary relational transformer) */
+ public Transformer CreateRelation(Term[] _IndParams, Term _Formula)
+ {
+ return CreateTransformer(new FuncDecl[0], _IndParams, _Formula);
+ }
+
+ /** A node in the RPFP graph */
+ public class Node
+ {
+ public FuncDecl Name;
+ public Transformer Annotation;
+ public Transformer Bound;
+ public RPFP owner;
+ public int number;
+ public Edge Outgoing;
+ public List<Edge> Incoming;
+ public Term dual;
+ public Node map;
+ }
+
+ /** Create a node in the graph. The input is a term R(v_1...v_n)
+ * where R is an arbitrary relational symbol and v_1...v_n are
+ * arbitary distinct variables. The names are only of mnemonic value,
+ * however, the number and type of arguments determine the type
+ * of the relation at this node. */
+
+ public Node CreateNode(Term t)
+ {
+ Node n = new Node();
+ // Microsoft.Boogie.VCExprAST.VCExprNAry tn = t as Microsoft.Boogie.VCExprAST.VCExprNAry;
+ // Term[] _IndParams = tn.ToArray();
+ Term[] _IndParams = t.GetAppArgs();
+ FuncDecl Name = t.GetAppDecl();
+ n.Annotation = CreateRelation(_IndParams,ctx.MkTrue());
+ n.Bound = CreateRelation(_IndParams, ctx.MkTrue());
+ n.owner = this;
+ n.number = ++nodeCount;
+ n.Name = Name; // just to have a unique name
+ n.Incoming = new List<Edge>();
+ return n;
+ }
+
+ /** Clone a node (can be from another graph). */
+
+ public Node CloneNode(Node old)
+ {
+ Node n = new Node();
+ n.Annotation = old.Annotation.Clone();
+ n.Bound = old.Bound.Clone();
+ n.owner = this;
+ n.number = ++nodeCount;
+ n.Name = old.Name; // just to have a unique name
+ n.Incoming = new List<Edge>();
+ return n;
+ }
+
+ /** This class represents a hyper-edge in the RPFP graph */
+
+ public class Edge
+ {
+ public Transformer F;
+ public Node Parent;
+ public Node[] Children;
+ public RPFP owner;
+ public int number;
+ public Edge map;
+ public HashSet<string> labels;
+ internal Term dual;
+ internal Dictionary<FuncDecl,int> relMap;
+ internal Dictionary<Term,Term> varMap;
+ }
+
+
+ /** Create a hyper-edge. */
+ public Edge CreateEdge(Node _Parent, Transformer _F, Node[] _Children)
+ {
+ Edge e = new Edge();
+ e.Parent = _Parent;
+ e.F = _F;
+ e.Children = _Children;
+ e.owner = this;
+ e.number = ++edgeCount;
+ _Parent.Outgoing = e;
+ foreach (var c in _Children)
+ c.Incoming.Add(e);
+ return e;
+ }
+
+ /** Create an edge that lower-bounds its parent. */
+ public Edge CreateLowerBoundEdge(Node _Parent)
+ {
+ return CreateEdge(_Parent, _Parent.Annotation, new RPFP.Node[0]);
+ }
+
+
+
+
+ /** Assert a background axiom. Background axioms can be used to provide the
+ * theory of auxilliary functions or relations. All symbols appearing in
+ * background axioms are considered global, and may appear in both transformer
+ * and relational solutions. Semantically, a solution to the RPFP gives
+ * an interpretation of the unknown relations for each interpretation of the
+ * auxilliary symbols that is consistent with the axioms. Axioms should be
+ * asserted before any calls to Push. They cannot be de-asserted by Pop. */
+
+ public void AssertAxiom(Term t)
+ {
+ ctx.AddAxiom(t);
+ }
+
+ /** Do not call this. */
+
+ public void RemoveAxiom(Term t)
+ {
+ ctx.RemoveAxiom(t);
+ }
+
+ /** Type of solve results */
+ public enum LBool { False, True, Undef };
+
+
+ /** Solve an RPFP graph. This means either strengthen the annotation
+ * so that the bound at the given root node is satisfied, or
+ * show that this cannot be done by giving a dual solution
+ * (i.e., a counterexample).
+ *
+ * In the current implementation, this only works for graphs that
+ * are:
+ * - tree-like
+ *
+ * - closed.
+ *
+ * In a tree-like graph, every nod has out most one incoming and one out-going edge,
+ * and there are no cycles. In a closed graph, every node has exactly one out-going
+ * edge. This means that the leaves of the tree are all hyper-edges with no
+ * children. Such an edge represents a relation (nullary transformer) and thus
+ * a lower bound on its parent. The parameter root must be the root of this tree.
+ *
+ * If Solve returns LBool.False, this indicates success. The annotation of the tree
+ * has been updated to satisfy the upper bound at the root.
+ *
+ * If Solve returns LBool.True, this indicates a counterexample. For each edge,
+ * you can then call Eval to determine the values of symbols in the transformer formula.
+ * You can also call Empty on a node to determine if its value in the counterexample
+ * is the empty relation.
+ *
+ * \param root The root of the tree
+ * \param persist Number of context pops through which result should persist
+ *
+ *
+ */
+
+ public LBool Solve(Node root, int persist)
+ {
+ return LBool.False; // TODO
+ }
+
+
+ /** Dispose of the dual model (counterexample) if there is one. */
+
+ public void DisposeDualModel()
+ {
+ // TODO dualModel = null;
+ }
+
+
+ /** Determines the value in the counterexample of a symbol occuring in the transformer formula of
+ * a given edge. */
+
+ public Term Eval(Edge e, Term t)
+ {
+ return ctx.MkFalse(); // TODO
+ }
+
+
+
+ /** Returns true if the given node is empty in the primal solution. For proecudure summaries,
+ this means that the procedure is not called in the current counter-model. */
+
+ public bool Empty(Node p)
+ {
+ return false; // TODO
+ }
+
+ /** Push a scope. Assertions made after Push can be undone by Pop. */
+
+ public void Push()
+ {
+ stack.Push(new stack_entry());
+ // TODO: do we need push/pop?
+ }
+
+ /** Pop a scope (see Push). Note, you cannot pop axioms. */
+
+ public void Pop(int num_scopes)
+ {
+ //TODO ctx.Pop((uint)num_scopes);
+ for (uint i = 0; i < num_scopes; i++)
+ {
+ stack_entry back = stack.Pop();
+ foreach (var e in back.edges)
+ e.dual = null;
+ foreach (var n in back.nodes)
+ n.dual = null;
+ }
+ }
+
+ public Context ctx;
+
+ public class LogicSolver {
+ public Context ctx;
+ };
+
+ public LogicSolver solver;
+
+ static public LogicSolver CreateLogicSolver(Context _ctx){
+ LogicSolver res = new LogicSolver();
+ res.ctx = _ctx;
+ return res;
+ }
+
+
+ /** Construct an RPFP graph with a given interpolating prover context. It is allowed to
+ have multiple RPFP's use the same context, but you should never have teo RPFP's
+ with the same conext asserting nodes or edges at the same time. Note, if you create
+ axioms in one RPFP, them create a second RPFP with the same context, the second will
+ inherit the axioms.
+ */
+
+ public RPFP(LogicSolver slvr)
+ {
+ solver = slvr;
+ ctx = slvr.ctx;
+ stack = new Stack<stack_entry>();
+ stack.Push(new stack_entry());
+ }
+
+
+ /** Convert an array of clauses to an RPFP.
+ */
+
+ public void FromClauses(Term[] clauses){
+ FuncDecl failName = ctx.MkFuncDecl("@Fail", ctx.MkBoolSort());
+ foreach(var clause in clauses){
+ Node foo = GetNodeFromClause(clause,failName);
+ if(foo != null)
+ nodes.Add(foo);
+ }
+ foreach (var clause in clauses)
+ edges.Add(GetEdgeFromClause(clause,failName));
+ }
+
+
+ // This returns a new FuncDel with same sort as top-level function
+ // of term t, but with numeric suffix appended to name.
+
+ private FuncDecl SuffixFuncDecl(Term t, int n)
+ {
+ var name = t.GetAppDecl().GetDeclName() + "_" + n.ToString();
+ return ctx.MkFuncDecl(name, t.GetAppDecl());
+ }
+
+ // Collect the relational paremeters
+
+ Dictionary<FuncDecl, Node> relationToNode = new Dictionary<FuncDecl, Node>();
+
+ private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ if (t.GetKind() == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ Node node;
+ if (relationToNode.TryGetValue(f, out node))
+ {
+ f = SuffixFuncDecl(t, parms.Count);
+ parms.Add(f);
+ nodes.Add(node);
+ }
+ var args = t.GetAppArgs();
+ args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();
+ res = ctx.MkApp(f, args);
+ } // TODO: handle quantifiers
+ else
+ res = t;
+ memo.Add(t, res);
+ return res;
+ }
+
+ private bool IsVariable(Term t)
+ {
+ // TODO: is this right?
+ // return t.IsFunctionApp() && t.GetAppArgs().Length == 0;
+ return t is VCExprVar;
+ }
+
+ private Edge GetEdgeFromClause(Term t, FuncDecl failName)
+ {
+ Term[] args = t.GetAppArgs();
+ Term body = args[0];
+ Term head = args[1];
+ Term[] _IndParams;
+ FuncDecl Name;
+ if (head.IsFalse())
+ {
+ Name = failName;
+ _IndParams = new Term[0];
+ }
+ else
+ {
+ _IndParams = head.GetAppArgs();
+ Name = head.GetAppDecl();
+ }
+ for(int i = 0; i < _IndParams.Length; i++)
+ if (!IsVariable(_IndParams[i]))
+ {
+ Term v = ctx.MkConst("@a" + i.ToString(), _IndParams[i].GetSort());
+ body = ctx.MkAnd(body, ctx.MkEq(v, _IndParams[i]));
+ _IndParams[i] = v;
+ }
+ var relParams = new List<FuncDecl>();
+ var nodeParams = new List<RPFP.Node>();
+ var memo = new Dictionary<Term, Term>();
+ body = CollectParamsRec(memo, body, relParams, nodeParams);
+ Transformer F = CreateTransformer(relParams.ToArray(), _IndParams, body);
+ Node parent = relationToNode[Name];
+ return CreateEdge(parent, F, nodeParams.ToArray());
+ }
+
+ private Node GetNodeFromClause(Term t, FuncDecl failName)
+ {
+ Term[] args = t.GetAppArgs();
+ Term body = args[0];
+ Term head = args[1];
+ FuncDecl Name;
+ Term[] _IndParams;
+ bool is_query = false;
+ if (head.Equals(ctx.MkFalse()))
+ {
+ Name = failName;
+ is_query = true;
+ _IndParams = new Term[0];
+ }
+ else
+ {
+ Name = head.GetAppDecl();
+ _IndParams = head.GetAppArgs();
+ }
+ if (relationToNode.ContainsKey(Name))
+ return null;
+ for (int i = 0; i < _IndParams.Length; i++)
+ if (!IsVariable(_IndParams[i]))
+ {
+ Term v = ctx.MkConst("@a" + i.ToString(), _IndParams[i].GetSort());
+ _IndParams[i] = v;
+ }
+ Term foo = ctx.MkApp(Name, _IndParams);
+ Node node = CreateNode(foo);
+ relationToNode[Name] = node;
+ if (is_query)
+ node.Bound = CreateRelation(new Term[0], ctx.MkFalse());
+ return node;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////////
+ // Convert RPFP to Z3 rules
+ /////////////////////////////////////////////////////////////////////////////////////////
+
+ /** Get the Z3 rule corresponding to an edge */
+
+ public Term GetRule(Edge edge)
+ {
+ Dictionary<FuncDecl, FuncDecl> predSubst = new Dictionary<FuncDecl, FuncDecl>();
+ for (int i = 0; i < edge.Children.Length; i++)
+ predSubst.Add(edge.F.RelParams[i], edge.Children[i].Name);
+ Term body = SubstPreds(predSubst, edge.F.Formula);
+ Term head = ctx.MkApp(edge.Parent.Name, edge.F.IndParams);
+ return BindVariables(ctx.MkImplies(body, head));
+ }
+
+ /** Get the Z3 query corresponding to the conjunction of the node bounds. */
+
+ public Term GetQuery()
+ {
+ List<Term> conjuncts = new List<Term>();
+ foreach (var node in nodes)
+ {
+ if (node.Bound.Formula != ctx.MkTrue())
+ conjuncts.Add(ctx.MkImplies(ctx.MkApp(node.Name, node.Bound.IndParams), node.Bound.Formula));
+ }
+ Term query = ctx.MkNot(ctx.MkAnd(conjuncts.ToArray()));
+ return BindVariables(query,false); // bind variables existentially
+ }
+
+ private void CollectVariables(Dictionary<Term, bool> memo, Term t, List<Term> vars)
+ {
+ if (memo.ContainsKey(t))
+ return;
+ if (IsVariable(t))
+ vars.Add(t);
+ if (t.GetKind() == TermKind.App)
+ {
+ foreach (var s in t.GetAppArgs())
+ CollectVariables(memo, s, vars);
+ }
+ memo.Add(t, true);
+ }
+
+ private Term BindVariables(Term t, bool universal = true)
+ {
+ Dictionary<Term, bool> memo = new Dictionary<Term,bool>();
+ List<Term> vars = new List<Term>();
+ CollectVariables(memo,t,vars);
+ return universal ? ctx.MkForall(vars.ToArray(), t) : ctx.MkExists(vars.ToArray(), t);
+ }
+
+ private Term SubstPredsRec(Dictionary<Term, Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ if (t.GetKind() == TermKind.App)
+ {
+ var args = t.GetAppArgs();
+ args = args.Select(x => SubstPredsRec(memo,subst,x)).ToArray();
+ FuncDecl nf = null;
+ var f = t.GetAppDecl();
+ if (subst.TryGetValue(f, out nf))
+ f = nf;
+ res = ctx.MkApp(f, args);
+ } // TODO: handle quantifiers
+ else
+ res = t;
+ memo.Add(t, res);
+ return res;
+ }
+
+ private Term SubstPreds(Dictionary<FuncDecl, FuncDecl> subst, Term t)
+ {
+ Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ return SubstPredsRec(memo, subst, t);
+ }
+
+ /* Everything after here is private. */
+
+ private class stack_entry
+ {
+ public List<Edge> edges = new List<Edge>();
+ public List<Node> nodes = new List<Node>();
+ };
+
+
+ private int nodeCount = 0;
+ private int edgeCount = 0;
+ // private Model dualModel;
+ // private LabeledLiterals dualLabels;
+ private Stack<stack_entry> stack;
+ public List<Node> nodes = new List<Node>();
+ public List<Edge> edges = new List<Edge>();
+
+
+ }
+}
|