Merge

4 files changed, 513 insertions, 5 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 03e2ce17..98086cf0 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -593,7 +593,6 @@ namespace Microsoft.Boogie {
     public bool PrintInlined = false;

     public bool ExtractLoops = false;

     public bool DeterministicExtractLoops = false;

-    public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)

     public int StratifiedInlining = 0;

     public string FixedPointEngine = null;

     public int StratifiedInliningOption = 0;

@@ -612,6 +611,10 @@ namespace Microsoft.Boogie {
        Call

     };

     public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure;

+		

+    public string PrintFixedPoint = null;

+		

+    public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)

 

     public enum TypeEncoding {

       None,

@@ -1126,6 +1129,12 @@ namespace Microsoft.Boogie {
               }

           }

           return true;

+        case "printFixedPoint":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              PrintFixedPoint = args[ps.i];

+          }

+          return true;

         case "siVerbose":

           if (ps.ConfirmArgumentCount(1)) {

             StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));

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<string,VCExprVar> var_map = new Dictionary<string, VCExprVar>();

+			public Dictionary<string,Function> func_map = new Dictionary<string, Function>();

+			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<Type>();

+                types.Add(idxType);

+				return gen.Variable (vname, new MapType(Token.NoToken,new List<TypeVariable>(),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<string,VCExpr> 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<VCExprVar>();

+                    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<VCTrigger>(), body);

+                    else

+                        body = gen.Exists(vcbinds, new List<VCTrigger>(), 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<VCExprLetBinding>();

+				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<int,Dictionary<string,string>> varSubst)

+		{

+			Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();

+

+			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<string,VCExpr>();

+				var pvs = new List<VCExpr>();

+				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<int,Dictionary<string,string>> 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<int,Dictionary<string,string>> 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<HashSet<string/*!*/>/*!*/> _KnownStoreFunctions = new Stack<HashSet<string>>();

     private readonly Stack<HashSet<string/*!*/>/*!*/> _KnownSelectFunctions = new Stack<HashSet<string>>();

     private readonly Stack<HashSet<string>> _KnownLBL = new Stack<HashSet<string>>();

-

+		

+	// 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<Function>());

@@ -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);

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 8d9fab15..d50f901b 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -689,6 +689,67 @@ namespace Microsoft.Boogie
                 proc.Ensures.Add(new Ensures(true, freePostExpr));

             }

         }

+		

+		private void FixedPointToSpecs(){

+			

+			if(mode != Mode.Corral || CommandLineOptions.Clo.PrintFixedPoint == null)

+				return; // not implemented for other annotation modes yet

+			

+			var twr = new TokenTextWriter(CommandLineOptions.Clo.PrintFixedPoint);

+			Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();

+

+			foreach (var node in rpfp.nodes)

+				pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);

+			

+			foreach (Declaration decl in program.TopLevelDeclarations)

+            {

+                Contract.Assert(decl != null);

+                Implementation impl = decl as Implementation;

+                if (impl == null)

+                    continue;

+                Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");

+

+                Procedure proc = cce.NonNull(impl.Proc);

+

+                {

+                    StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, boogieContext, QuantifierExpr.GetNextSkolemId());

+                    implName2StratifiedInliningInfo[impl.Name] = info;

+                    // We don't need controlFlowVariable for stratified Inlining

+                    //impl.LocVars.Add(info.controlFlowVariable);

+                    List<Expr> exprs = new List<Expr>();

+

+                    {

+						// last ensures clause will be the symbolic one

+						if(info.isMain)

+							continue;

+						var ens = proc.Ensures[proc.Ensures.Count - 1];

+						if(ens.Condition == Expr.False) // this is main

+							continue;

+                        var postExpr = ens.Condition as NAryExpr;

+						var args = postExpr.Args;

+						if(pmap.ContainsKey (impl.Name)){

+							RPFP.Node node = pmap[impl.Name];

+							var ind = node.Annotation.IndParams;

+							var bound = new Dictionary<VCExpr,Expr>(); 

+							for(int i = 0; i < args.Count; i++){

+								bound[ind[i]] = args[i];

+							}

+							var new_ens_cond = VCExprToExpr(node.Annotation.Formula,bound);

+                            if (new_ens_cond != Expr.True)

+                            {

+                                var new_ens = new Ensures(false, new_ens_cond);

+                                var enslist = new List<Ensures>();

+                                enslist.Add(new_ens);

+                                var new_proc = new Procedure(proc.tok, proc.Name, proc.TypeParameters, proc.InParams,

+                                                             proc.OutParams, new List<Requires>(), new List<IdentifierExpr>(), enslist);

+                                new_proc.Emit(twr, 0);

+                            }

+						}

+                    }

+                }

+            }

+			twr.Close ();

+		}

 

         private Term ExtractSmallerVCsRec(TermDict< Term> memo, Term t, List<Term> small, Term lbl = null)

         {

@@ -1482,6 +1543,7 @@ namespace Microsoft.Boogie
                             return VC.ConditionGeneration.Outcome.Errors;

                         case RPFP.LBool.False:

                             Console.WriteLine("Procedure is correct.");

+							FixedPointToSpecs();

                             return Outcome.Correct;

                         case RPFP.LBool.Undef:

                             Console.WriteLine("Inconclusive result.");

@@ -1964,7 +2026,132 @@ namespace Microsoft.Boogie
                 return m.MkElement(subst[uniqueName]);

             return m.MkFunc("@undefined", 0).GetConstant();

         }

