fixup! Add support for function definitions

Source/Core/Absy.cs

@@ -1527,7 +1527,7 @@ public override void Emit(TokenTextWriter stream, int level) {
 
  public class Axiom : Declaration {
  private Expr/*!*/ expression;
- public bool isFunctionDefinition;
+ public bool IsFunctionDefinition;
 
  public Expr Expr {
  get {
@@ -1558,7 +1558,7 @@ public Axiom(IToken/*!*/ tok, Expr/*!*/ expr, string comment)
  Contract.Requires(tok != null);
  Contract.Requires(expr != null);
  this.expression = expr;
- this.isFunctionDefinition = false;
+ this.IsFunctionDefinition = false;
  Comment = comment;
  }
 
@@ -2840,7 +2840,7 @@ public override Absy StdDispatch(StandardVisitor visitor) {
  return visitor.VisitFunction(this);
  }
 
- public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null, bool isFuncDef=false) {
+ public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null, bool isFuncDef = false) {
  Contract.Requires(definition != null);
 
  List<Variable> dummies = new List<Variable>();

Source/Core/AbsyQuant.cs

@@ -593,30 +593,30 @@ public override int GetHashCode() {
 
  public class ForallExpr : QuantifierExpr {
  public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,
- List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false, bool isFuncDef=false)
+ List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable = false, bool isFuncDef=false)
  : base(tok, typeParams, dummies, kv, triggers, body, immutable, isFuncDef) {
  Contract.Requires(tok != null);
  Contract.Requires(typeParams != null);
  Contract.Requires(dummies != null);
  Contract.Requires(body != null);
  Contract.Requires(dummies.Count + typeParams.Count > 0);
  }
- public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false, bool isFuncDef=false)
- : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable, isFuncDef) {
+ public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable = false)
+ : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
  Contract.Requires(tok != null);
  Contract.Requires(dummies.Count > 0);
  }
- public ForallExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false, bool isFuncDef=false)
- : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable, isFuncDef) {
+ public ForallExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable = false)
+ : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
  Contract.Requires(tok != null);
  Contract.Requires(dummies.Count > 0);
  }
- public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body, bool immutable=false, bool isFuncDef=false)
- : base(tok, typeParams, dummies, null, null, body, immutable, isFuncDef) {
+ public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body, bool immutable = false)
+ : base(tok, typeParams, dummies, null, null, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
  Contract.Requires(typeParams != null);
@@ -639,15 +639,15 @@ public override BinderKind Kind {
 
  public class ExistsExpr : QuantifierExpr {
  public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ dummies,
- QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)
+ QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable = false)
  : base(tok, typeParams, dummies, kv, triggers, body, immutable) {
  Contract.Requires(tok != null);
  Contract.Requires(typeParams != null);
  Contract.Requires(dummies != null);
  Contract.Requires(body != null);
  Contract.Requires(dummies.Count + typeParams.Count > 0);
  }
- public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)
+ public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable = false)
  : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);

Source/Provers/SMTLib/ProverInterface.cs

@@ -33,14 +33,12 @@ protected override bool StandardResult(VCExpr node, bool arg) {
  }
 
  public List<Function> Collect(VCExpr expr) {
- Contract.Requires(expr != null);
  functionList = new List<Function>();
  Traverse(expr, true);
  return functionList;
  }
 
  public override bool Visit(VCExprNAry node, bool arg) {
- Contract.Requires(node != null);
  VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
  if (op != null) {
  functionList.Add(op.Func);
@@ -251,7 +249,7 @@ private void FindDependentTypes(Type type, List<CtorType> dependentTypes)
  }
  }
 
- protected Function IsFunctionDef(VCExpr expr)
+ protected Function AsFunctionDef(VCExpr expr)
  {
  // If this expr is a function definition, return the function object.
  var quan = expr as VCExprQuantifier;
@@ -362,21 +360,23 @@ private void PrepareCommon()
  SendCommon("(declare-datatypes (" + datatypesString + ") (" + datatypeConstructorsString + "))");
  }
  }
