From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Provers/SMTLib/ProverInterface.cs | 5075 ++++++++++++++++-------------- 1 file changed, 2651 insertions(+), 2424 deletions(-) (limited to 'Source/Provers/SMTLib/ProverInterface.cs') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 868b9ee3..300fbc10 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -1,2424 +1,2651 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections; -using System.Collections.Generic; -using System.Threading; -using System.IO; -//using ExternalProver; -using System.Linq; -using System.Diagnostics; -using System.Diagnostics.Contracts; -using Microsoft.Boogie.AbstractInterpretation; -using Microsoft.Boogie; -using Microsoft.Boogie.VCExprAST; -using Microsoft.Boogie.Clustering; -using Microsoft.Boogie.TypeErasure; -using System.Text; - -using RPFP = Microsoft.Boogie.RPFP; - -namespace Microsoft.Boogie.SMTLib -{ - public class SMTLibProcessTheoremProver : ProverInterface - { - private readonly SMTLibProverContext ctx; - private VCExpressionGenerator gen; - private readonly SMTLibProverOptions options; - private bool usingUnsatCore; - private RPFP rpfp = null; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(ctx != null); - Contract.Invariant(AxBuilder != null); - Contract.Invariant(Namer != null); - Contract.Invariant(DeclCollector != null); - Contract.Invariant(cce.NonNullElements(Axioms)); - Contract.Invariant(cce.NonNullElements(TypeDecls)); - Contract.Invariant(_backgroundPredicates != null); - - } - - - [NotDelayed] - public SMTLibProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen, - SMTLibProverContext ctx) - { - Contract.Requires(options != null); - Contract.Requires(gen != null); - Contract.Requires(ctx != null); - - InitializeGlobalInformation(); - - this.options = (SMTLibProverOptions)options; - this.ctx = ctx; - this.gen = gen; - this.usingUnsatCore = false; - - SetupAxiomBuilder(gen); - - Namer = new SMTLibNamer(); - ctx.parent = this; - this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer); - - if (CommandLineOptions.Clo.PrintFixedPoint != null || CommandLineOptions.Clo.PrintConjectures != null) - { - declHandler = new MyDeclHandler(); - DeclCollector.SetDeclHandler(declHandler); - } - - SetupProcess(); - - if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer - || CommandLineOptions.Clo.SecureVcGen != null) - { - // Prepare for ApiChecker usage - if (options.LogFilename != null && currentLogFile == null) - { - currentLogFile = OpenOutputFile(""); - } - PrepareCommon(); - } - } - - private void SetupAxiomBuilder(VCExpressionGenerator gen) - { - switch (CommandLineOptions.Clo.TypeEncodingMethod) - { - case CommandLineOptions.TypeEncoding.Arguments: - AxBuilder = new TypeAxiomBuilderArguments(gen); - AxBuilder.Setup(); - break; - case CommandLineOptions.TypeEncoding.Monomorphic: - AxBuilder = new TypeAxiomBuilderPremisses(gen); - break; - default: - AxBuilder = new TypeAxiomBuilderPremisses(gen); - AxBuilder.Setup(); - break; - } - } - - ProcessStartInfo ComputeProcessStartInfo() - { - var path = this.options.ProverPath; - switch (options.Solver) { - case SolverKind.Z3: - if (path == null) - path = Z3.ExecutablePath(); - return SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in"); - case SolverKind.CVC4: - if (path == null) - path = CVC4.ExecutablePath(); - return SMTLibProcess.ComputerProcessStartInfo(path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental"); - default: - Debug.Assert(false); - return null; - } - } - - void SetupProcess() - { - if (Process != null) return; - - var psi = ComputeProcessStartInfo(); - Process = new SMTLibProcess(psi, this.options); - Process.ErrorHandler += this.HandleProverError; - } - - - void PossiblyRestart() - { - if (Process != null && Process.NeedsRestart) { - Process.Close(); - Process = null; - SetupProcess(); - Process.Send(common.ToString()); - } - } - - public override ProverContext Context - { - get - { - Contract.Ensures(Contract.Result() != null); - - return ctx; - } - } - - internal TypeAxiomBuilder AxBuilder { get; private set; } - internal readonly UniqueNamer Namer; - readonly TypeDeclCollector DeclCollector; - protected SMTLibProcess Process; - readonly List proverErrors = new List(); - readonly List proverWarnings = new List(); - readonly StringBuilder common = new StringBuilder(); - protected TextWriter currentLogFile; - protected volatile ErrorHandler currentErrorHandler; - - private void FeedTypeDeclsToProver() - { - foreach (string s in DeclCollector.GetNewDeclarations()) { - Contract.Assert(s != null); - AddTypeDecl(s); - } - } - - private string Sanitize(string msg) - { - var idx = msg.IndexOf('\n'); - if (idx > 0) - msg = msg.Replace("\r", "").Replace("\n", "\r\n"); - return msg; - } - - public override void LogComment(string comment) - { - SendCommon("; " + comment); - } - - private void SendCommon(string s) - { - Send(s, true); - } - - protected void SendThisVC(string s) - { - Send(s, false); - } - - private void Send(string s, bool isCommon) - { - s = Sanitize(s); - - if (isCommon) - common.Append(s).Append("\r\n"); - - if (Process != null) - Process.Send(s); - if (currentLogFile != null) { - currentLogFile.WriteLine(s); - currentLogFile.Flush(); - } - } - - private void FindDependentTypes(Type type, List dependentTypes) - { - MapType mapType = type as MapType; - if (mapType != null) - { - foreach (Type t in mapType.Arguments) - { - FindDependentTypes(t, dependentTypes); - } - FindDependentTypes(mapType.Result, dependentTypes); - } - CtorType ctorType = type as CtorType; - if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey(ctorType)) - { - dependentTypes.Add(ctorType); - } - } - - private void PrepareCommon() - { - if (common.Length == 0) - { - SendCommon("(set-option :print-success false)"); - SendCommon("(set-info :smt-lib-version 2.0)"); - if (options.ProduceModel()) - SendCommon("(set-option :produce-models true)"); - foreach (var opt in options.SmtOptions) - { - SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); - } - - if (!string.IsNullOrEmpty(options.Logic)) - { - SendCommon("(set-logic " + options.Logic + ")"); - } - - // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value - // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 ) - if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)) - { - SendThisVC("(set-option :produce-unsat-cores true)"); - this.usingUnsatCore = true; - } - - SendCommon("; done setting options\n"); - SendCommon(_backgroundPredicates); - - if (options.UseTickleBool) - { - SendCommon("(declare-fun tickleBool (Bool) Bool)"); - SendCommon("(assert (and (tickleBool true) (tickleBool false)))"); - } - - if (ctx.KnownDatatypeConstructors.Count > 0) - { - GraphUtil.Graph dependencyGraph = new GraphUtil.Graph(); - foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) - { - dependencyGraph.AddSource(datatype); - foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) - { - List dependentTypes = new List(); - foreach (Variable v in f.InParams) - { - FindDependentTypes(v.TypedIdent.Type, dependentTypes); - } - foreach (CtorType result in dependentTypes) - { - dependencyGraph.AddEdge(datatype, result); - } - } - } - GraphUtil.StronglyConnectedComponents sccs = new GraphUtil.StronglyConnectedComponents(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors); - sccs.Compute(); - foreach (GraphUtil.SCC scc in sccs) - { - string datatypeString = ""; - foreach (CtorType datatype in scc) - { - datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " "; - foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) - { - string quotedConstructorName = Namer.GetQuotedName(f, f.Name); - if (f.InParams.Count == 0) - { - datatypeString += quotedConstructorName + " "; - } - else - { - datatypeString += "(" + quotedConstructorName + " "; - foreach (Variable v in f.InParams) - { - string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name); - datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") "; - } - datatypeString += ") "; - } - } - datatypeString += ") "; - } - List decls = DeclCollector.GetNewDeclarations(); - foreach (string decl in decls) - { - SendCommon(decl); - } - SendCommon("(declare-datatypes () (" + datatypeString + "))"); - } - } - } - - if (!AxiomsAreSetup) - { - var axioms = ctx.Axioms; - var nary = axioms as VCExprNAry; - if (nary != null && nary.Op == VCExpressionGenerator.AndOp) - foreach (var expr in nary.UniformArguments) - { - var str = VCExpr2String(expr, -1); - if (str != "true") - AddAxiom(str); - } - else - AddAxiom(VCExpr2String(axioms, -1)); - AxiomsAreSetup = true; - } - } - - public override int FlushAxiomsToTheoremProver() - { - // we feed the axioms when begincheck is called. - return 0; - } - - private void FlushAxioms() - { - TypeDecls.Iter(SendCommon); - TypeDecls.Clear(); - foreach (string s in Axioms) { - Contract.Assert(s != null); - if (s != "true") - SendCommon("(assert " + s + ")"); - } - Axioms.Clear(); - //FlushPushedAssertions(); - } - - private void CloseLogFile() - { - if (currentLogFile != null) { - currentLogFile.Close(); - currentLogFile = null; - } - } - - private void FlushLogFile() - { - if (currentLogFile != null) { - currentLogFile.Flush(); - } - } - - public override void Close() - { - base.Close(); - CloseLogFile(); - if (Process != null) - Process.Close(); - } - - public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) - { - //Contract.Requires(descriptiveName != null); - //Contract.Requires(vc != null); - //Contract.Requires(handler != null); - rpfp = null; - - if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen - - if (options.LogFilename != null && currentLogFile == null) - { - currentLogFile = OpenOutputFile(descriptiveName); - currentLogFile.Write(common.ToString()); - } - - PrepareCommon(); - string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; - FlushAxioms(); - - PossiblyRestart(); - - SendThisVC("(push 1)"); - SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); - SendThisVC(vcString); - FlushLogFile(); - - if (Process != null) { - Process.PingPong(); // flush any errors - - if (Process.Inspector != null) - Process.Inspector.NewProblem(descriptiveName, vc, handler); - } - - SendThisVC("(check-sat)"); - FlushLogFile(); - } - - public override void Reset(VCExpressionGenerator gen) - { - if (options.Solver == SolverKind.Z3) - { - this.gen = gen; - SendThisVC("(reset)"); - - if (0 < common.Length) - { - var c = common.ToString(); - Process.Send(c); - if (currentLogFile != null) - { - currentLogFile.WriteLine(c); - } - } - } - } - - public override void FullReset(VCExpressionGenerator gen) - { - if (options.Solver == SolverKind.Z3) - { - this.gen = gen; - Namer.Reset(); - common.Clear(); - SetupAxiomBuilder(gen); - Axioms.Clear(); - TypeDecls.Clear(); - AxiomsAreSetup = false; - ctx.Reset(); - ctx.KnownDatatypeConstructors.Clear(); - ctx.parent = this; - DeclCollector.Reset(); - SendThisVC("; doing a full reset..."); - } - } - - - - private string StripCruft(string name){ - if(name.Contains("@@")) - return name.Remove(name.LastIndexOf ("@@")); - return name; - } - - private class BadExprFromProver : Exception - { - }; - - private delegate VCExpr ArgGetter (int pos); - - private delegate VCExpr[] ArgsGetter (); - - private delegate VCExprVar[] VarsGetter (); - - private VCExprOp VCStringToVCOp (string op) - { - switch (op) { - case "+" : - return VCExpressionGenerator.AddIOp; - case "-" : - return VCExpressionGenerator.SubIOp; - case "*" : - return VCExpressionGenerator.MulIOp; - case "div" : - return VCExpressionGenerator.DivIOp; - case "=" : - return VCExpressionGenerator.EqOp; - case "<=" : - return VCExpressionGenerator.LeOp; - case "<" : - return VCExpressionGenerator.LtOp; - case ">=" : - return VCExpressionGenerator.GeOp; - case ">" : - return VCExpressionGenerator.GtOp; - case "and" : - return VCExpressionGenerator.AndOp; - case "or" : - return VCExpressionGenerator.OrOp; - case "not" : - return VCExpressionGenerator.NotOp; - case "ite" : - return VCExpressionGenerator.IfThenElseOp; - default: - return null; - } - } - - private class MyDeclHandler : TypeDeclCollector.DeclHandler { - public Dictionary var_map = new Dictionary(); - public Dictionary func_map = new Dictionary(); - public override void VarDecl(VCExprVar v){ - var_map[v.Name] = v; - } - public override void FuncDecl(Function f){ - func_map[f.Name] = f; - } - public MyDeclHandler() { - } - } - - private MyDeclHandler declHandler = null; - - private VCExprVar SExprToVar (SExpr e) - { - if(e.Arguments.Count() != 1){ - HandleProverError ("Prover error: bad quantifier syntax"); - throw new BadExprFromProver (); - } - string vname = StripCruft(e.Name); - SExpr vtype = e[0]; - switch(vtype.Name){ - case "Int": - return gen.Variable(vname,Type.Int); - case "Bool": - return gen.Variable (vname,Type.Bool); - case "Array":{ - // TODO: handle more general array types - var idxType = Type.Int; // well, could be something else - var valueType = - (vtype.Arguments[1].Name == "Int") ? Type.Int : Type.Bool; - var types = new List(); - types.Add(idxType); - return gen.Variable (vname, new MapType(Token.NoToken,new List(),types,valueType)); - } - default: { - HandleProverError ("Prover error: bad type: " + vtype.Name); - throw new BadExprFromProver (); - } - } - } - - private VCExpr MakeBinary(VCExprOp op, VCExpr [] args) - { - if (args.Count() == 0) - { - // with zero args we need the identity of the op - if (op == VCExpressionGenerator.AndOp) - return VCExpressionGenerator.True; - if (op == VCExpressionGenerator.OrOp) - return VCExpressionGenerator.False; - if (op == VCExpressionGenerator.AddIOp) - { - Microsoft.Basetypes.BigNum x = Microsoft.Basetypes.BigNum.ZERO; - return gen.Integer(x); - } - HandleProverError("Prover error: bad expression "); - throw new BadExprFromProver(); - } - var temp = args[0]; - for (int i = 1; i < args.Count(); i++) - temp = gen.Function(op, temp, args[i]); - return temp; - } - - protected VCExpr SExprToVCExpr (SExpr e, Dictionary bound) - { - if (e.Arguments.Count() == 0) { - var name = StripCruft(e.Name); - if (name [0] >= '0' && name [0] <= '9') { - Microsoft.Basetypes.BigNum x = Microsoft.Basetypes.BigNum.FromString(name); - return gen.Integer (x); - } - if (bound.ContainsKey (name)) { - return bound [name]; - } - if(name == "true") - return VCExpressionGenerator.True; - if(name == "false") - return VCExpressionGenerator.False; - if(declHandler.var_map.ContainsKey(name)) - return declHandler.var_map[name]; - HandleProverError ("Prover error: unknown symbol:" + name); - throw new BadExprFromProver (); - } - ArgGetter g = i => SExprToVCExpr (e [i], bound); - ArgsGetter ga = () => e.Arguments.Select (x => SExprToVCExpr (x, bound)).ToArray (); - VarsGetter gb = () => e [0].Arguments.Select (x => SExprToVar (x)).ToArray (); - switch (e.Name) { - case "select" : - return gen.Select (ga ()); - case "store" : - return gen.Store (ga ()); - case "forall": - case "exists": - { - var binds = e.Arguments[0]; - var vcbinds = new List(); - for (int i = 0; i < binds.Arguments.Count(); i++) - { - var bind = binds.Arguments[i]; - var symb = bind.Name; - var vcv = SExprToVar(bind); - vcbinds.Add(vcv); - bound[symb] = vcv; - } - var body = g(1); - if (e.Name == "forall") - body = gen.Forall(vcbinds, new List(), body); - else - body = gen.Exists(vcbinds, new List(), body); - for (int i = 0; i < binds.Arguments.Count(); i++) - { - var bind = binds.Arguments[i]; - var symb = bind.Name; - bound.Remove(symb); - } - return body; - } - case "-" : // have to deal with unary case - { - if(e.ArgCount == 1){ - var args = new VCExpr[2]; - args[0] = gen.Integer (Microsoft.Basetypes.BigNum.ZERO); - args[1] = g(0); - return gen.Function(VCStringToVCOp("-"),args); - } - return gen.Function(VCStringToVCOp("-"),ga()); - } - case "!" : // this is commentary - return g(0); - case "let" : { - // we expand lets exponentially since there is no let binding in Boogie surface syntax - bool expand_lets = true; - var binds = e.Arguments[0]; - var vcbinds = new List(); - for(int i = 0; i < binds.Arguments.Count(); i++){ - var bind = binds.Arguments[i]; - var symb = bind.Name; - var def = bind.Arguments[0]; - var vce = SExprToVCExpr(def, bound); - var vcv = gen.Variable(symb,vce.Type); - var vcb = gen.LetBinding(vcv,vce); - vcbinds.Add (vcb); - bound[symb] = expand_lets ? vce : vcv; - } - var body = g(1); - if(!expand_lets) - body = gen.Let(vcbinds,body); - for(int i = 0; i < binds.Arguments.Count(); i++){ - var bind = binds.Arguments[i]; - var symb = bind.Name; - bound.Remove (symb); - } - return body; - } - - default: { - var op = VCStringToVCOp (e.Name); - if (op == null) { - var name = StripCruft(e.Name); - if(declHandler.func_map.ContainsKey(name)){ - Function f = declHandler.func_map[name]; - return gen.Function (f, ga()); - } - HandleProverError ("Prover error: unknown operator:" + e.Name); - throw new BadExprFromProver (); - } - if(op.Arity == 2) - return MakeBinary (op, ga ()); - return gen.Function(op, ga()); - } - } - } - - private void SExprToSoln (SExpr resp, - Dictionary> varSubst) - { - Dictionary pmap = new Dictionary (); - - foreach (var node in rpfp.nodes) - pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node); - - var lines = resp.Arguments; - - // get all the predicate definitions - for (int i = 0; i < lines.Length; i++) { - var line = lines [i]; - string pname; - RPFP.Transformer annot; - GetDefun(line, out pname, out annot); - - if(pmap.ContainsKey(pname)){ - var node = pmap[pname]; - node.Annotation = annot; - } - else if(pname[0] != '@'){ // if not an internal symbol - HandleProverError ("Prover error: got unknown predicate:" + pname); - throw new BadExprFromProver (); - } - } - - } - - private void GetDefun(SExpr line, out string pname, out RPFP.Transformer annot) - { - if (line.Name != "define-fun") - { - HandleProverError("Prover error: expected define-fun but got:" + line.Name); - throw new BadExprFromProver(); - } - if (line.ArgCount != 4) - { - HandleProverError("Prover error: define-fun has wrong number of arguments"); - throw new BadExprFromProver(); - } - pname = StripCruft(line.Arguments[0].Name); - var pvars = line.Arguments[1]; - var pbody = line.Arguments[3]; // range has to be Bool - var binding = new Dictionary(); - var pvs = new List(); - foreach (var b in pvars.Arguments) - { - var e = SExprToVar(b); - pvs.Add(e); - binding.Add(StripCruft(b.Name), e); - } - VCExpr bexpr = SExprToVCExpr(pbody, binding); - - annot = rpfp.CreateRelation(pvs.ToArray(), bexpr); - } - - private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, - Dictionary> varSubst) - { - Dictionary nmap = new Dictionary(); - Dictionary pmap = new Dictionary(); - - foreach(var node in rpfp.nodes) - pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name,node); - - RPFP.Node topnode = null; - var lines = resp.Arguments; - - // last line of derivation is from query, skip it - for (int i = 0; i < lines.Length-1; i++) - { - var line = lines[i]; - if (line.ArgCount != 6) - { - HandleProverError("bad derivation line from prover: " + line.ToString()); - return null; - } - var name = line[0]; - var conseq = line[1]; - var rule = line[2]; - var subst = line[3]; - var labs = line[4]; - var refs = line[5]; - var predName = conseq.Name; - { - string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it! - int pos = predName.LastIndexOf(spacer); - if (pos >= 0) - predName = predName.Substring(0, pos); - } - RPFP.Node node = null; - if (!pmap.TryGetValue(predName, out node)) - { - HandleProverError("unknown predicate from prover: " + predName.ToString()); - return null; - } - RPFP.Node cexnode = rpfp.CloneNode(node); - cexnode.map = node; - nmap.Add(name.Name, cexnode); - List Chs = new List(); - - if (refs.Name != "ref") - { - HandleProverError("bad references from prover: " + refs.ToString()); - return null; - } - foreach (var c in refs.Arguments) - { - if (c.Name == "true") - Chs.Add(null); - else - { - RPFP.Node ch = null; - if (!nmap.TryGetValue(c.Name, out ch)) - { - HandleProverError("unknown reference from prover: " + c.ToString()); - return null; - } - Chs.Add(ch); - } - } - - if (!rule.Name.StartsWith("rule!")) - { - HandleProverError("bad rule name from prover: " + refs.ToString()); - return null; - } - int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1; - if (ruleNum < 0 || ruleNum > rpfp.edges.Count) - { - HandleProverError("bad rule name from prover: " + refs.ToString()); - return null; - } - RPFP.Edge orig_edge = rpfp.edges[ruleNum]; - RPFP.Edge e = rpfp.CreateEdge(cexnode, orig_edge.F, Chs.ToArray()); - e.map = orig_edge; - topnode = cexnode; - - if (labs.Name != "labels") - { - HandleProverError("bad labels from prover: " + labs.ToString()); - return null; - } - e.labels = new HashSet(); - foreach (var l in labs.Arguments) - e.labels.Add(l.Name); - - if (subst.Name != "subst") - { - HandleProverError("bad subst from prover: " + subst.ToString()); - return null; - } - Dictionary dict = new Dictionary(); - varSubst[e.number] = dict; - foreach (var s in subst.Arguments) - { - if (s.Name != "=" || s.Arguments.Length != 2) - { - HandleProverError("bad equation from prover: " + s.ToString()); - return null; - } - string uniqueName = s.Arguments[0].Name; - string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it! - int pos = uniqueName.LastIndexOf(spacer); - if (pos >= 0) - uniqueName = uniqueName.Substring(0, pos); - dict.Add(uniqueName, s.Arguments[1].ToString()); - } - - } - if (topnode == null) - { - HandleProverError("empty derivation from prover: " + resp.ToString()); - } - return topnode; - } - - private Model SExprToModel(SExpr resp, ErrorHandler handler) - { - // Concatenate all the arguments - string modelString = resp[0].Name; - // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")" - var models = Model.ParseModels(new StringReader("Error model: \n" + modelString)); - if (models == null || models.Count == 0) - { - HandleProverError("no model from prover: " + resp.ToString()); - } - return models[0]; - } - - private string QuantifiedVCExpr2String(VCExpr x) - { - return VCExpr2String(x, 1); -#if false - if (!(x is VCExprQuantifier)) - return VCExpr2String(x, 1); - VCExprQuantifier node = (x as VCExprQuantifier); - if(node.BoundVars.Count == 0) - return VCExpr2String(x, 1); - - StringWriter wr = new StringWriter(); - - string kind = node.Quan == Quantifier.ALL ? "forall" : "exists"; - wr.Write("({0} (", kind); - - for (int i = 0; i < node.BoundVars.Count; i++) - { - VCExprVar var = node.BoundVars[i]; - Contract.Assert(var != null); - string printedName = Namer.GetQuotedName(var, var.Name); - Contract.Assert(printedName != null); - wr.Write("({0} {1}) ", printedName, SMTLibExprLineariser.TypeToString(var.Type)); - } - - wr.Write(") "); - wr.Write(VCExpr2String(node.Body, 1)); - wr.Write(")"); - string res = wr.ToString(); - return res; -#endif - } - - public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler, - out RPFP.Node cex, - Dictionary> varSubst, - Dictionary extra_bound) - { - //Contract.Requires(descriptiveName != null); - //Contract.Requires(vc != null); - //Contract.Requires(handler != null); - rpfp = _rpfp; - cex = null; - - - if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen - - if (options.LogFilename != null && currentLogFile == null) - { - currentLogFile = OpenOutputFile(descriptiveName); - currentLogFile.Write(common.ToString()); - } - - PrepareCommon(); - - Push(); - SendThisVC("(fixedpoint-push)"); - foreach (var node in rpfp.nodes) - { - DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func); - } - - LineariserOptions.Default.LabelsBelowQuantifiers = true; - List ruleStrings = new List(); - var recursion_bound = CommandLineOptions.Clo.RecursionBound; - foreach (var edge in rpfp.edges) - { - string node_name = (edge.Parent.Name as VCExprBoogieFunctionOp).Func.Name; - string rule_name = "rule_" + edge.number.ToString(); - string rec_bound = ""; - if(extra_bound != null && extra_bound.ContainsKey(node_name)) - rec_bound = (recursion_bound + extra_bound[node_name]).ToString(); - string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + " " + rule_name + " " + rec_bound + "\n)"; - ruleStrings.Add(ruleString); - } - string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n :engine duality\n :print-certificate true\n"; - -#if true - if (CommandLineOptions.Clo.StratifiedInlining != 0) - queryString += " :stratified-inlining true\n"; - if (CommandLineOptions.Clo.RecursionBound > 0) - queryString += " :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n"; -#endif - queryString += ")"; - LineariserOptions.Default.LabelsBelowQuantifiers = false; - FlushAxioms(); - - PossiblyRestart(); - - SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); - foreach(var rs in ruleStrings) - SendThisVC(rs); - FlushLogFile(); - - if (Process != null) - { - Process.PingPong(); // flush any errors - -#if false - // TODO: this is not going to work - if (Process.Inspector != null) - Process.Inspector.NewProblem(descriptiveName, vc, handler); -#endif - } - - SendThisVC(queryString); - FlushLogFile(); - - var result = Outcome.Undetermined; - - if (Process != null) - { - - var resp = Process.GetProverResponse(); - - if (proverErrors.Count > 0) - { - result = Outcome.Undetermined; - foreach (var err in proverErrors) - { - if (err.Contains("canceled")) - { - result = Outcome.TimeOut; - } - } - } - else if(resp == null) - HandleProverError("Prover did not respond"); - else switch (resp.Name) - { - case "unsat": - result = Outcome.Valid; - break; - case "sat": - result = Outcome.Invalid; - break; - case "unknown": - result = Outcome.Invalid; - break; - case "error": - if (resp.ArgCount > 0 && resp.Arguments[0].Name.Contains("canceled")) - { - result = Outcome.TimeOut; - } - else - { - HandleProverError("Prover error: " + resp.Arguments[0]); - result = Outcome.Undetermined; - } - break; - default: - HandleProverError("Unexpected prover response: " + resp.ToString()); - break; - } - - switch (result) - { - case Outcome.Invalid: - { - resp = Process.GetProverResponse(); - if (resp.Name == "derivation") - { - cex = SExprToCex(resp, handler,varSubst); - } - else - HandleProverError("Unexpected prover response: " + resp.ToString()); - resp = Process.GetProverResponse(); - if (resp.Name == "model") - { - var model = SExprToModel(resp, handler); - cex.owner.SetBackgroundModel(model); - } - else - HandleProverError("Unexpected prover response: " + resp.ToString()); - break; - } - case Outcome.Valid: - { - resp = Process.GetProverResponse(); - if (resp.Name == "fixedpoint") - { - // only get the response if we need it - if(CommandLineOptions.Clo.PrintFixedPoint != null) - SExprToSoln(resp, varSubst); - } - else - HandleProverError("Unexpected prover response: " + resp.ToString()); - break; - } - default: - break; - } - -#if false - while (true) - { - resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - HandleProverError("Unexpected prover response: " + resp.ToString()); - } -#endif - } - SendThisVC("(fixedpoint-pop)"); - Pop(); - AxiomsAreSetup = false; - - if (CommandLineOptions.Clo.PrintConjectures != null) - { - ReadConjectures(CommandLineOptions.Clo.PrintConjectures); - } - - return result; - } - - class MyFileParser : SExpr.Parser - { - SMTLibProcessTheoremProver parent; - - public MyFileParser(System.IO.StreamReader _sr, SMTLibProcessTheoremProver _parent) - : base(_sr) - { - parent = _parent; - } - public override void ParseError(string msg) - { - parent.HandleProverError("Error in conjecture file from prover: " + msg); - } - } - - void ReadConjectures(string filename) - { - try - { - System.IO.StreamReader sr = new StreamReader(filename + ".tmp"); - SExpr.Parser p = new MyFileParser(sr, this); - var sexps = p.ParseSExprs(false); - Dictionary pmap = GetNodeMap(); - foreach (var e in sexps) - { - string pname; - RPFP.Transformer annot; - GetDefun(e, out pname, out annot); - - if (pmap.ContainsKey(pname)) - { - var c = new RPFP.Conjecture(); - c.node = pmap[pname]; - c.bound = annot; - rpfp.conjectures.Add(c); - } - else if (pname[0] != '@') - { // if not an internal symbol - HandleProverError("Prover error: got unknown predicate:" + pname); - throw new BadExprFromProver(); - } - } - sr.Close(); - } - catch (Exception) - { - HandleProverError("No conjecture file from prover"); - throw new BadExprFromProver(); - } - } - - private Dictionary GetNodeMap() - { - Dictionary pmap = new Dictionary(); - foreach (var node in rpfp.nodes) - pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name, node); - return pmap; - } - - private static HashSet usedLogNames = new HashSet(); - - private TextWriter OpenOutputFile(string descriptiveName) - { - Contract.Requires(descriptiveName != null); - Contract.Ensures(Contract.Result() != null); - - string filename = options.LogFilename; - filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename)); - var curFilename = filename; - - lock (usedLogNames) { - int n = 1; - while (usedLogNames.Contains(curFilename)) { - curFilename = filename + "." + n++; - } - usedLogNames.Add(curFilename); - } - - return new StreamWriter(curFilename, false); - } - - private void FlushProverWarnings() - { - var handler = currentErrorHandler; - if (handler != null) { - lock (proverWarnings) { - proverWarnings.Iter(handler.OnProverWarning); - proverWarnings.Clear(); - } - } - } - - protected void HandleProverError(string s) - { - s = s.Replace("\r", ""); - lock (proverWarnings) { - while (s.StartsWith("WARNING: ")) { - var idx = s.IndexOf('\n'); - var warn = s; - if (idx > 0) { - warn = s.Substring(0, idx); - s = s.Substring(idx + 1); - } else { - s = ""; - } - warn = warn.Substring(9); - proverWarnings.Add(warn); - } - } - - FlushProverWarnings(); - - if (s == "") return; - - lock (proverErrors) { - proverErrors.Add(s); - Console.WriteLine("Prover error: " + s); - } - } - - [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) - { - Contract.EnsuresOnThrow(true); - - var result = CheckOutcomeCore(handler, taskID: taskID); - SendThisVC("(pop 1)"); - FlushLogFile(); - - return result; - } - - [NoDefaultContract] - public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1) - { - Contract.EnsuresOnThrow(true); - - var result = Outcome.Undetermined; - - if (Process == null) - return result; - - try { - currentErrorHandler = handler; - FlushProverWarnings(); - - int errorsLeft; - if (CommandLineOptions.Clo.ConcurrentHoudini) { - Contract.Assert(taskID >= 0); - errorsLeft = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit; - } else { - errorsLeft = CommandLineOptions.Clo.ProverCCLimit; - } - - if (errorsLeft < 1) - errorsLeft = 1; - - var globalResult = Outcome.Undetermined; - - while (true) { - errorsLeft--; - string[] labels = null; - - result = GetResponse(); - if (globalResult == Outcome.Undetermined) - globalResult = result; - - if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) { - IList xlabels; - if (CommandLineOptions.Clo.UseLabels) { - labels = GetLabelsInfo(); - if (labels == null) - { - xlabels = new string[] { }; - } - else - { - xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); - } - } - else if(CommandLineOptions.Clo.SIBoolControlVC) { - labels = new string[0]; - xlabels = labels; - } else { - labels = CalculatePath(handler.StartingProcId()); - xlabels = labels; - } - Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null : - GetErrorModel(); - handler.OnModel(xlabels, model, result); - } - - if (labels == null || !labels.Any() || errorsLeft == 0) break; - - if (CommandLineOptions.Clo.UseLabels) { - var negLabels = labels.Where(l => l.StartsWith("@")).ToArray(); - var posLabels = labels.Where(l => !l.StartsWith("@")); - Func lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s)); - if (!options.MultiTraces) - posLabels = Enumerable.Empty(); - var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray(); - string expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); ; - if (!conjuncts.Any()) - { - expr = "false"; - } - SendThisVC("(assert " + expr + ")"); - SendThisVC("(check-sat)"); - } - else { - string source = labels[labels.Length - 2]; - string target = labels[labels.Length - 1]; - SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))"); - SendThisVC("(check-sat)"); - } - } - - FlushLogFile(); - - if (CommandLineOptions.Clo.RestartProverPerVC && Process != null) - Process.NeedsRestart = true; - - return globalResult; - - } finally { - currentErrorHandler = null; - } - } - - public override string[] CalculatePath(int controlFlowConstant) { - SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))"); - var path = new List(); - while (true) { - var resp = Process.GetProverResponse(); - if (resp == null) break; - if (!(resp.Name == "" && resp.ArgCount == 1)) break; - resp = resp.Arguments[0]; - if (!(resp.Name == "" && resp.ArgCount == 2)) break; - resp = resp.Arguments[1]; - var v = resp.Name; - if (v == "-" && resp.ArgCount == 1) { - v = resp.Arguments[0].Name; - path.Add(v); - break; - } - else if (resp.ArgCount != 0) - break; - path.Add(v); - SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))"); - } - return path.ToArray(); - } - - - private class SMTErrorModelConverter { - private struct SMTDataType { - public string Constructor; - public List Types; - } - - private List ErrorModelTodo; - private SMTLibProcessTheoremProver Parent; - private StringBuilder ErrorModel = new StringBuilder(); - private HashSet TopLevelProcessed = new HashSet(); - private int NumNewArrays = 0; - private Dictionary SortSet = new Dictionary(); - private Dictionary DataTypes = new Dictionary(); - private Dictionary Functions = new Dictionary(); - - public SMTErrorModelConverter(SExpr _ErrorModel, SMTLibProcessTheoremProver _Parent) { - ErrorModelTodo = _ErrorModel.Arguments.ToList();; - Parent = _Parent; - } - - public string Convert() { - ConvertErrorModel(ErrorModel); - return ErrorModel.ToString(); - } - - bool isConstArray(SExpr element, SExpr type) { - if (type.Name != "Array") - return false; - - if (element.Name == "__array_store_all__") // CVC4 1.4 - return true; - else if (element.Name == "" && element[0].Name == "as" && - element[0][0].Name == "const") // CVC4 > 1.4 - return true; - - return false; - } - - SExpr getConstArrayElement(SExpr element) { - if (element.Name == "__array_store_all__") // CVC4 1.4 - return element[1]; - else if (element.Name == "" && element[0].Name == "as" && - element[0][0].Name == "const") // CVC4 > 1.4 - return element[1]; - - Parent.HandleProverError("Unexpected value: " + element); - throw new BadExprFromProver (); - } - - void ConstructComplexValue(SExpr element, SExpr type, StringBuilder m) { - if (type.Name == "Array") { - if (element.Name == "store" || isConstArray(element, type)) { - NumNewArrays++; - m.Append("as-array[k!" + NumNewArrays + ']'); - SExpr[] args = {new SExpr("k!" + NumNewArrays), new SExpr(""), type, element}; - var newElement = new SExpr("define-fun", args); - TopLevelProcessed.Add(newElement); - ErrorModelTodo.Add(newElement); - return; - } - } - - ConstructSimpleValue(element, type, m); - } - - void ConstructSimpleValue(SExpr element, SExpr type, StringBuilder m) { - if (type.Name == "Bool" && element.ArgCount == 0) { - m.Append(element.ToString()); - return; - } - - if (type.Name == "Int") { - if (element.ArgCount == 0) { - m.Append(element.ToString()); - return; - } else if (element.Name == "-" && element.ArgCount == 1) { - m.Append(element.ToString()); - return; - } - } - - if (type.Name == "_" && type.ArgCount == 2 && type[0].Name == "BitVec") { - if (element.Name == "_" && element.ArgCount == 2 && - element[0].Name.StartsWith("bv") && element[0].ArgCount == 0 && - element[1].Name == type.Arguments[1].Name && element[1].ArgCount == 0) { - m.Append(element[0].Name + '[' + element[1].Name + ']'); - return; - } - } - - if (type.Name == "Array") { - while (element.Name == "store") { - ConstructComplexValue(element[1], type[0], m); - m.Append(" -> "); - ConstructComplexValue(element[2], type[1], m); - m.Append("\n "); - if (element[0].Name != "store") { - m.Append("else -> "); - } - element = element[0]; - } - - if (isConstArray(element, type)) { - ConstructComplexValue(getConstArrayElement(element), type[1], m); - return; - } else if (element.Name == "_" && element.ArgCount == 2 && - element[0].Name == "as-array") { - m.Append("as-array[" + element[1].Name + ']'); - return; - } - } - - if (SortSet.ContainsKey(type.Name) && SortSet[type.Name] == 0) { - var prefix = "@uc_T_" + type.Name.Substring(2) + "_"; - if (element.Name.StartsWith(prefix)) { - m.Append(type.Name + "!val!" + element.Name.Substring(prefix.Length)); - return; - } - } - - if (Functions.ContainsKey(element.Name) && - type.Name == Functions[element.Name].Name) { - m.Append(element.Name); - return; - } - - if (DataTypes.ContainsKey(type.Name) && - DataTypes[type.Name].Constructor == element.Name && - element.ArgCount == DataTypes[type.Name].Types.Count) { - m.Append("(" + element.Name); - for (int i = 0; i < element.ArgCount; ++i) { - m.Append(" "); - ConstructComplexValue(element[i], DataTypes[type.Name].Types[i], m); - } - m.Append(")"); - return; - } - - Parent.HandleProverError("Unexpected value: " + element); - throw new BadExprFromProver (); - } - - void ConstructFunctionArguments(SExpr arguments, List argTypes, StringBuilder[] argValues) { - if (arguments.Name == "and") { - ConstructFunctionArguments(arguments[0], argTypes, argValues); - ConstructFunctionArguments(arguments[1], argTypes, argValues); - } else if (arguments.Name == "=" && - (arguments[0].Name.StartsWith("_ufmt_") || arguments[0].Name.StartsWith("x!"))) { - int argNum; - if (arguments[0].Name.StartsWith("_ufmt_")) - argNum = System.Convert.ToInt32(arguments[0].Name.Substring("_uftm_".Length)) - 1; - else /* if (arguments[0].Name.StartsWith("x!")) */ - argNum = System.Convert.ToInt32(arguments[0].Name.Substring("x!".Length)) - 1; - if (argNum < 0 || argNum >= argTypes.Count) { - Parent.HandleProverError("Unexpected function argument: " + arguments[0]); - throw new BadExprFromProver (); - } - if (argValues[argNum] != null) { - Parent.HandleProverError("Function argument defined multiple times: " + arguments[0]); - throw new BadExprFromProver (); - } - argValues[argNum] = new StringBuilder(); - ConstructComplexValue(arguments[1], argTypes[argNum], argValues[argNum]); - } else { - Parent.HandleProverError("Unexpected function argument: " + arguments); - throw new BadExprFromProver (); - } - } - - void ConstructFunctionElements(SExpr element, List argTypes, SExpr outType, StringBuilder m) { - while (element.Name == "ite") { - StringBuilder[] argValues = new StringBuilder[argTypes.Count]; - ConstructFunctionArguments(element[0], argTypes, argValues); - foreach (var s in argValues) - m.Append(s + " "); - m.Append("-> "); - ConstructComplexValue(element[1], outType, m); - m.Append("\n "); - if (element[2].Name != "ite") - m.Append("else -> "); - element = element[2]; - } - - ConstructComplexValue(element, outType, m); - } - - void ConstructFunction(SExpr element, SExpr inType, SExpr outType, StringBuilder m) { - List argTypes = new List(); - - for (int i = 0; i < inType.ArgCount; ++i) { - if (inType[i].Name != "_ufmt_" + (i + 1) && inType[i].Name != "x!" + (i + 1) && - !inType[i].Name.StartsWith("BOUND_VARIABLE_")) { - Parent.HandleProverError("Unexpected function argument: " + inType[i].Name); - throw new BadExprFromProver (); - } - argTypes.Add(inType[i][0]); - } - - ConstructFunctionElements(element, argTypes, outType, m); - } - - void ConstructDefine(SExpr element, StringBuilder m) { - Debug.Assert(element.Name == "define-fun"); - - if (element[1].ArgCount != 0) - TopLevelProcessed.Add(element); - - m.Append(element[0] + " -> "); - if (TopLevelProcessed.Contains(element)) - m.Append("{\n "); - - if (element[1].ArgCount == 0 && element[2].Name == "Array" && !TopLevelProcessed.Contains(element)) { - ConstructComplexValue(element[3], element[2], m); - } else if (element[1].ArgCount == 0) { - ConstructSimpleValue(element[3], element[2], m); - } else { - ConstructFunction(element[3], element[1], element[2], m); - } - - if (TopLevelProcessed.Contains(element)) - m.Append("\n}"); - m.Append("\n"); - } - - void ExtractDataType(SExpr datatypes) { - Debug.Assert(datatypes.Name == "declare-datatypes"); - - if (datatypes[0].Name != "" || datatypes[1].Name != "" || datatypes[1].ArgCount != 1) { - Parent.HandleProverError("Unexpected datatype: " + datatypes); - throw new BadExprFromProver (); - } - - SMTDataType dt = new SMTDataType(); - SExpr typeDef = datatypes[1][0]; - - if (typeDef.ArgCount != 1) { - Parent.HandleProverError("Unexpected datatype: " + datatypes); - throw new BadExprFromProver (); - } - - dt.Constructor = typeDef[0].Name; - dt.Types = new List(); - - for (int i = 0; i < typeDef[0].ArgCount; ++i) { - if (typeDef[0][i].ArgCount != 1) { - Parent.HandleProverError("Unexpected datatype constructor: " + typeDef[0]); - throw new BadExprFromProver (); - } - dt.Types.Add(typeDef[0][i][0]); - } - - DataTypes[typeDef.Name] = dt; - } - - private void ConvertErrorModel(StringBuilder m) { - if (Parent.options.Solver == SolverKind.Z3) { - // Datatype declarations are not returned by Z3, so parse common - // instead. This is not very efficient, but currently not an issue, - // as this not the normal way of interfacing with Z3. - var ms = new MemoryStream(Encoding.ASCII.GetBytes(Parent.common.ToString())); - var sr = new StreamReader(ms); - SExpr.Parser p = new MyFileParser(sr, null); - var sexprs = p.ParseSExprs(false); - foreach (var e in sexprs) { - switch (e.Name) { - case "declare-datatypes": - ExtractDataType(e); - break; - } - } - } - - while (ErrorModelTodo.Count > 0) { - var e = ErrorModelTodo[0]; - ErrorModelTodo.RemoveAt(0); - - switch (e.Name) { - case "define-fun": - ConstructDefine(e, m); - break; - case "declare-sort": - SortSet[e[0].Name] = System.Convert.ToInt32(e[1].Name); - break; - case "declare-datatypes": - ExtractDataType(e); - break; - case "declare-fun": - if (e[1].Name != "" || e[1].ArgCount > 0 || e[2].ArgCount > 0 || - e[2].Name == "Bool" || e[2].Name == "Int") { - Parent.HandleProverError("Unexpected top level model element: " + e.Name); - throw new BadExprFromProver (); - } - Functions[e[0].Name] = e[2]; - break; - case "forall": - // ignore - break; - default: - Parent.HandleProverError("Unexpected top level model element: " + e.Name); - throw new BadExprFromProver (); - } - } - } - } - - private Model GetErrorModel() { - if (!options.ExpectingModel()) - return null; - SendThisVC("(get-model)"); - Process.Ping(); - Model theModel = null; - while (true) { - var resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - if (theModel != null) - HandleProverError("Expecting only one model but got many"); - - string modelStr = null; - if (resp.Name == "model" && resp.ArgCount >= 1) { - var converter = new SMTErrorModelConverter(resp, this); - modelStr = converter.Convert(); - } - else if (resp.ArgCount == 0 && resp.Name.Contains("->")) { - modelStr = resp.Name; - } - else { - HandleProverError("Unexpected prover response getting model: " + resp.ToString()); - } - - List models = null; - try { - switch (options.Solver) { - case SolverKind.Z3: - case SolverKind.CVC4: - models = Model.ParseModels(new StringReader("Error model: \n" + modelStr)); - break; - default: - Debug.Assert(false); - return null; - } - } - catch (ArgumentException exn) { - HandleProverError("Model parsing error: " + exn.Message); - } - if (models == null) - HandleProverError("Could not parse any models"); - else if (models.Count == 0) - HandleProverError("Could not parse any models"); - else if (models.Count > 1) - HandleProverError("Expecting only one model but got many"); - else - theModel = models[0]; - } - return theModel; - } - - private string[] GetLabelsInfo() - { - SendThisVC("(labels)"); - Process.Ping(); - - string[] res = null; - while (true) { - var resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - if (res != null) - HandleProverError("Expecting only one sequence of labels but got many"); - if (resp.Name == "labels" && resp.ArgCount >= 1) { - res = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray(); - } - else { - HandleProverError("Unexpected prover response getting labels: " + resp.ToString()); - } - } - return res; - } - - private Outcome GetResponse() - { - var result = Outcome.Undetermined; - var wasUnknown = false; - - Process.Ping(); - - while (true) { - var resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - - switch (resp.Name) { - case "unsat": - result = Outcome.Valid; - break; - case "sat": - result = Outcome.Invalid; - break; - case "unknown": - result = Outcome.Invalid; - wasUnknown = true; - break; - default: - HandleProverError("Unexpected prover response: " + resp.ToString()); - break; - } - } - - if (wasUnknown) { - SendThisVC("(get-info :reason-unknown)"); - Process.Ping(); - while (true) { - var resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - - if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") { - switch (resp[0].Name) { - case "memout": - currentErrorHandler.OnResourceExceeded("memory"); - result = Outcome.OutOfMemory; - Process.NeedsRestart = true; - break; - case "timeout": case "canceled": - currentErrorHandler.OnResourceExceeded("timeout"); - result = Outcome.TimeOut; - break; - default: - break; - } - } else { - HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString()); - } - } - - } - - return result; - } - - protected string VCExpr2String(VCExpr expr, int polarity) - { - Contract.Requires(expr != null); - Contract.Ensures(Contract.Result() != null); - - lock (gen) - { - DateTime start = DateTime.UtcNow; - //if (CommandLineOptions.Clo.Trace) - // Console.Write("Linearising ... "); - - // handle the types in the VCExpr - TypeEraser eraser; - switch (CommandLineOptions.Clo.TypeEncodingMethod) - { - case CommandLineOptions.TypeEncoding.Arguments: - eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen); - break; - case CommandLineOptions.TypeEncoding.Monomorphic: - eraser = null; - break; - default: - eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen); - break; - } - VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity); - Contract.Assert(exprWithoutTypes != null); - - LetBindingSorter letSorter = new LetBindingSorter(gen); - Contract.Assert(letSorter != null); - VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true); - Contract.Assert(sortedExpr != null); - VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true); - Contract.Assert(sortedAxioms != null); - - DeclCollector.Collect(sortedAxioms); - DeclCollector.Collect(sortedExpr); - FeedTypeDeclsToProver(); - - - - AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options)); - string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options); - Contract.Assert(res != null); - - if (CommandLineOptions.Clo.Trace) - { - DateTime end = DateTime.UtcNow; - TimeSpan elapsed = end - start; - if (elapsed.TotalSeconds > 0.5) - Console.WriteLine("Linearising [{0} s]", elapsed.TotalSeconds); - } - return res; - } - } - - // the list of all known axioms, where have to be included in each - // verification condition - private readonly List!*/> Axioms = new List(); - private bool AxiomsAreSetup = false; - - - - - // similarly, a list of function/predicate declarations - private readonly List!*/> TypeDecls = new List(); - - protected void AddAxiom(string axiom) - { - Contract.Requires(axiom != null); - Axioms.Add(axiom); - // if (thmProver != null) { - // LogActivity(":assume " + axiom); - // thmProver.AddAxioms(axiom); - // } - } - - protected void AddTypeDecl(string decl) - { - Contract.Requires(decl != null); - TypeDecls.Add(decl); - // if (thmProver != null) { - // LogActivity(decl); - // thmProver.Feed(decl, 0); - // } - } - - //////////////////////////////////////////////////////////////////////////// - - private static string _backgroundPredicates; - - static void InitializeGlobalInformation() - { - Contract.Ensures(_backgroundPredicates != null); - //throws ProverException, System.IO.FileNotFoundException; - if (_backgroundPredicates == null) { - if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) - { - _backgroundPredicates = ""; - } - else - { - _backgroundPredicates = @" -(set-info :category ""industrial"") -(declare-sort |T@U| 0) -(declare-sort |T@T| 0) -(declare-fun real_pow (Real Real) Real) -(declare-fun UOrdering2 (|T@U| |T@U|) Bool) -(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)"; - } - } - } - - public override VCExpressionGenerator VCExprGen - { - get { return this.gen; } - } - - //// Push/pop interface - - //List pushedAssertions = new List(); - //int numRealPushes; - public override string VCExpressionToString(VCExpr vc) - { - return VCExpr2String(vc, 1); - } - - public override void PushVCExpression(VCExpr vc) - { - throw new NotImplementedException(); - - } - - public override void Pop() - { - SendThisVC("(pop 1)"); - DeclCollector.Pop(); - } - - public override int NumAxiomsPushed() - { - throw new NotImplementedException(); - //return numRealPushes + pushedAssertions.Count; - } - - private void FlushPushedAssertions() - { - throw new NotImplementedException(); - } - - public override void Assert(VCExpr vc, bool polarity) - { - string a = ""; - if (polarity) - { - a = "(assert " + VCExpr2String(vc, 1) + ")"; - } - else - { - a = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; - } - AssertAxioms(); - SendThisVC(a); - } - - public override void DefineMacro(Macro f, VCExpr vc) { - DeclCollector.AddFunction(f); - string printedName = Namer.GetQuotedName(f, f.Name); - var argTypes = f.InParams.Cast().MapConcat(p => DeclCollector.TypeToStringReg(p.TypedIdent.Type), " "); - string decl = "(define-fun " + printedName + " (" + argTypes + ") " + DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VCExpr2String(vc, 1) + ")"; - AssertAxioms(); - SendThisVC(decl); - } - - public override void AssertAxioms() - { - FlushAxioms(); - } - - public override void Check() - { - PrepareCommon(); - SendThisVC("(check-sat)"); - FlushLogFile(); - } - - public override void SetTimeOut(int ms) - { - if (options.Solver == SolverKind.Z3) { - var name = Z3.SetTimeoutOption(); - var value = ms.ToString(); - options.TimeLimit = ms; - options.SmtOptions.RemoveAll(ov => ov.Option == name); - options.AddSmtOption(name, value); - SendThisVC(string.Format("(set-option :{0} {1})", name, value)); - } - } - - public override object Evaluate(VCExpr expr) - { - string vcString = VCExpr2String(expr, 1); - SendThisVC("(get-value (" + vcString + "))"); - var resp = Process.GetProverResponse(); - if (resp == null) throw new VCExprEvaluationException(); - if (!(resp.Name == "" && resp.ArgCount == 1)) throw new VCExprEvaluationException(); - resp = resp.Arguments[0]; - if (resp.Name == "") - { - // evaluating an expression - if (resp.ArgCount == 2) - resp = resp.Arguments[1]; - else - throw new VCExprEvaluationException(); - } - else - { - // evaluating a variable - if (resp.ArgCount == 1) - resp = resp.Arguments[0]; - else - throw new VCExprEvaluationException(); - } - if (resp.Name == "-" && resp.ArgCount == 1) // negative int - return Microsoft.Basetypes.BigNum.FromString("-" + resp.Arguments[0].Name); - if (resp.Name == "_" && resp.ArgCount == 2 && resp.Arguments[0].Name.StartsWith("bv")) // bitvector - return new BvConst(Microsoft.Basetypes.BigNum.FromString(resp.Arguments[0].Name.Substring("bv".Length)), - int.Parse(resp.Arguments[1].Name)); - if (resp.ArgCount != 0) - throw new VCExprEvaluationException(); - if (expr.Type.Equals(Boogie.Type.Bool)) - return bool.Parse(resp.Name); - else if (expr.Type.Equals(Boogie.Type.Int)) - return Microsoft.Basetypes.BigNum.FromString(resp.Name); - else - return resp.Name; - } - - /// - /// Extra state for ApiChecker (used by stratifiedInlining) - /// - static int nameCounter = 0; - - public override Outcome CheckAssumptions(List assumptions, out List unsatCore, ErrorHandler handler) - { - unsatCore = new List(); - - Push(); - // Name the assumptions - var nameToAssumption = new Dictionary(); - int i = 0; - foreach (var vc in assumptions) - { - var name = "a" + nameCounter.ToString(); - nameCounter++; - nameToAssumption.Add(name, i); - - string vcString = VCExpr2String(vc, 1); - AssertAxioms(); - SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); - i++; - } - Check(); - - var outcome = CheckOutcomeCore(handler); - - if (outcome != Outcome.Valid) { - Pop(); - return outcome; - } - - Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores"); - SendThisVC("(get-unsat-core)"); - var resp = Process.GetProverResponse(); - unsatCore = new List(); - if (resp.Name != "") unsatCore.Add(nameToAssumption[resp.Name]); - foreach (var s in resp.Arguments) unsatCore.Add(nameToAssumption[s.Name]); - - FlushLogFile(); - Pop(); - return outcome; - } - - public override void Push() - { - SendThisVC("(push 1)"); - DeclCollector.Push(); - } - - public override Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions, ErrorHandler handler) { - unsatisfiedSoftAssumptions = new List(); - - // First, convert both hard and soft assumptions to SMTLIB strings - List hardAssumptionStrings = new List(); - foreach (var a in hardAssumptions) { - hardAssumptionStrings.Add(VCExpr2String(a, 1)); - } - List currAssumptionStrings = new List(); - foreach (var a in softAssumptions) { - currAssumptionStrings.Add(VCExpr2String(a, 1)); - } - - Push(); - AssertAxioms(); - foreach (var a in hardAssumptionStrings) { - SendThisVC("(assert " + a + ")"); - } - Check(); - Outcome outcome = GetResponse(); - if (outcome != Outcome.Invalid) { - Pop(); - return outcome; - } - - int k = 0; - List relaxVars = new List(); - while (true) { - Push(); - foreach (var a in currAssumptionStrings) { - SendThisVC("(assert " + a + ")"); - } - Check(); - outcome = CheckOutcomeCore(handler); - if (outcome != Outcome.Valid) - break; - Pop(); - string relaxVar = "relax_" + k; - relaxVars.Add(relaxVar); - SendThisVC("(declare-fun " + relaxVar + " () Int)"); - List nextAssumptionStrings = new List(); - for (int i = 0; i < currAssumptionStrings.Count; i++) { - string constraint = "(= " + relaxVar + " " + i + ")"; - nextAssumptionStrings.Add("(or " + currAssumptionStrings[i] + " " + constraint + ")"); - } - currAssumptionStrings = nextAssumptionStrings; - k++; - } - - if (outcome == Outcome.Invalid) { - foreach (var relaxVar in relaxVars) { - SendThisVC("(get-value (" + relaxVar + "))"); - FlushLogFile(); - var resp = Process.GetProverResponse(); - if (resp == null) break; - if (!(resp.Name == "" && resp.ArgCount == 1)) break; - resp = resp.Arguments[0]; - if (!(resp.Name != "" && resp.ArgCount == 1)) break; - resp = resp.Arguments[0]; - if (resp.ArgCount != 0) - break; - int v; - if (int.TryParse(resp.Name, out v)) - unsatisfiedSoftAssumptions.Add(v); - else - break; - } - Pop(); - } - - Pop(); - return outcome; - } - } - - public class SMTLibInterpolatingProcessTheoremProver : SMTLibProcessTheoremProver - { - public SMTLibInterpolatingProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen, - SMTLibProverContext ctx) - : base(AddInterpOption(options), gen, ctx) - { - - } - - private static ProverOptions AddInterpOption(ProverOptions options) - { - var opts = (SMTLibProverOptions)options; - opts.AddSmtOption("produce-interpolants", "true"); - if (CommandLineOptions.Clo.PrintFixedPoint == null) - CommandLineOptions.Clo.PrintFixedPoint = "itp.fixedpoint.bpl"; - return opts; - } - - public override void AssertNamed(VCExpr vc, bool polarity, string name) - { - string vcString; - if (polarity) - { - vcString = VCExpr2String(vc, 1); - } - else - { - vcString = "(not " + VCExpr2String(vc, 1) + ")"; - } - AssertAxioms(); - SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); - } - - public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B) - { - string A_str = VCExpr2String(A, 1); - string B_str = VCExpr2String(B, 1); - - AssertAxioms(); - SendThisVC("(compute-interpolant " + A_str + " " + B_str + ")"); - - SExpr interpolant; - Outcome result = GetInterpolantResponse(out interpolant); - - if (result != Outcome.Valid) - return null; - - VCExpr interpolantVC = SExprToVCExpr(interpolant, new Dictionary()); - return interpolantVC; - } - - private Outcome GetInterpolantResponse(out SExpr interpolant) - { - var result = Outcome.Undetermined; - var wasUnknown = false; - interpolant = null; - - Process.Ping(); - bool onlyOnce = false; - - while (true) - { - var resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - - switch (resp.Name) - { - case "unsat": - result = Outcome.Valid; - break; - case "sat": - result = Outcome.Invalid; - break; - case "unknown": - result = Outcome.Invalid; - wasUnknown = true; - break; - default: - if (result == Outcome.Valid) - { - interpolant = resp as SExpr; - - Contract.Assert(onlyOnce == false); - onlyOnce = true; - continue; - } - HandleProverError("Unexpected prover response: " + resp.ToString()); - break; - } - } - - if (wasUnknown) - { - SendThisVC("(get-info :reason-unknown)"); - Process.Ping(); - - while (true) - { - var resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - - if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") - { - switch (resp[0].Name) - { - case "memout": - currentErrorHandler.OnResourceExceeded("memory"); - result = Outcome.OutOfMemory; - Process.NeedsRestart = true; - break; - case "timeout": - case "canceled": - currentErrorHandler.OnResourceExceeded("timeout"); - result = Outcome.TimeOut; - break; - default: - break; - } - } - else - { - HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString()); - } - } - } - - return result; - } - - public override List GetTreeInterpolant(List root, List leaves) - { - List result = new List(); - - string vcStr = "true"; - foreach (string str in root) - vcStr = vcStr + " " + str; - foreach (string str in leaves) - vcStr = vcStr + "\r\n (interp " + str + ")"; - - vcStr = "(get-interpolant (and\r\n" + vcStr + "\r\n))"; - SendThisVC(vcStr); - if(currentLogFile != null) currentLogFile.Flush(); - - List interpolantList; - GetTreeInterpolantResponse(out interpolantList); - - Dictionary bound = new Dictionary(); - foreach (SExpr sexpr in interpolantList) - { - VCExpr interpolantVC = SExprToVCExpr(sexpr, bound); - result.Add(interpolantVC); - } - - return result; - } - - private void GetTreeInterpolantResponse(out List interpolantList) - { - interpolantList = new List(); - - Process.Ping(); - - while (true) - { - var resp = Process.GetProverResponse(); - if (resp == null || Process.IsPong(resp)) - break; - - SExpr interpolant = resp as SExpr; - if(interpolant == null) - HandleProverError("Unexpected prover response: got null for interpolant!"); - interpolantList.Add(interpolant); - } - } - } - - public class SMTLibProverContext : DeclFreeProverContext - { - internal SMTLibProcessTheoremProver parent; - - public readonly Dictionary> KnownDatatypeConstructors = new Dictionary>(); - - public SMTLibProverContext(VCExpressionGenerator gen, - VCGenerationOptions genOptions) - : base(gen, genOptions) - { - } - - protected SMTLibProverContext(SMTLibProverContext par) - : base(par) - { - } - - public override object Clone() - { - return new SMTLibProverContext(this); - } - - public override string Lookup(VCExprVar var) - { - VCExprVar v = parent.AxBuilder.TryTyped2Untyped(var); - if (v != null) { - var = v; - } - return parent.Namer.Lookup(var); - } - - public override void DeclareFunction(Function f, string attributes) { - if (f is DatatypeConstructor) { - CtorType datatype = (CtorType) f.OutParams[0].TypedIdent.Type; - if (!KnownDatatypeConstructors.ContainsKey(datatype)) - KnownDatatypeConstructors[datatype] = new List(); - KnownDatatypeConstructors[datatype].Add(f); - } - base.DeclareFunction(f, attributes); - } - } - - public class Factory : ProverFactory - { - // Set programmatically - public static bool UseInterpolation = false; - - public override object SpawnProver(ProverOptions options, object ctxt) - { - //Contract.Requires(ctxt != null); - //Contract.Requires(options != null); - Contract.Ensures(Contract.Result() != null); - - return this.SpawnProver(options, - cce.NonNull((SMTLibProverContext)ctxt).ExprGen, - cce.NonNull((SMTLibProverContext)ctxt)); - } - - public override object NewProverContext(ProverOptions options) - { - //Contract.Requires(options != null); - Contract.Ensures(Contract.Result() != null); - - VCExpressionGenerator gen = new VCExpressionGenerator(); - List/*!>!*/ proverCommands = new List(); - proverCommands.Add("smtlib"); - var opts = (SMTLibProverOptions)options ; - if (opts.Solver == SolverKind.Z3) - proverCommands.Add("z3"); - else - proverCommands.Add("external"); - VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands); - return new SMTLibProverContext(gen, genOptions); - } - - public override ProverOptions BlankProverOptions() - { - return new SMTLibProverOptions(); - } - - protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options, - VCExpressionGenerator gen, - SMTLibProverContext ctx) - { - Contract.Requires(options != null); - Contract.Requires(gen != null); - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); - - if (UseInterpolation) - return new SMTLibInterpolatingProcessTheoremProver(options, gen, ctx); - - return new SMTLibProcessTheoremProver(options, gen, ctx); - } - - public override bool SupportsLabels(ProverOptions options) - { - return ((SMTLibProverOptions)options).SupportsLabels; - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +//using ExternalProver; +using System.Linq; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.VCExprAST; +using Microsoft.Boogie.Clustering; +using Microsoft.Boogie.TypeErasure; +using System.Text; + +using RPFP = Microsoft.Boogie.RPFP; + +namespace Microsoft.Boogie.SMTLib +{ + public class SMTLibProcessTheoremProver : ProverInterface + { + private readonly SMTLibProverContext ctx; + private VCExpressionGenerator gen; + private readonly SMTLibProverOptions options; + private bool usingUnsatCore; + private RPFP rpfp = null; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(ctx != null); + Contract.Invariant(AxBuilder != null); + Contract.Invariant(Namer != null); + Contract.Invariant(DeclCollector != null); + Contract.Invariant(cce.NonNullElements(Axioms)); + Contract.Invariant(cce.NonNullElements(TypeDecls)); + Contract.Invariant(_backgroundPredicates != null); + + } + + + [NotDelayed] + public SMTLibProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen, + SMTLibProverContext ctx) + { + Contract.Requires(options != null); + Contract.Requires(gen != null); + Contract.Requires(ctx != null); + + InitializeGlobalInformation(); + + this.options = (SMTLibProverOptions)options; + this.ctx = ctx; + this.gen = gen; + this.usingUnsatCore = false; + + SetupAxiomBuilder(gen); + + Namer = new SMTLibNamer(); + ctx.parent = this; + this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer); + + if (CommandLineOptions.Clo.PrintFixedPoint != null || CommandLineOptions.Clo.PrintConjectures != null) + { + declHandler = new MyDeclHandler(); + DeclCollector.SetDeclHandler(declHandler); + } + + SetupProcess(); + + if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer + || CommandLineOptions.Clo.SecureVcGen != null) + { + // Prepare for ApiChecker usage + if (options.LogFilename != null && currentLogFile == null) + { + currentLogFile = OpenOutputFile(""); + } + PrepareCommon(); + } + } + + public override void AssertNamed(VCExpr vc, bool polarity, string name) + { + string vcString; + if (polarity) + { + vcString = VCExpr2String(vc, 1); + } + else + { + vcString = "(not " + VCExpr2String(vc, 1) + ")"; + } + AssertAxioms(); + SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); + } + + private void SetupAxiomBuilder(VCExpressionGenerator gen) + { + switch (CommandLineOptions.Clo.TypeEncodingMethod) + { + case CommandLineOptions.TypeEncoding.Arguments: + AxBuilder = new TypeAxiomBuilderArguments(gen); + AxBuilder.Setup(); + break; + case CommandLineOptions.TypeEncoding.Monomorphic: + AxBuilder = new TypeAxiomBuilderPremisses(gen); + break; + default: + AxBuilder = new TypeAxiomBuilderPremisses(gen); + AxBuilder.Setup(); + break; + } + } + + ProcessStartInfo ComputeProcessStartInfo() + { + var path = this.options.ProverPath; + switch (options.Solver) { + case SolverKind.Z3: + if (path == null) + path = Z3.ExecutablePath(); + return SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in"); + case SolverKind.CVC4: + if (path == null) + path = CVC4.ExecutablePath(); + return SMTLibProcess.ComputerProcessStartInfo(path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental"); + default: + Debug.Assert(false); + return null; + } + } + + void SetupProcess() + { + if (Process != null) return; + + var psi = ComputeProcessStartInfo(); + Process = new SMTLibProcess(psi, this.options); + Process.ErrorHandler += this.HandleProverError; + } + + + void PossiblyRestart() + { + if (Process != null && Process.NeedsRestart) { + Process.Close(); + Process = null; + SetupProcess(); + Process.Send(common.ToString()); + } + } + + public override ProverContext Context + { + get + { + Contract.Ensures(Contract.Result() != null); + + return ctx; + } + } + + internal TypeAxiomBuilder AxBuilder { get; private set; } + internal readonly UniqueNamer Namer; + readonly TypeDeclCollector DeclCollector; + protected SMTLibProcess Process; + readonly List proverErrors = new List(); + readonly List proverWarnings = new List(); + readonly StringBuilder common = new StringBuilder(); + protected TextWriter currentLogFile; + protected volatile ErrorHandler currentErrorHandler; + + private void FeedTypeDeclsToProver() + { + foreach (string s in DeclCollector.GetNewDeclarations()) { + Contract.Assert(s != null); + AddTypeDecl(s); + } + } + + private string Sanitize(string msg) + { + var idx = msg.IndexOf('\n'); + if (idx > 0) + msg = msg.Replace("\r", "").Replace("\n", "\r\n"); + return msg; + } + + public override void LogComment(string comment) + { + SendCommon("; " + comment); + } + + private void SendCommon(string s) + { + Send(s, true); + } + + protected void SendThisVC(string s) + { + Send(s, false); + } + + private void Send(string s, bool isCommon) + { + s = Sanitize(s); + + if (isCommon) + common.Append(s).Append("\r\n"); + + if (Process != null) + Process.Send(s); + if (currentLogFile != null) { + currentLogFile.WriteLine(s); + currentLogFile.Flush(); + } + } + + private void FindDependentTypes(Type type, List dependentTypes) + { + MapType mapType = type as MapType; + if (mapType != null) + { + foreach (Type t in mapType.Arguments) + { + FindDependentTypes(t, dependentTypes); + } + FindDependentTypes(mapType.Result, dependentTypes); + } + CtorType ctorType = type as CtorType; + if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey(ctorType)) + { + dependentTypes.Add(ctorType); + } + } + + private void PrepareCommon() + { + if (common.Length == 0) + { + SendCommon("(set-option :print-success false)"); + SendCommon("(set-info :smt-lib-version 2.0)"); + if (options.ProduceModel()) + SendCommon("(set-option :produce-models true)"); + foreach (var opt in options.SmtOptions) + { + SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); + } + + if (!string.IsNullOrEmpty(options.Logic)) + { + SendCommon("(set-logic " + options.Logic + ")"); + } + + // Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value + // gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 ) + if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))) + { + SendCommon("(set-option :produce-unsat-cores true)"); + this.usingUnsatCore = true; + } + + SendCommon("; done setting options\n"); + SendCommon(_backgroundPredicates); + + if (options.UseTickleBool) + { + SendCommon("(declare-fun tickleBool (Bool) Bool)"); + SendCommon("(assert (and (tickleBool true) (tickleBool false)))"); + } + + if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout) + { + SendCommon("(declare-fun timeoutDiagnostics (Int) Bool)"); + } + + if (ctx.KnownDatatypeConstructors.Count > 0) + { + GraphUtil.Graph dependencyGraph = new GraphUtil.Graph(); + foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) + { + dependencyGraph.AddSource(datatype); + foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) + { + List dependentTypes = new List(); + foreach (Variable v in f.InParams) + { + FindDependentTypes(v.TypedIdent.Type, dependentTypes); + } + foreach (CtorType result in dependentTypes) + { + dependencyGraph.AddEdge(datatype, result); + } + } + } + GraphUtil.StronglyConnectedComponents sccs = new GraphUtil.StronglyConnectedComponents(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors); + sccs.Compute(); + foreach (GraphUtil.SCC scc in sccs) + { + string datatypeString = ""; + foreach (CtorType datatype in scc) + { + datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " "; + foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) + { + string quotedConstructorName = Namer.GetQuotedName(f, f.Name); + if (f.InParams.Count == 0) + { + datatypeString += quotedConstructorName + " "; + } + else + { + datatypeString += "(" + quotedConstructorName + " "; + foreach (Variable v in f.InParams) + { + string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name); + datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") "; + } + datatypeString += ") "; + } + } + datatypeString += ") "; + } + List decls = DeclCollector.GetNewDeclarations(); + foreach (string decl in decls) + { + SendCommon(decl); + } + SendCommon("(declare-datatypes () (" + datatypeString + "))"); + } + } + if (CommandLineOptions.Clo.ProverPreamble != null) + SendCommon("(include \"" + CommandLineOptions.Clo.ProverPreamble + "\")"); + } + + if (!AxiomsAreSetup) + { + var axioms = ctx.Axioms; + var nary = axioms as VCExprNAry; + if (nary != null && nary.Op == VCExpressionGenerator.AndOp) + foreach (var expr in nary.UniformArguments) + { + var str = VCExpr2String(expr, -1); + if (str != "true") + AddAxiom(str); + } + else + AddAxiom(VCExpr2String(axioms, -1)); + AxiomsAreSetup = true; + } + } + + public override int FlushAxiomsToTheoremProver() + { + // we feed the axioms when begincheck is called. + return 0; + } + + private void FlushAxioms() + { + TypeDecls.Iter(SendCommon); + TypeDecls.Clear(); + foreach (string s in Axioms) { + Contract.Assert(s != null); + if (s != "true") + SendCommon("(assert " + s + ")"); + } + Axioms.Clear(); + //FlushPushedAssertions(); + } + + private void CloseLogFile() + { + if (currentLogFile != null) { + currentLogFile.Close(); + currentLogFile = null; + } + } + + private void FlushLogFile() + { + if (currentLogFile != null) { + currentLogFile.Flush(); + } + } + + public override void Close() + { + base.Close(); + CloseLogFile(); + if (Process != null) + Process.Close(); + } + + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) + { + //Contract.Requires(descriptiveName != null); + //Contract.Requires(vc != null); + //Contract.Requires(handler != null); + rpfp = null; + + if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen + + if (options.LogFilename != null && currentLogFile == null) + { + currentLogFile = OpenOutputFile(descriptiveName); + currentLogFile.Write(common.ToString()); + } + + PrepareCommon(); + + OptimizationRequests.Clear(); + + string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; + FlushAxioms(); + + PossiblyRestart(); + + SendThisVC("(push 1)"); + SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + + SendThisVC(vcString); + + SendOptimizationRequests(); + + FlushLogFile(); + + if (Process != null) { + Process.PingPong(); // flush any errors + + if (Process.Inspector != null) + Process.Inspector.NewProblem(descriptiveName, vc, handler); + } + + SendCheckSat(); + FlushLogFile(); + } + + private void SendOptimizationRequests() + { + if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count) + { + foreach (var r in OptimizationRequests) + { + SendThisVC(r); + } + } + } + + public override void Reset(VCExpressionGenerator gen) + { + if (options.Solver == SolverKind.Z3) + { + this.gen = gen; + SendThisVC("(reset)"); + + if (0 < common.Length) + { + var c = common.ToString(); + Process.Send(c); + if (currentLogFile != null) + { + currentLogFile.WriteLine(c); + } + } + } + } + + public override void FullReset(VCExpressionGenerator gen) + { + if (options.Solver == SolverKind.Z3) + { + this.gen = gen; + SendThisVC("(reset)"); + Namer.Reset(); + common.Clear(); + SetupAxiomBuilder(gen); + Axioms.Clear(); + TypeDecls.Clear(); + AxiomsAreSetup = false; + ctx.Reset(); + ctx.KnownDatatypeConstructors.Clear(); + ctx.parent = this; + DeclCollector.Reset(); + NamedAssumes.Clear(); + UsedNamedAssumes = null; + SendThisVC("; did a full reset"); + } + } + + + + private string StripCruft(string name){ + if(name.Contains("@@")) + return name.Remove(name.LastIndexOf ("@@")); + return name; + } + + private class BadExprFromProver : Exception + { + }; + + private delegate VCExpr ArgGetter (int pos); + + private delegate VCExpr[] ArgsGetter (); + + private delegate VCExprVar[] VarsGetter (); + + private VCExprOp VCStringToVCOp (string op) + { + switch (op) { + case "+" : + return VCExpressionGenerator.AddIOp; + case "-" : + return VCExpressionGenerator.SubIOp; + case "*" : + return VCExpressionGenerator.MulIOp; + case "div" : + return VCExpressionGenerator.DivIOp; + case "=" : + return VCExpressionGenerator.EqOp; + case "<=" : + return VCExpressionGenerator.LeOp; + case "<" : + return VCExpressionGenerator.LtOp; + case ">=" : + return VCExpressionGenerator.GeOp; + case ">" : + return VCExpressionGenerator.GtOp; + case "and" : + return VCExpressionGenerator.AndOp; + case "or" : + return VCExpressionGenerator.OrOp; + case "not" : + return VCExpressionGenerator.NotOp; + case "ite" : + return VCExpressionGenerator.IfThenElseOp; + default: + return null; + } + } + + private class MyDeclHandler : TypeDeclCollector.DeclHandler { + public Dictionary var_map = new Dictionary(); + public Dictionary func_map = new Dictionary(); + public override void VarDecl(VCExprVar v){ + var_map[v.Name] = v; + } + public override void FuncDecl(Function f){ + func_map[f.Name] = f; + } + public MyDeclHandler() { + } + } + + private MyDeclHandler declHandler = null; + + private VCExprVar SExprToVar (SExpr e) + { + if(e.Arguments.Count() != 1){ + HandleProverError ("Prover error: bad quantifier syntax"); + throw new BadExprFromProver (); + } + string vname = StripCruft(e.Name); + SExpr vtype = e[0]; + switch(vtype.Name){ + case "Int": + return gen.Variable(vname,Type.Int); + case "Bool": + return gen.Variable (vname,Type.Bool); + case "Array":{ + // TODO: handle more general array types + var idxType = Type.Int; // well, could be something else + var valueType = + (vtype.Arguments[1].Name == "Int") ? Type.Int : Type.Bool; + var types = new List(); + types.Add(idxType); + return gen.Variable (vname, new MapType(Token.NoToken,new List(),types,valueType)); + } + default: { + HandleProverError ("Prover error: bad type: " + vtype.Name); + throw new BadExprFromProver (); + } + } + } + + private VCExpr MakeBinary(VCExprOp op, VCExpr [] args) + { + if (args.Count() == 0) + { + // with zero args we need the identity of the op + if (op == VCExpressionGenerator.AndOp) + return VCExpressionGenerator.True; + if (op == VCExpressionGenerator.OrOp) + return VCExpressionGenerator.False; + if (op == VCExpressionGenerator.AddIOp) + { + Microsoft.Basetypes.BigNum x = Microsoft.Basetypes.BigNum.ZERO; + return gen.Integer(x); + } + HandleProverError("Prover error: bad expression "); + throw new BadExprFromProver(); + } + var temp = args[0]; + for (int i = 1; i < args.Count(); i++) + temp = gen.Function(op, temp, args[i]); + return temp; + } + + protected VCExpr SExprToVCExpr (SExpr e, Dictionary bound) + { + if (e.Arguments.Count() == 0) { + var name = StripCruft(e.Name); + if (name [0] >= '0' && name [0] <= '9') { + Microsoft.Basetypes.BigNum x = Microsoft.Basetypes.BigNum.FromString(name); + return gen.Integer (x); + } + if (bound.ContainsKey (name)) { + return bound [name]; + } + if(name == "true") + return VCExpressionGenerator.True; + if(name == "false") + return VCExpressionGenerator.False; + if(declHandler.var_map.ContainsKey(name)) + return declHandler.var_map[name]; + HandleProverError ("Prover error: unknown symbol:" + name); + //throw new BadExprFromProver (); + var v = gen.Variable(name, Type.Int); + bound.Add(name, v); + return v; + } + ArgGetter g = i => SExprToVCExpr (e [i], bound); + ArgsGetter ga = () => e.Arguments.Select (x => SExprToVCExpr (x, bound)).ToArray (); + VarsGetter gb = () => e [0].Arguments.Select (x => SExprToVar (x)).ToArray (); + switch (e.Name) { + case "select" : + return gen.Select (ga ()); + case "store" : + return gen.Store (ga ()); + case "forall": + case "exists": + { + var binds = e.Arguments[0]; + var vcbinds = new List(); + var bound_copy = new Dictionary(bound); + for (int i = 0; i < binds.Arguments.Count(); i++) + { + var bind = binds.Arguments[i]; + var symb = StripCruft(bind.Name); + var vcv = SExprToVar(bind); + vcbinds.Add(vcv); + bound[symb] = vcv; + } + var body = g(1); + if (e.Name == "forall") + body = gen.Forall(vcbinds, new List(), body); + else + body = gen.Exists(vcbinds, new List(), body); + bound = bound_copy; + return body; + } + case "-" : // have to deal with unary case + { + if(e.ArgCount == 1){ + var args = new VCExpr[2]; + args[0] = gen.Integer (Microsoft.Basetypes.BigNum.ZERO); + args[1] = g(0); + return gen.Function(VCStringToVCOp("-"),args); + } + return gen.Function(VCStringToVCOp("-"),ga()); + } + case "!" : // this is commentary + return g(0); + case "let" : { + // we expand lets exponentially since there is no let binding in Boogie surface syntax + bool expand_lets = true; + var binds = e.Arguments[0]; + var vcbinds = new List(); + var bound_copy = new Dictionary(bound); + for(int i = 0; i < binds.Arguments.Count(); i++){ + var bind = binds.Arguments[i]; + var symb = bind.Name; + var def = bind.Arguments[0]; + var vce = SExprToVCExpr(def, bound); + var vcv = gen.Variable(symb,vce.Type); + var vcb = gen.LetBinding(vcv,vce); + vcbinds.Add (vcb); + bound[symb] = expand_lets ? vce : vcv; + } + var body = g(1); + if(!expand_lets) + body = gen.Let(vcbinds,body); + bound = bound_copy; + return body; + } + + default: { + var op = VCStringToVCOp (e.Name); + if (op == null) { + var name = StripCruft(e.Name); + if(declHandler.func_map.ContainsKey(name)){ + Function f = declHandler.func_map[name]; + return gen.Function (f, ga()); + } + HandleProverError ("Prover error: unknown operator:" + e.Name); + throw new BadExprFromProver (); + } + if(op.Arity == 2) + return MakeBinary (op, ga ()); + return gen.Function(op, ga()); + } + } + } + + private void SExprToSoln (SExpr resp, + Dictionary> varSubst) + { + Dictionary pmap = new Dictionary (); + + foreach (var node in rpfp.nodes) + pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node); + + var lines = resp.Arguments; + + // get all the predicate definitions + for (int i = 0; i < lines.Length; i++) { + var line = lines [i]; + string pname; + RPFP.Transformer annot; + GetDefun(line, out pname, out annot); + + if(pmap.ContainsKey(pname)){ + var node = pmap[pname]; + node.Annotation = annot; + } + else if(pname[0] != '@'){ // if not an internal symbol + HandleProverError ("Prover error: got unknown predicate:" + pname); + throw new BadExprFromProver (); + } + } + + } + + private void GetDefun(SExpr line, out string pname, out RPFP.Transformer annot) + { + if (line.Name != "define-fun") + { + HandleProverError("Prover error: expected define-fun but got:" + line.Name); + throw new BadExprFromProver(); + } + if (line.ArgCount != 4) + { + HandleProverError("Prover error: define-fun has wrong number of arguments"); + throw new BadExprFromProver(); + } + pname = StripCruft(line.Arguments[0].Name); + var pvars = line.Arguments[1]; + var pbody = line.Arguments[3]; // range has to be Bool + var binding = new Dictionary(); + var pvs = new List(); + foreach (var b in pvars.Arguments) + { + var e = SExprToVar(b); + pvs.Add(e); + binding.Add(StripCruft(b.Name), e); + } + VCExpr bexpr = SExprToVCExpr(pbody, binding); + + annot = rpfp.CreateRelation(pvs.ToArray(), bexpr); + } + + private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, + Dictionary> varSubst) + { + Dictionary nmap = new Dictionary(); + Dictionary pmap = new Dictionary(); + + foreach(var node in rpfp.nodes) + pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name,node); + + RPFP.Node topnode = null; + var lines = resp.Arguments; + + // last line of derivation is from query, skip it + for (int i = 0; i < lines.Length-1; i++) + { + var line = lines[i]; + if (line.ArgCount != 6) + { + HandleProverError("bad derivation line from prover: " + line.ToString()); + return null; + } + var name = line[0]; + var conseq = line[1]; + var rule = line[2]; + var subst = line[3]; + var labs = line[4]; + var refs = line[5]; + var predName = conseq.Name; + { + string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it! + int pos = predName.LastIndexOf(spacer); + if (pos >= 0) + predName = predName.Substring(0, pos); + } + RPFP.Node node = null; + if (!pmap.TryGetValue(predName, out node)) + { + HandleProverError("unknown predicate from prover: " + predName.ToString()); + return null; + } + RPFP.Node cexnode = rpfp.CloneNode(node); + cexnode.map = node; + nmap.Add(name.Name, cexnode); + List Chs = new List(); + + if (refs.Name != "ref") + { + HandleProverError("bad references from prover: " + refs.ToString()); + return null; + } + foreach (var c in refs.Arguments) + { + if (c.Name == "true") + Chs.Add(null); + else + { + RPFP.Node ch = null; + if (!nmap.TryGetValue(c.Name, out ch)) + { + HandleProverError("unknown reference from prover: " + c.ToString()); + return null; + } + Chs.Add(ch); + } + } + + if (!rule.Name.StartsWith("rule!")) + { + HandleProverError("bad rule name from prover: " + refs.ToString()); + return null; + } + int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1; + if (ruleNum < 0 || ruleNum > rpfp.edges.Count) + { + HandleProverError("bad rule name from prover: " + refs.ToString()); + return null; + } + RPFP.Edge orig_edge = rpfp.edges[ruleNum]; + RPFP.Edge e = rpfp.CreateEdge(cexnode, orig_edge.F, Chs.ToArray()); + e.map = orig_edge; + topnode = cexnode; + + if (labs.Name != "labels") + { + HandleProverError("bad labels from prover: " + labs.ToString()); + return null; + } + e.labels = new HashSet(); + foreach (var l in labs.Arguments) + e.labels.Add(l.Name); + + if (subst.Name != "subst") + { + HandleProverError("bad subst from prover: " + subst.ToString()); + return null; + } + Dictionary dict = new Dictionary(); + varSubst[e.number] = dict; + foreach (var s in subst.Arguments) + { + if (s.Name != "=" || s.Arguments.Length != 2) + { + HandleProverError("bad equation from prover: " + s.ToString()); + return null; + } + string uniqueName = s.Arguments[0].Name; + string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it! + int pos = uniqueName.LastIndexOf(spacer); + if (pos >= 0) + uniqueName = uniqueName.Substring(0, pos); + dict.Add(uniqueName, s.Arguments[1].ToString()); + } + + } + if (topnode == null) + { + HandleProverError("empty derivation from prover: " + resp.ToString()); + } + return topnode; + } + + private Model SExprToModel(SExpr resp, ErrorHandler handler) + { + // Concatenate all the arguments + string modelString = resp[0].Name; + // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")" + var models = Model.ParseModels(new StringReader("Error model: \n" + modelString)); + if (models == null || models.Count == 0) + { + HandleProverError("no model from prover: " + resp.ToString()); + } + return models[0]; + } + + private string QuantifiedVCExpr2String(VCExpr x) + { + return VCExpr2String(x, 1); +#if false + if (!(x is VCExprQuantifier)) + return VCExpr2String(x, 1); + VCExprQuantifier node = (x as VCExprQuantifier); + if(node.BoundVars.Count == 0) + return VCExpr2String(x, 1); + + StringWriter wr = new StringWriter(); + + string kind = node.Quan == Quantifier.ALL ? "forall" : "exists"; + wr.Write("({0} (", kind); + + for (int i = 0; i < node.BoundVars.Count; i++) + { + VCExprVar var = node.BoundVars[i]; + Contract.Assert(var != null); + string printedName = Namer.GetQuotedName(var, var.Name); + Contract.Assert(printedName != null); + wr.Write("({0} {1}) ", printedName, SMTLibExprLineariser.TypeToString(var.Type)); + } + + wr.Write(") "); + wr.Write(VCExpr2String(node.Body, 1)); + wr.Write(")"); + string res = wr.ToString(); + return res; +#endif + } + + public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler, + out RPFP.Node cex, + Dictionary> varSubst, + Dictionary extra_bound) + { + //Contract.Requires(descriptiveName != null); + //Contract.Requires(vc != null); + //Contract.Requires(handler != null); + rpfp = _rpfp; + cex = null; + + + if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen + + if (options.LogFilename != null && currentLogFile == null) + { + currentLogFile = OpenOutputFile(descriptiveName); + currentLogFile.Write(common.ToString()); + } + + PrepareCommon(); + + Push(); + SendThisVC("(fixedpoint-push)"); + foreach (var node in rpfp.nodes) + { + DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func); + } + + LineariserOptions.Default.LabelsBelowQuantifiers = true; + List ruleStrings = new List(); + var recursion_bound = CommandLineOptions.Clo.RecursionBound; + foreach (var edge in rpfp.edges) + { + string node_name = (edge.Parent.Name as VCExprBoogieFunctionOp).Func.Name; + string rule_name = "rule_" + edge.number.ToString(); + string rec_bound = ""; + if(extra_bound != null && extra_bound.ContainsKey(node_name)) + rec_bound = (recursion_bound + extra_bound[node_name]).ToString(); + string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + " " + rule_name + " " + rec_bound + "\n)"; + ruleStrings.Add(ruleString); + } + string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n :engine duality\n :print-certificate true\n"; + +#if true + if (CommandLineOptions.Clo.StratifiedInlining != 0) + queryString += " :stratified-inlining true\n"; + if (CommandLineOptions.Clo.RecursionBound > 0) + queryString += " :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n"; +#endif + queryString += ")"; + LineariserOptions.Default.LabelsBelowQuantifiers = false; + FlushAxioms(); + + PossiblyRestart(); + + SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + foreach(var rs in ruleStrings) + SendThisVC(rs); + FlushLogFile(); + + if (Process != null) + { + Process.PingPong(); // flush any errors + +#if false + // TODO: this is not going to work + if (Process.Inspector != null) + Process.Inspector.NewProblem(descriptiveName, vc, handler); +#endif + } + + SendThisVC(queryString); + FlushLogFile(); + + var result = Outcome.Undetermined; + + if (Process != null) + { + + var resp = Process.GetProverResponse(); + + if (proverErrors.Count > 0) + { + result = Outcome.Undetermined; + foreach (var err in proverErrors) + { + if (err.Contains("canceled")) + { + result = Outcome.TimeOut; + } + } + } + else if(resp == null) + HandleProverError("Prover did not respond"); + else switch (resp.Name) + { + case "unsat": + result = Outcome.Valid; + break; + case "sat": + result = Outcome.Invalid; + break; + case "unknown": + result = Outcome.Invalid; + break; + case "bounded": + result = Outcome.Bounded; + break; + case "error": + if (resp.ArgCount > 0 && resp.Arguments[0].Name.Contains("canceled")) + { + result = Outcome.TimeOut; + } + else + { + HandleProverError("Prover error: " + resp.Arguments[0]); + result = Outcome.Undetermined; + } + break; + default: + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + + switch (result) + { + case Outcome.Invalid: + { + resp = Process.GetProverResponse(); + if (resp.Name == "derivation") + { + cex = SExprToCex(resp, handler,varSubst); + } + else + HandleProverError("Unexpected prover response: " + resp.ToString()); + resp = Process.GetProverResponse(); + if (resp.Name == "model") + { + var model = SExprToModel(resp, handler); + cex.owner.SetBackgroundModel(model); + } + else + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + case Outcome.Valid: + case Outcome.Bounded: + { + resp = Process.GetProverResponse(); + if (resp.Name == "fixedpoint") + { + // only get the response if we need it + if(CommandLineOptions.Clo.PrintFixedPoint != null) + SExprToSoln(resp, varSubst); + } + else + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + default: + break; + } + +#if false + while (true) + { + resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + HandleProverError("Unexpected prover response: " + resp.ToString()); + } +#endif + } + SendThisVC("(fixedpoint-pop)"); + Pop(); + AxiomsAreSetup = false; + + if (CommandLineOptions.Clo.PrintConjectures != null) + { + ReadConjectures(CommandLineOptions.Clo.PrintConjectures); + } + + return result; + } + + class MyFileParser : SExpr.Parser + { + SMTLibProcessTheoremProver parent; + + public MyFileParser(System.IO.StreamReader _sr, SMTLibProcessTheoremProver _parent) + : base(_sr) + { + parent = _parent; + } + public override void ParseError(string msg) + { + parent.HandleProverError("Error in conjecture file from prover: " + msg); + } + } + + void ReadConjectures(string filename) + { + try + { + System.IO.StreamReader sr = new StreamReader(filename + ".tmp"); + SExpr.Parser p = new MyFileParser(sr, this); + var sexps = p.ParseSExprs(false); + Dictionary pmap = GetNodeMap(); + foreach (var e in sexps) + { + string pname; + RPFP.Transformer annot; + GetDefun(e, out pname, out annot); + + if (pmap.ContainsKey(pname)) + { + var c = new RPFP.Conjecture(); + c.node = pmap[pname]; + c.bound = annot; + rpfp.conjectures.Add(c); + } + else if (pname[0] != '@') + { // if not an internal symbol + HandleProverError("Prover error: got unknown predicate:" + pname); + throw new BadExprFromProver(); + } + } + sr.Close(); + } + catch (Exception) + { + HandleProverError("No conjecture file from prover"); + throw new BadExprFromProver(); + } + } + + private Dictionary GetNodeMap() + { + Dictionary pmap = new Dictionary(); + foreach (var node in rpfp.nodes) + pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name, node); + return pmap; + } + + private static HashSet usedLogNames = new HashSet(); + + private TextWriter OpenOutputFile(string descriptiveName) + { + Contract.Requires(descriptiveName != null); + Contract.Ensures(Contract.Result() != null); + + string filename = options.LogFilename; + filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename)); + var curFilename = filename; + + lock (usedLogNames) { + int n = 1; + while (usedLogNames.Contains(curFilename)) { + curFilename = filename + "." + n++; + } + usedLogNames.Add(curFilename); + } + + return new StreamWriter(curFilename, false); + } + + private void FlushProverWarnings() + { + var handler = currentErrorHandler; + if (handler != null) { + lock (proverWarnings) { + proverWarnings.Iter(handler.OnProverWarning); + proverWarnings.Clear(); + } + } + } + + protected void HandleProverError(string s) + { + s = s.Replace("\r", ""); + lock (proverWarnings) { + while (s.StartsWith("WARNING: ")) { + var idx = s.IndexOf('\n'); + var warn = s; + if (idx > 0) { + warn = s.Substring(0, idx); + s = s.Substring(idx + 1); + } else { + s = ""; + } + warn = warn.Substring(9); + proverWarnings.Add(warn); + } + } + + FlushProverWarnings(); + + if (s == "") return; + + lock (proverErrors) { + proverErrors.Add(s); + Console.WriteLine("Prover error: " + s); + } + } + + [NoDefaultContract] + public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) + { + Contract.EnsuresOnThrow(true); + + var result = CheckOutcomeCore(handler, taskID: taskID); + SendThisVC("(pop 1)"); + FlushLogFile(); + + return result; + } + + [NoDefaultContract] + public override Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1) + { + Contract.EnsuresOnThrow(true); + + var result = Outcome.Undetermined; + + if (Process == null) + return result; + + try { + currentErrorHandler = handler; + FlushProverWarnings(); + + int errorLimit; + if (CommandLineOptions.Clo.ConcurrentHoudini) { + Contract.Assert(taskID >= 0); + errorLimit = CommandLineOptions.Clo.Cho[taskID].ProverCCLimit; + } else { + errorLimit = CommandLineOptions.Clo.ProverCCLimit; + } + + if (errorLimit < 1) + errorLimit = 1; + + int errorsLeft = errorLimit; + + var globalResult = Outcome.Undetermined; + + while (true) { + string[] labels = null; + bool popLater = false; + + try { + errorsLeft--; + + result = GetResponse(); + + var reporter = handler as VC.VCGen.ErrorReporter; + // TODO(wuestholz): Is the reporter ever null? + if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count) + { + if (usingUnsatCore) + { + UsedNamedAssumes = new HashSet(); + SendThisVC("(get-unsat-core)"); + var resp = Process.GetProverResponse(); + if (resp.Name != "") + { + UsedNamedAssumes.Add(resp.Name); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length)); + } + } + foreach (var arg in resp.Arguments) + { + UsedNamedAssumes.Add(arg.Name); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length)); + } + } + } + else + { + UsedNamedAssumes = null; + } + } + + if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut) + { + #region Run timeout diagnostics + + if (CommandLineOptions.Clo.TraceDiagnosticsOnTimeout) + { + Console.Out.WriteLine("Starting timeout diagnostics with initial time limit {0}.", options.TimeLimit); + } + + SendThisVC("; begin timeout diagnostics"); + + var start = DateTime.UtcNow; + var unverified = new SortedSet(ctx.TimeoutDiagnosticIDToAssertion.Keys); + var timedOut = new SortedSet(); + int frac = 2; + int queries = 0; + int timeLimitPerAssertion = 0 < options.TimeLimit ? (options.TimeLimit / 100) * CommandLineOptions.Clo.TimeLimitPerAssertionInPercent : 1000; + while (true) + { + int rem = unverified.Count; + if (rem == 0) + { + if (0 < timedOut.Count) + { + result = CheckSplit(timedOut, ref popLater, options.TimeLimit, timeLimitPerAssertion, ref queries); + if (result == Outcome.Valid) + { + timedOut.Clear(); + } + else if (result == Outcome.TimeOut) + { + // Give up and report which assertions were not verified. + var cmds = timedOut.Select(id => ctx.TimeoutDiagnosticIDToAssertion[id]); + + if (cmds.Any()) + { + handler.OnResourceExceeded("timeout after running diagnostics", cmds); + } + } + } + else + { + result = Outcome.Valid; + } + break; + } + + // TODO(wuestholz): Try out different ways for splitting up the work (e.g., randomly). + var cnt = Math.Max(1, rem / frac); + // It seems like assertions later in the control flow have smaller indexes. + var split = new SortedSet(unverified.Where((val, idx) => (rem - idx - 1) < cnt)); + Contract.Assert(0 < split.Count); + var splitRes = CheckSplit(split, ref popLater, timeLimitPerAssertion, timeLimitPerAssertion, ref queries); + if (splitRes == Outcome.Valid) + { + unverified.ExceptWith(split); + frac = 1; + } + else if (splitRes == Outcome.Invalid) + { + result = splitRes; + break; + } + else if (splitRes == Outcome.TimeOut) + { + if (2 <= frac && (4 <= (rem / frac))) + { + frac *= 4; + } + else if (2 <= (rem / frac)) + { + frac *= 2; + } + else + { + timedOut.UnionWith(split); + unverified.ExceptWith(split); + frac = 1; + } + } + else + { + break; + } + } + + unverified.UnionWith(timedOut); + + var end = DateTime.UtcNow; + + SendThisVC("; end timeout diagnostics"); + + if (CommandLineOptions.Clo.TraceDiagnosticsOnTimeout) + { + Console.Out.WriteLine("Terminated timeout diagnostics after {0:F0} ms and {1} prover queries.", end.Subtract(start).TotalMilliseconds, queries); + Console.Out.WriteLine("Outcome: {0}", result); + Console.Out.WriteLine("Unverified assertions: {0} (of {1})", unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count); + + string filename = "unknown"; + var assertion = ctx.TimeoutDiagnosticIDToAssertion.Values.Select(t => t.Item1).FirstOrDefault(a => a.tok != null && a.tok != Token.NoToken && a.tok.filename != null); + if (assertion != null) + { + filename = assertion.tok.filename; + } + File.AppendAllText("timeouts.csv", string.Format(";{0};{1};{2:F0};{3};{4};{5};{6}\n", filename, options.TimeLimit, end.Subtract(start).TotalMilliseconds, queries, result, unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count)); + } + + #endregion + } + + if (globalResult == Outcome.Undetermined) + globalResult = result; + + if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) { + IList xlabels; + if (CommandLineOptions.Clo.UseLabels) { + labels = GetLabelsInfo(); + if (labels == null) + { + xlabels = new string[] { }; + } + else + { + xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); + } + } + else if(CommandLineOptions.Clo.SIBoolControlVC) { + labels = new string[0]; + xlabels = labels; + } else { + labels = CalculatePath(handler.StartingProcId()); + xlabels = labels; + } + Model model = (result == Outcome.TimeOut || result == Outcome.OutOfMemory) ? null : + GetErrorModel(); + handler.OnModel(xlabels, model, result); + } + + if (labels == null || !labels.Any() || errorsLeft == 0) break; + } finally { + if (popLater) + { + SendThisVC("(pop 1)"); + } + } + + if (CommandLineOptions.Clo.UseLabels) { + var negLabels = labels.Where(l => l.StartsWith("@")).ToArray(); + var posLabels = labels.Where(l => !l.StartsWith("@")); + Func lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s)); + if (!options.MultiTraces) + posLabels = Enumerable.Empty(); + var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray(); + string expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); ; + if (!conjuncts.Any()) + { + expr = "false"; + } + SendThisVC("(assert " + expr + ")"); + SendCheckSat(); + } + else { + string source = labels[labels.Length - 2]; + string target = labels[labels.Length - 1]; + SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))"); + SendCheckSat(); + } + } + + FlushLogFile(); + + if (CommandLineOptions.Clo.RestartProverPerVC && Process != null) + Process.NeedsRestart = true; + + return globalResult; + + } finally { + currentErrorHandler = null; + } + } + + private Outcome CheckSplit(SortedSet split, ref bool popLater, int timeLimit, int timeLimitPerAssertion, ref int queries) + { + var tla = timeLimitPerAssertion * split.Count; + + if (popLater) + { + SendThisVC("(pop 1)"); + } + + SendThisVC("(push 1)"); + SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), (0 < tla && tla < timeLimit) ? tla : timeLimit)); + popLater = true; + + SendThisVC(string.Format("; checking split VC with {0} unverified assertions", split.Count)); + var expr = VCExpressionGenerator.True; + foreach (var i in ctx.TimeoutDiagnosticIDToAssertion.Keys) + { + var lit = VCExprGen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, VCExprGen.Integer(Microsoft.Basetypes.BigNum.FromInt(i))); + if (split.Contains(i)) { + lit = VCExprGen.Not(lit); + } + expr = VCExprGen.AndSimp(expr, lit); + } + SendThisVC("(assert " + VCExpr2String(expr, 1) + ")"); + if (options.Solver == SolverKind.Z3) + { + SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)"); + } + FlushLogFile(); + SendCheckSat(); + queries++; + return GetResponse(); + } + + public override string[] CalculatePath(int controlFlowConstant) { + SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))"); + var path = new List(); + while (true) { + var resp = Process.GetProverResponse(); + if (resp == null) break; + if (!(resp.Name == "" && resp.ArgCount == 1)) break; + resp = resp.Arguments[0]; + if (!(resp.Name == "" && resp.ArgCount == 2)) break; + resp = resp.Arguments[1]; + var v = resp.Name; + if (v == "-" && resp.ArgCount == 1) { + v = resp.Arguments[0].Name; + path.Add(v); + break; + } + else if (resp.ArgCount != 0) + break; + path.Add(v); + SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))"); + } + return path.ToArray(); + } + + + private class SMTErrorModelConverter { + private struct SMTDataType { + public string Constructor; + public List Types; + } + + private List ErrorModelTodo; + private SMTLibProcessTheoremProver Parent; + private StringBuilder ErrorModel = new StringBuilder(); + private HashSet TopLevelProcessed = new HashSet(); + private int NumNewArrays = 0; + private Dictionary SortSet = new Dictionary(); + private Dictionary DataTypes = new Dictionary(); + private Dictionary Functions = new Dictionary(); + + public SMTErrorModelConverter(SExpr _ErrorModel, SMTLibProcessTheoremProver _Parent) { + ErrorModelTodo = _ErrorModel.Arguments.ToList();; + Parent = _Parent; + } + + public string Convert() { + ConvertErrorModel(ErrorModel); + return ErrorModel.ToString(); + } + + bool isConstArray(SExpr element, SExpr type) { + if (type.Name != "Array") + return false; + + if (element.Name == "__array_store_all__") // CVC4 1.4 + return true; + else if (element.Name == "" && element[0].Name == "as" && + element[0][0].Name == "const") // CVC4 > 1.4 + return true; + + return false; + } + + SExpr getConstArrayElement(SExpr element) { + if (element.Name == "__array_store_all__") // CVC4 1.4 + return element[1]; + else if (element.Name == "" && element[0].Name == "as" && + element[0][0].Name == "const") // CVC4 > 1.4 + return element[1]; + + Parent.HandleProverError("Unexpected value: " + element); + throw new BadExprFromProver (); + } + + void ConstructComplexValue(SExpr element, SExpr type, StringBuilder m) { + if (type.Name == "Array") { + if (element.Name == "store" || isConstArray(element, type)) { + NumNewArrays++; + m.Append("as-array[k!" + NumNewArrays + ']'); + SExpr[] args = {new SExpr("k!" + NumNewArrays), new SExpr(""), type, element}; + var newElement = new SExpr("define-fun", args); + TopLevelProcessed.Add(newElement); + ErrorModelTodo.Add(newElement); + return; + } + } + + ConstructSimpleValue(element, type, m); + } + + void ConstructSimpleValue(SExpr element, SExpr type, StringBuilder m) { + if (type.Name == "Bool" && element.ArgCount == 0) { + m.Append(element.ToString()); + return; + } + + if (type.Name == "Int") { + if (element.ArgCount == 0) { + m.Append(element.ToString()); + return; + } else if (element.Name == "-" && element.ArgCount == 1) { + m.Append(element.ToString()); + return; + } + } + + if (type.Name == "_" && type.ArgCount == 2 && type[0].Name == "BitVec") { + if (element.Name == "_" && element.ArgCount == 2 && + element[0].Name.StartsWith("bv") && element[0].ArgCount == 0 && + element[1].Name == type.Arguments[1].Name && element[1].ArgCount == 0) { + m.Append(element[0].Name + '[' + element[1].Name + ']'); + return; + } + } + + if (type.Name == "Array") { + while (element.Name == "store") { + ConstructComplexValue(element[1], type[0], m); + m.Append(" -> "); + ConstructComplexValue(element[2], type[1], m); + m.Append("\n "); + if (element[0].Name != "store") { + m.Append("else -> "); + } + element = element[0]; + } + + if (isConstArray(element, type)) { + ConstructComplexValue(getConstArrayElement(element), type[1], m); + return; + } else if (element.Name == "_" && element.ArgCount == 2 && + element[0].Name == "as-array") { + m.Append("as-array[" + element[1].Name + ']'); + return; + } + } + + if (SortSet.ContainsKey(type.Name) && SortSet[type.Name] == 0) { + var prefix = "@uc_T_" + type.Name.Substring(2) + "_"; + if (element.Name.StartsWith(prefix)) { + m.Append(type.Name + "!val!" + element.Name.Substring(prefix.Length)); + return; + } + } + + if (Functions.ContainsKey(element.Name) && + type.Name == Functions[element.Name].Name) { + m.Append(element.Name); + return; + } + + if (DataTypes.ContainsKey(type.Name) && + DataTypes[type.Name].Constructor == element.Name && + element.ArgCount == DataTypes[type.Name].Types.Count) { + m.Append("(" + element.Name); + for (int i = 0; i < element.ArgCount; ++i) { + m.Append(" "); + ConstructComplexValue(element[i], DataTypes[type.Name].Types[i], m); + } + m.Append(")"); + return; + } + + Parent.HandleProverError("Unexpected value: " + element); + throw new BadExprFromProver (); + } + + void ConstructFunctionArguments(SExpr arguments, List argTypes, StringBuilder[] argValues) { + if (arguments.Name == "and") { + ConstructFunctionArguments(arguments[0], argTypes, argValues); + ConstructFunctionArguments(arguments[1], argTypes, argValues); + } else if (arguments.Name == "=" && + (arguments[0].Name.StartsWith("_ufmt_") || arguments[0].Name.StartsWith("x!"))) { + int argNum; + if (arguments[0].Name.StartsWith("_ufmt_")) + argNum = System.Convert.ToInt32(arguments[0].Name.Substring("_uftm_".Length)) - 1; + else /* if (arguments[0].Name.StartsWith("x!")) */ + argNum = System.Convert.ToInt32(arguments[0].Name.Substring("x!".Length)) - 1; + if (argNum < 0 || argNum >= argTypes.Count) { + Parent.HandleProverError("Unexpected function argument: " + arguments[0]); + throw new BadExprFromProver (); + } + if (argValues[argNum] != null) { + Parent.HandleProverError("Function argument defined multiple times: " + arguments[0]); + throw new BadExprFromProver (); + } + argValues[argNum] = new StringBuilder(); + ConstructComplexValue(arguments[1], argTypes[argNum], argValues[argNum]); + } else { + Parent.HandleProverError("Unexpected function argument: " + arguments); + throw new BadExprFromProver (); + } + } + + void ConstructFunctionElements(SExpr element, List argTypes, SExpr outType, StringBuilder m) { + while (element.Name == "ite") { + StringBuilder[] argValues = new StringBuilder[argTypes.Count]; + ConstructFunctionArguments(element[0], argTypes, argValues); + foreach (var s in argValues) + m.Append(s + " "); + m.Append("-> "); + ConstructComplexValue(element[1], outType, m); + m.Append("\n "); + if (element[2].Name != "ite") + m.Append("else -> "); + element = element[2]; + } + + ConstructComplexValue(element, outType, m); + } + + void ConstructFunction(SExpr element, SExpr inType, SExpr outType, StringBuilder m) { + List argTypes = new List(); + + for (int i = 0; i < inType.ArgCount; ++i) { + if (inType[i].Name != "_ufmt_" + (i + 1) && inType[i].Name != "x!" + (i + 1) && + !inType[i].Name.StartsWith("BOUND_VARIABLE_")) { + Parent.HandleProverError("Unexpected function argument: " + inType[i].Name); + throw new BadExprFromProver (); + } + argTypes.Add(inType[i][0]); + } + + ConstructFunctionElements(element, argTypes, outType, m); + } + + void ConstructDefine(SExpr element, StringBuilder m) { + Debug.Assert(element.Name == "define-fun"); + + if (element[1].ArgCount != 0) + TopLevelProcessed.Add(element); + + m.Append(element[0] + " -> "); + if (TopLevelProcessed.Contains(element)) + m.Append("{\n "); + + if (element[1].ArgCount == 0 && element[2].Name == "Array" && !TopLevelProcessed.Contains(element)) { + ConstructComplexValue(element[3], element[2], m); + } else if (element[1].ArgCount == 0) { + ConstructSimpleValue(element[3], element[2], m); + } else { + ConstructFunction(element[3], element[1], element[2], m); + } + + if (TopLevelProcessed.Contains(element)) + m.Append("\n}"); + m.Append("\n"); + } + + void ExtractDataType(SExpr datatypes) { + Debug.Assert(datatypes.Name == "declare-datatypes"); + + if (datatypes[0].Name != "" || datatypes[1].Name != "" || datatypes[1].ArgCount != 1) { + Parent.HandleProverError("Unexpected datatype: " + datatypes); + throw new BadExprFromProver (); + } + + SMTDataType dt = new SMTDataType(); + SExpr typeDef = datatypes[1][0]; + + if (typeDef.ArgCount != 1) { + Parent.HandleProverError("Unexpected datatype: " + datatypes); + throw new BadExprFromProver (); + } + + dt.Constructor = typeDef[0].Name; + dt.Types = new List(); + + for (int i = 0; i < typeDef[0].ArgCount; ++i) { + if (typeDef[0][i].ArgCount != 1) { + Parent.HandleProverError("Unexpected datatype constructor: " + typeDef[0]); + throw new BadExprFromProver (); + } + dt.Types.Add(typeDef[0][i][0]); + } + + DataTypes[typeDef.Name] = dt; + } + + private void ConvertErrorModel(StringBuilder m) { + if (Parent.options.Solver == SolverKind.Z3) { + // Datatype declarations are not returned by Z3, so parse common + // instead. This is not very efficient, but currently not an issue, + // as this not the normal way of interfacing with Z3. + var ms = new MemoryStream(Encoding.ASCII.GetBytes(Parent.common.ToString())); + var sr = new StreamReader(ms); + SExpr.Parser p = new MyFileParser(sr, null); + var sexprs = p.ParseSExprs(false); + foreach (var e in sexprs) { + switch (e.Name) { + case "declare-datatypes": + ExtractDataType(e); + break; + } + } + } + + while (ErrorModelTodo.Count > 0) { + var e = ErrorModelTodo[0]; + ErrorModelTodo.RemoveAt(0); + + switch (e.Name) { + case "define-fun": + ConstructDefine(e, m); + break; + case "declare-sort": + SortSet[e[0].Name] = System.Convert.ToInt32(e[1].Name); + break; + case "declare-datatypes": + ExtractDataType(e); + break; + case "declare-fun": + if (e[1].Name != "" || e[1].ArgCount > 0 || e[2].ArgCount > 0 || + e[2].Name == "Bool" || e[2].Name == "Int") { + Parent.HandleProverError("Unexpected top level model element: " + e.Name); + throw new BadExprFromProver (); + } + Functions[e[0].Name] = e[2]; + break; + case "forall": + // ignore + break; + default: + Parent.HandleProverError("Unexpected top level model element: " + e.Name); + throw new BadExprFromProver (); + } + } + } + } + + private Model GetErrorModel() { + if (!options.ExpectingModel()) + return null; + + SendThisVC("(get-model)"); + Process.Ping(); + Model theModel = null; + while (true) { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + if (theModel != null) + HandleProverError("Expecting only one model but got many"); + + string modelStr = null; + if (resp.Name == "model" && resp.ArgCount >= 1) { + var converter = new SMTErrorModelConverter(resp, this); + modelStr = converter.Convert(); + } + else if (resp.ArgCount == 0 && resp.Name.Contains("->")) { + modelStr = resp.Name; + } + else { + HandleProverError("Unexpected prover response getting model: " + resp.ToString()); + } + + List models = null; + try { + switch (options.Solver) { + case SolverKind.Z3: + case SolverKind.CVC4: + models = Model.ParseModels(new StringReader("Error model: \n" + modelStr)); + break; + default: + Debug.Assert(false); + return null; + } + } + catch (ArgumentException exn) { + HandleProverError("Model parsing error: " + exn.Message); + } + if (models == null) + HandleProverError("Could not parse any models"); + else if (models.Count == 0) + HandleProverError("Could not parse any models"); + else if (models.Count > 1) + HandleProverError("Expecting only one model but got many"); + else + theModel = models[0]; + } + return theModel; + } + + private string[] GetLabelsInfo() + { + SendThisVC("(labels)"); + Process.Ping(); + + string[] res = null; + while (true) { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + if (res != null) + HandleProverError("Expecting only one sequence of labels but got many"); + if (resp.Name == "labels" && resp.ArgCount >= 1) { + res = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray(); + } + else { + HandleProverError("Unexpected prover response getting labels: " + resp.ToString()); + } + } + return res; + } + + private Outcome GetResponse() + { + var result = Outcome.Undetermined; + var wasUnknown = false; + + Process.Ping(); + + while (true) { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + + switch (resp.Name) { + case "unsat": + result = Outcome.Valid; + break; + case "sat": + result = Outcome.Invalid; + break; + case "unknown": + result = Outcome.Invalid; + wasUnknown = true; + break; + case "objectives": + // We ignore this. + break; + default: + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + } + + if (wasUnknown) { + SendThisVC("(get-info :reason-unknown)"); + Process.Ping(); + while (true) { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + + if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") { + switch (resp[0].Name) { + case "memout": + currentErrorHandler.OnResourceExceeded("memory"); + result = Outcome.OutOfMemory; + Process.NeedsRestart = true; + break; + case "timeout": case "canceled": + currentErrorHandler.OnResourceExceeded("timeout"); + result = Outcome.TimeOut; + break; + default: + break; + } + } else { + HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString()); + } + } + + } + + return result; + } + + readonly IList OptimizationRequests = new List(); + + protected string VCExpr2String(VCExpr expr, int polarity) + { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + + lock (gen) + { + DateTime start = DateTime.UtcNow; + //if (CommandLineOptions.Clo.Trace) + // Console.Write("Linearising ... "); + + // handle the types in the VCExpr + TypeEraser eraser; + switch (CommandLineOptions.Clo.TypeEncodingMethod) + { + case CommandLineOptions.TypeEncoding.Arguments: + eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen); + break; + case CommandLineOptions.TypeEncoding.Monomorphic: + eraser = null; + break; + default: + eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen); + break; + } + VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity); + Contract.Assert(exprWithoutTypes != null); + + LetBindingSorter letSorter = new LetBindingSorter(gen); + Contract.Assert(letSorter != null); + VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true); + Contract.Assert(sortedExpr != null); + VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true); + Contract.Assert(sortedAxioms != null); + + DeclCollector.Collect(sortedAxioms); + DeclCollector.Collect(sortedExpr); + FeedTypeDeclsToProver(); + + AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, namedAssumes: NamedAssumes)); + string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, NamedAssumes, OptimizationRequests); + Contract.Assert(res != null); + + if (CommandLineOptions.Clo.Trace) + { + DateTime end = DateTime.UtcNow; + TimeSpan elapsed = end - start; + if (elapsed.TotalSeconds > 0.5) + Console.WriteLine("Linearising [{0} s]", elapsed.TotalSeconds); + } + return res; + } + } + + // the list of all known axioms, where have to be included in each + // verification condition + private readonly List!*/> Axioms = new List(); + private bool AxiomsAreSetup = false; + + + + + // similarly, a list of function/predicate declarations + private readonly List!*/> TypeDecls = new List(); + + protected void AddAxiom(string axiom) + { + Contract.Requires(axiom != null); + Axioms.Add(axiom); + // if (thmProver != null) { + // LogActivity(":assume " + axiom); + // thmProver.AddAxioms(axiom); + // } + } + + protected void AddTypeDecl(string decl) + { + Contract.Requires(decl != null); + TypeDecls.Add(decl); + // if (thmProver != null) { + // LogActivity(decl); + // thmProver.Feed(decl, 0); + // } + } + + //////////////////////////////////////////////////////////////////////////// + + private static string _backgroundPredicates; + + static void InitializeGlobalInformation() + { + Contract.Ensures(_backgroundPredicates != null); + //throws ProverException, System.IO.FileNotFoundException; + if (_backgroundPredicates == null) { + if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) + { + _backgroundPredicates = ""; + } + else + { + _backgroundPredicates = @" +(set-info :category ""industrial"") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)"; + } + } + } + + public override VCExpressionGenerator VCExprGen + { + get { return this.gen; } + } + + //// Push/pop interface + + //List pushedAssertions = new List(); + //int numRealPushes; + public override string VCExpressionToString(VCExpr vc) + { + return VCExpr2String(vc, 1); + } + + public override void PushVCExpression(VCExpr vc) + { + throw new NotImplementedException(); + + } + + public override void Pop() + { + SendThisVC("(pop 1)"); + DeclCollector.Pop(); + } + + public override int NumAxiomsPushed() + { + throw new NotImplementedException(); + //return numRealPushes + pushedAssertions.Count; + } + + private void FlushPushedAssertions() + { + throw new NotImplementedException(); + } + + public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) + { + OptimizationRequests.Clear(); + string assert = "assert"; + if (options.Solver == SolverKind.Z3 && isSoft) { + assert += "-soft"; + } + var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)"; + if (options.Solver == SolverKind.Z3 && isSoft) { + expr += " :weight " + weight; + } + AssertAxioms(); + SendThisVC("(" + assert + " " + expr + ")"); + SendOptimizationRequests(); + } + + public override void DefineMacro(Macro f, VCExpr vc) { + DeclCollector.AddFunction(f); + string printedName = Namer.GetQuotedName(f, f.Name); + var argTypes = f.InParams.Cast().MapConcat(p => DeclCollector.TypeToStringReg(p.TypedIdent.Type), " "); + string decl = "(define-fun " + printedName + " (" + argTypes + ") " + DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VCExpr2String(vc, 1) + ")"; + AssertAxioms(); + SendThisVC(decl); + } + + public override void AssertAxioms() + { + FlushAxioms(); + } + + public override void Check() + { + PrepareCommon(); + SendCheckSat(); + FlushLogFile(); + } + + public void SendCheckSat() + { + UsedNamedAssumes = null; + SendThisVC("(check-sat)"); + } + + public override void SetTimeOut(int ms) + { + if (options.Solver == SolverKind.Z3) { + var name = Z3.SetTimeoutOption(); + var value = ms.ToString(); + options.TimeLimit = ms; + options.SmtOptions.RemoveAll(ov => ov.Option == name); + options.AddSmtOption(name, value); + SendThisVC(string.Format("(set-option :{0} {1})", name, value)); + } + } + + public override object Evaluate(VCExpr expr) + { + string vcString = VCExpr2String(expr, 1); + SendThisVC("(get-value (" + vcString + "))"); + var resp = Process.GetProverResponse(); + if (resp == null) throw new VCExprEvaluationException(); + if (!(resp.Name == "" && resp.ArgCount == 1)) throw new VCExprEvaluationException(); + resp = resp.Arguments[0]; + if (resp.Name == "") + { + // evaluating an expression + if (resp.ArgCount == 2) + resp = resp.Arguments[1]; + else + throw new VCExprEvaluationException(); + } + else + { + // evaluating a variable + if (resp.ArgCount == 1) + resp = resp.Arguments[0]; + else + throw new VCExprEvaluationException(); + } + if (resp.Name == "-" && resp.ArgCount == 1) // negative int + return Microsoft.Basetypes.BigNum.FromString("-" + resp.Arguments[0].Name); + if (resp.Name == "_" && resp.ArgCount == 2 && resp.Arguments[0].Name.StartsWith("bv")) // bitvector + return new BvConst(Microsoft.Basetypes.BigNum.FromString(resp.Arguments[0].Name.Substring("bv".Length)), + int.Parse(resp.Arguments[1].Name)); + if (resp.ArgCount != 0) + throw new VCExprEvaluationException(); + if (expr.Type.Equals(Boogie.Type.Bool)) + return bool.Parse(resp.Name); + else if (expr.Type.Equals(Boogie.Type.Int)) + return Microsoft.Basetypes.BigNum.FromString(resp.Name); + else + return resp.Name; + } + + /// + /// Extra state for ApiChecker (used by stratifiedInlining) + /// + static int nameCounter = 0; + + public override Outcome CheckAssumptions(List assumptions, out List unsatCore, ErrorHandler handler) + { + unsatCore = new List(); + + Push(); + // Name the assumptions + var nameToAssumption = new Dictionary(); + int i = 0; + foreach (var vc in assumptions) + { + var name = "a" + nameCounter.ToString(); + nameCounter++; + nameToAssumption.Add(name, i); + + string vcString = VCExpr2String(vc, 1); + AssertAxioms(); + SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); + i++; + } + Check(); + + var outcome = CheckOutcomeCore(handler); + + if (outcome != Outcome.Valid) { + Pop(); + return outcome; + } + + Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores"); + SendThisVC("(get-unsat-core)"); + var resp = Process.GetProverResponse(); + unsatCore = new List(); + if (resp.Name != "") unsatCore.Add(nameToAssumption[resp.Name]); + foreach (var s in resp.Arguments) unsatCore.Add(nameToAssumption[s.Name]); + + FlushLogFile(); + Pop(); + return outcome; + } + + public override void Push() + { + SendThisVC("(push 1)"); + DeclCollector.Push(); + } + + public override Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, out List unsatisfiedSoftAssumptions, ErrorHandler handler) { + unsatisfiedSoftAssumptions = new List(); + + // First, convert both hard and soft assumptions to SMTLIB strings + List hardAssumptionStrings = new List(); + foreach (var a in hardAssumptions) { + hardAssumptionStrings.Add(VCExpr2String(a, 1)); + } + List currAssumptionStrings = new List(); + foreach (var a in softAssumptions) { + currAssumptionStrings.Add(VCExpr2String(a, 1)); + } + + Push(); + AssertAxioms(); + foreach (var a in hardAssumptionStrings) { + SendThisVC("(assert " + a + ")"); + } + Check(); + Outcome outcome = GetResponse(); + if (outcome != Outcome.Invalid) { + Pop(); + return outcome; + } + + int k = 0; + List relaxVars = new List(); + while (true) { + Push(); + foreach (var a in currAssumptionStrings) { + SendThisVC("(assert " + a + ")"); + } + Check(); + outcome = CheckOutcomeCore(handler); + if (outcome != Outcome.Valid) + break; + Pop(); + string relaxVar = "relax_" + k; + relaxVars.Add(relaxVar); + SendThisVC("(declare-fun " + relaxVar + " () Int)"); + List nextAssumptionStrings = new List(); + for (int i = 0; i < currAssumptionStrings.Count; i++) { + string constraint = "(= " + relaxVar + " " + i + ")"; + nextAssumptionStrings.Add("(or " + currAssumptionStrings[i] + " " + constraint + ")"); + } + currAssumptionStrings = nextAssumptionStrings; + k++; + } + + if (outcome == Outcome.Invalid) { + foreach (var relaxVar in relaxVars) { + SendThisVC("(get-value (" + relaxVar + "))"); + FlushLogFile(); + var resp = Process.GetProverResponse(); + if (resp == null) break; + if (!(resp.Name == "" && resp.ArgCount == 1)) break; + resp = resp.Arguments[0]; + if (!(resp.Name != "" && resp.ArgCount == 1)) break; + resp = resp.Arguments[0]; + if (resp.ArgCount != 0) + break; + int v; + if (int.TryParse(resp.Name, out v)) + unsatisfiedSoftAssumptions.Add(v); + else + break; + } + Pop(); + } + + Pop(); + return outcome; + } + } + + public class SMTLibInterpolatingProcessTheoremProver : SMTLibProcessTheoremProver + { + public SMTLibInterpolatingProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen, + SMTLibProverContext ctx) + : base(AddInterpOption(options), gen, ctx) + { + + } + + private static ProverOptions AddInterpOption(ProverOptions options) + { + var opts = (SMTLibProverOptions)options; + opts.AddSmtOption("produce-interpolants", "true"); + if (CommandLineOptions.Clo.PrintFixedPoint == null) + CommandLineOptions.Clo.PrintFixedPoint = "itp.fixedpoint.bpl"; + return opts; + } + + public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B) + { + string A_str = VCExpr2String(A, 1); + string B_str = VCExpr2String(B, 1); + + AssertAxioms(); + SendThisVC("(compute-interpolant " + A_str + " " + B_str + ")"); + + SExpr interpolant; + Outcome result = GetInterpolantResponse(out interpolant); + + if (result != Outcome.Valid) + return null; + + VCExpr interpolantVC = SExprToVCExpr(interpolant, new Dictionary()); + return interpolantVC; + } + + private Outcome GetInterpolantResponse(out SExpr interpolant) + { + var result = Outcome.Undetermined; + var wasUnknown = false; + interpolant = null; + + Process.Ping(); + bool onlyOnce = false; + + while (true) + { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + + switch (resp.Name) + { + case "unsat": + result = Outcome.Valid; + break; + case "sat": + result = Outcome.Invalid; + break; + case "unknown": + result = Outcome.Invalid; + wasUnknown = true; + break; + default: + if (result == Outcome.Valid) + { + interpolant = resp as SExpr; + + Contract.Assert(onlyOnce == false); + onlyOnce = true; + continue; + } + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + } + + if (wasUnknown) + { + SendThisVC("(get-info :reason-unknown)"); + Process.Ping(); + + while (true) + { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + + if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") + { + switch (resp[0].Name) + { + case "memout": + currentErrorHandler.OnResourceExceeded("memory"); + result = Outcome.OutOfMemory; + Process.NeedsRestart = true; + break; + case "timeout": + case "canceled": + currentErrorHandler.OnResourceExceeded("timeout"); + result = Outcome.TimeOut; + break; + default: + break; + } + } + else + { + HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString()); + } + } + } + + return result; + } + + public override List GetTreeInterpolant(List root, List leaves) + { + List result = new List(); + + string vcStr = "true"; + foreach (string str in root) + vcStr = vcStr + " " + str; + foreach (string str in leaves) + vcStr = vcStr + "\r\n (interp " + str + ")"; + + vcStr = "(get-interpolant (and\r\n" + vcStr + "\r\n))"; + SendThisVC(vcStr); + if(currentLogFile != null) currentLogFile.Flush(); + + List interpolantList; + GetTreeInterpolantResponse(out interpolantList); + + Dictionary bound = new Dictionary(); + foreach (SExpr sexpr in interpolantList) + { + VCExpr interpolantVC = SExprToVCExpr(sexpr, bound); + result.Add(interpolantVC); + } + + return result; + } + + private void GetTreeInterpolantResponse(out List interpolantList) + { + interpolantList = new List(); + + Process.Ping(); + + while (true) + { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + + SExpr interpolant = resp as SExpr; + if(interpolant == null) + HandleProverError("Unexpected prover response: got null for interpolant!"); + interpolantList.Add(interpolant); + } + } + } + + public class SMTLibProverContext : DeclFreeProverContext + { + internal SMTLibProcessTheoremProver parent; + + public readonly Dictionary> KnownDatatypeConstructors = new Dictionary>(); + + public SMTLibProverContext(VCExpressionGenerator gen, + VCGenerationOptions genOptions) + : base(gen, genOptions) + { + } + + protected SMTLibProverContext(SMTLibProverContext par) + : base(par) + { + } + + public override object Clone() + { + return new SMTLibProverContext(this); + } + + public override string Lookup(VCExprVar var) + { + VCExprVar v = parent.AxBuilder.TryTyped2Untyped(var); + if (v != null) { + var = v; + } + return parent.Namer.Lookup(var); + } + + public override void DeclareFunction(Function f, string attributes) { + if (f is DatatypeConstructor) { + CtorType datatype = (CtorType) f.OutParams[0].TypedIdent.Type; + if (!KnownDatatypeConstructors.ContainsKey(datatype)) + KnownDatatypeConstructors[datatype] = new List(); + KnownDatatypeConstructors[datatype].Add(f); + } + base.DeclareFunction(f, attributes); + } + } + + public class Factory : ProverFactory + { + // Set programmatically + public static bool UseInterpolation = false; + + public override object SpawnProver(ProverOptions options, object ctxt) + { + //Contract.Requires(ctxt != null); + //Contract.Requires(options != null); + Contract.Ensures(Contract.Result() != null); + + return this.SpawnProver(options, + cce.NonNull((SMTLibProverContext)ctxt).ExprGen, + cce.NonNull((SMTLibProverContext)ctxt)); + } + + public override object NewProverContext(ProverOptions options) + { + //Contract.Requires(options != null); + Contract.Ensures(Contract.Result() != null); + + VCExpressionGenerator gen = new VCExpressionGenerator(); + List/*!>!*/ proverCommands = new List(); + proverCommands.Add("smtlib"); + var opts = (SMTLibProverOptions)options ; + if (opts.Solver == SolverKind.Z3) + proverCommands.Add("z3"); + else + proverCommands.Add("external"); + VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands); + return new SMTLibProverContext(gen, genOptions); + } + + public override ProverOptions BlankProverOptions() + { + return new SMTLibProverOptions(); + } + + protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options, + VCExpressionGenerator gen, + SMTLibProverContext ctx) + { + Contract.Requires(options != null); + Contract.Requires(gen != null); + Contract.Requires(ctx != null); + Contract.Ensures(Contract.Result() != null); + + if (UseInterpolation) + return new SMTLibInterpolatingProcessTheoremProver(options, gen, ctx); + + return new SMTLibProcessTheoremProver(options, gen, ctx); + } + + public override bool SupportsLabels(ProverOptions options) + { + return ((SMTLibProverOptions)options).SupportsLabels; + } + } +} -- cgit v1.2.3