-

+		

+		class InternalError : Exception {

+		}

+		

+		

+		private BinaryOperator.Opcode VCOpToOp (VCExprOp op)

+		{

+			if (op == VCExpressionGenerator.AddIOp)

+				return BinaryOperator.Opcode.Add;

+			if (op == VCExpressionGenerator.SubIOp)

+				return BinaryOperator.Opcode.Sub;

+			if (op == VCExpressionGenerator.MulIOp)

+				return BinaryOperator.Opcode.Mul;

+			if (op == VCExpressionGenerator.DivIOp)

+				return BinaryOperator.Opcode.Div;

+			if (op == VCExpressionGenerator.EqOp)

+				return BinaryOperator.Opcode.Eq;

+			if (op == VCExpressionGenerator.LeOp)

+				return BinaryOperator.Opcode.Le;

+			if (op == VCExpressionGenerator.LtOp)

+				return BinaryOperator.Opcode.Lt;

+			if (op == VCExpressionGenerator.GeOp)

+				return BinaryOperator.Opcode.Ge;

+			if (op == VCExpressionGenerator.GtOp)

+				return BinaryOperator.Opcode.Gt;

+			if (op == VCExpressionGenerator.AndOp)

+				return BinaryOperator.Opcode.And;

+			if (op == VCExpressionGenerator.OrOp)

+				return BinaryOperator.Opcode.Or;

+			throw new InternalError();

+		}

+		

+		private Expr MakeBinary (BinaryOperator.Opcode op, List<Expr> args)

+		{

+			if(args.Count == 0){

+				// with zero args we need the identity of the op

+				switch(op){

+					case BinaryOperator.Opcode.And:

+					    return Expr.True;

+					case BinaryOperator.Opcode.Or:

+					    return Expr.False;

+				    case BinaryOperator.Opcode.Add:

+						return new LiteralExpr(Token.NoToken,Microsoft.Basetypes.BigNum.ZERO);

+				default:

+					throw new InternalError();

+				}

+			}

+			var temp = args[0];

+			for(int i = 1; i < args.Count; i++)

+				temp = Expr.Binary(Token.NoToken,op,temp,args[i]);

+			return temp;		

+		}

+		

+		private Variable MakeVar(VCExprVar v){

+			var foo = new TypedIdent(Token.NoToken,v.Name.ToString(),v.Type);

+			return new BoundVariable(Token.NoToken,foo);

+		}

+		

+		private Expr VCExprToExpr (VCExpr e, Dictionary<VCExpr,Expr> bound)

+		{

+			if (e is VCExprVar) {

+				if(bound.ContainsKey(e))

+					return bound[e];

+                return Expr.Ident(MakeVar(e as VCExprVar)); // TODO: this isn't right

+			}

+			if (e is VCExprIntLit) {

+				var n = e as VCExprIntLit;

+				return new LiteralExpr(Token.NoToken,n.Val);

+			}

+			if (e is VCExprNAry) {

+				var f = e as VCExprNAry;

+				var args = new List<Expr>();

+				for(int i = 0; i < f.Arity; i++){

+					args.Add (VCExprToExpr (f[i],bound));

+				}

+				

+				if(f.Op == VCExpressionGenerator.NotOp)

+					return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, args[0]);

+

+				if(f.Op == VCExpressionGenerator.IfThenElseOp)

+					return new NAryExpr(Token.NoToken,new IfThenElse(Token.NoToken),args);

+					

+				if(f.Op is VCExprSelectOp){

+					var idx = new List<Expr>();

+					idx.Add(args[1]);

+				    return Expr.Select(args[0],idx);

+				}

+				

+				if(f.Op is VCExprStoreOp){

+					var idx = new List<Expr>();

+					idx.Add(args[1]);

+					return Expr.Store(args[0],idx,args[2]);

+				}

+				

+				var op = VCOpToOp (f.Op);

+				return MakeBinary(op,args);

+			}

+			

+			if(e is VCExprQuantifier) {

+				var f = e as VCExprQuantifier;

+				var vs = new List<Variable>();

+				var new_bound = new Dictionary<VCExpr,Expr>(bound);

+				foreach(var v in f.BoundVars){

+					var ve = MakeVar(v);

+					vs.Add(ve);

+					new_bound.Add (v,Expr.Ident (ve));

+				}

+				var bd = VCExprToExpr(f.Body,new_bound);

+				if(f.Quan == Quantifier.EX)

+					return new ExistsExpr(Token.NoToken,vs,bd);

+				else

+					return new ForallExpr(Token.NoToken,vs,bd);	

+			}

+			if (e == VCExpressionGenerator.True) {

+				return Expr.True;

+			}

+			if (e == VCExpressionGenerator.False) {

+				return Expr.False;

+			}

+			if (e is VCExprLet) {

+				

+			}

+			

+			throw new InternalError();

+		}

+		

 

     }