- if (CommandLineOptions.Clo.ProverPreamble != null)
- SendCommon("(include \"" + CommandLineOptions.Clo.ProverPreamble + "\")");
+ if (CommandLineOptions.Clo.ProverPreamble != null) {
+ SendCommon("(include \"" + CommandLineOptions.Clo.ProverPreamble + "\")");
+ }
  }
 
  if (!AxiomsAreSetup)
  {
  var axioms = ctx.Axioms;
  var nary = axioms as VCExprNAry;
  List<VCExpr> axiomList = new List<VCExpr>();
- if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
+ if (nary != null && nary.Op == VCExpressionGenerator.AndOp) {
  foreach (var expr in nary.UniformArguments) {
  axiomList.Add(expr);
  }
- else
+ } else {
  axiomList.Add(axioms);
+ }
 
  // Separate function definitions from other axioms. Function definitions must be processed
  // first; otherwise, processing an axiom that uses the function definition can create a declaration
@@ -385,7 +385,7 @@ private void PrepareCommon()
  Stack<Function> functionDefs = new Stack<Function>();
  Stack<VCExpr> otherAxioms = new Stack<VCExpr>();
  for (int i = axiomList.Count-1; i >= 0; i--) {
- Function f = IsFunctionDef(axiomList[i]);
+ Function f = AsFunctionDef(axiomList[i]);
  if (f != null) {
  // Add as a known function to DeclCollector so that it's not declared later.
  DeclCollector.AddFunction(f);
@@ -441,8 +441,9 @@ private void PrepareCommon()
  while (otherAxioms.Count > 0) {
  VCExpr expr = otherAxioms.Pop();
  var str = VCExpr2String(expr, -1);
- if (str != "true")
+ if (str != "true") {
  AddAxiom(str);
+ }
  }
  AxiomsAreSetup = true;
  CachedAxBuilder = AxBuilder;
@@ -470,10 +471,11 @@ private void FlushAxioms()
  TypeDecls.Clear();
  foreach (string s in Axioms) {
  Contract.Assert(s != null);
- if (s.StartsWith("(define-fun"))
+ if (s.StartsWith("(define-fun")) {
  SendCommon(s);
- else if (s != "true")
+ } else if (s != "true") {
  SendCommon("(assert " + s + ")");
+ }
  }
  Axioms.Clear();
  //FlushPushedAssertions();

Source/Provers/SMTLib/SMTLibLineariser.cs

@@ -333,15 +333,15 @@ public bool Visit(VCExprQuantifier node, LineariserOptions options)
 
  VCQuantifierInfos infos = node.Infos;
  if (infos.isFunctionDefinition) {
-  wr.Write("(define-fun ");
-  var naryExpr = node.Body as VCExprNAry;
-  Contract.Assert(naryExpr != null);
-  var funCall = naryExpr[0] as VCExprNAry;
-  Contract.Assert(funCall != null);
-  VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)funCall.Op;
+  wr.Write("(define-fun ");
+  var naryExpr = node.Body as VCExprNAry;
+  Contract.Assert(naryExpr != null);
+  var funCall = naryExpr[0] as VCExprNAry;
+  Contract.Assert(funCall != null);
+  VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)funCall.Op;
  Contract.Assert(op != null);
  wr.Write(Namer.GetQuotedName(op.Func, op.Func.Name));
-  wr.Write(" (");
+  wr.Write(" (");
  } else {
  string kind = node.Quan == Quantifier.ALL ? "forall" : "exists";
  wr.Write("({0} (", kind);
@@ -357,14 +357,14 @@ public bool Visit(VCExprQuantifier node, LineariserOptions options)
 
  wr.Write(") ");
 
- if (infos.isFunctionDefinition) {
-  var naryExpr = node.Body as VCExprNAry;
-  Contract.Assert(naryExpr != null);
-  wr.Write(" {0} ", TypeToString(naryExpr[0].Type));
+ if (infos.isFunctionDefinition) {
+  var naryExpr = node.Body as VCExprNAry;
+  Contract.Assert(naryExpr != null);
+  wr.Write(" {0} ", TypeToString(naryExpr[0].Type));
  Linearise(naryExpr[1], options);
  wr.Write(")");
-  return true;
- }
+  return true;
+ }
 
  var weight = QKeyValue.FindIntAttribute(infos.attributes, "weight", 1);
  if (!ProverOptions.UseWeights)

Source/VCExpr/Boogie2VCExpr.cs

@@ -1,4 +1,4 @@
-1//-----------------------------------------------------------------------------
+//-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation. All Rights Reserved.
 //

Source/VCExpr/VCExprAST.cs

@@ -663,13 +663,13 @@ public VCExpr Exists(List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*
  Contract.Ensures(Contract.Result<VCExpr>() != null);
  return Quantify(Quantifier.EX, typeParams, vars, triggers, infos, body);
  }
- public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body, bool isFuncDef = false) {
+ public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {
  Contract.Requires(body != null);
  Contract.Requires(cce.NonNullElements(triggers));
  Contract.Requires(cce.NonNullElements(vars));
  Contract.Ensures(Contract.Result<VCExpr>() != null);
  return Quantify(Quantifier.EX, new List<TypeVariable/*!*/>(), vars,
- triggers, new VCQuantifierInfos(null, -1, false, isFuncDef, null), body);
+ triggers, new VCQuantifierInfos(null, -1, false, false, null), body);
  }
  public VCExpr Exists(VCExprVar var, VCTrigger trigger, VCExpr body) {
  Contract.Requires(body != null);

Source/VCGeneration/Context.cs

@@ -180,6 +180,7 @@ public override object Clone() {
 
  public override void AddAxiom(Axiom ax, string attributes) {//Contract.Requires(ax != null);
  base.AddAxiom(ax, attributes);
+
  axiomConjuncts.Add(translator.Translate(ax.Expr));
  }
 

Test/functiondefine/fundef.bpl

@@ -8,8 +8,8 @@ function {:define} foo2(x:int) returns(int)
  { x + 1 }
 
 procedure test(x:int) returns (r:int)
-requires x > 0;
-ensures r > 0;
+ requires x > 0;
+ ensures r > 0;
 {
  if (foo(x)) {
  r := foo2(x);