From 37817c9f009f54b7203a0c0c132f9966b3b91bc8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 14 Apr 2014 14:43:29 -0700 Subject: Added /printFixedPoint option --- Source/Provers/SMTLib/ProverInterface.cs | 300 ++++++++++++++++++++++++++++- Source/Provers/SMTLib/TypeDeclCollector.cs | 18 +- 2 files changed, 315 insertions(+), 3 deletions(-) (limited to 'Source/Provers/SMTLib') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 05bcdb01..4e895931 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -434,7 +434,283 @@ namespace Microsoft.Boogie.SMTLib 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; + } + + private 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]; + 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 (); + } + var 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 (b.Name,e); + } + VCExpr bexpr = SExprToVCExpr(pbody,binding); + + var annot = rpfp.CreateRelation(pvs.ToArray(),bexpr); + + 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 RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, Dictionary> varSubst) { @@ -600,7 +876,7 @@ namespace Microsoft.Boogie.SMTLib return res; #endif } - + public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler, out RPFP.Node cex, Dictionary> varSubst) @@ -610,7 +886,12 @@ namespace Microsoft.Boogie.SMTLib //Contract.Requires(handler != null); rpfp = _rpfp; cex = null; - + + if(CommandLineOptions.Clo.PrintFixedPoint != null){ + declHandler = new MyDeclHandler(); + DeclCollector.SetDeclHandler(declHandler); + } + if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen if (options.LogFilename != null && currentLogFile == null) @@ -736,6 +1017,19 @@ namespace Microsoft.Boogie.SMTLib 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; } @@ -753,6 +1047,8 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(fixedpoint-pop)"); Pop(); AxiomsAreSetup = false; + DeclCollector.SetDeclHandler(null); + declHandler = null; // just so we can GC it return result; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 2bf8fa22..30363102 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -90,7 +90,19 @@ void ObjectInvariant() private readonly Stack/*!*/> _KnownStoreFunctions = new Stack>(); private readonly Stack/*!*/> _KnownSelectFunctions = new Stack>(); private readonly Stack> _KnownLBL = new Stack>(); - + + // lets RPFP checker capture decls + public abstract class DeclHandler { + public abstract void VarDecl(VCExprVar v); + public abstract void FuncDecl(Function f); + } + + private DeclHandler declHandler = null; + + public void SetDeclHandler(DeclHandler _d){ + declHandler = _d; + } + private void InitializeKnownDecls() { _KnownFunctions.Push(new HashSet()); @@ -182,6 +194,8 @@ void ObjectInvariant() if (KnownFunctions.Contains(func)) return; KnownFunctions.Add(func); + if(declHandler != null) + declHandler.FuncDecl(func); } public void RegisterRelation(Function func) @@ -242,6 +256,8 @@ void ObjectInvariant() "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; AddDeclaration(decl); KnownVariables.Add(node); + if(declHandler != null) + declHandler.VarDecl(node); } return base.Visit(node, arg); -- cgit v1.2.3