Merge pull request #236 from zvonimir/define-func

Refactored the define attribute on functions

Source/Core/Absy.cs

@@ -2671,8 +2671,8 @@ public override void Emit(TokenTextWriter stream, int level) { }
  public class Function : DeclWithFormals {
  public string Comment;
 
- // the body is only set if the function is declared with {:inline}
- public Expr Body;
+ public Expr Body; // Only set if the function is declared with {:inline}
+ public NAryExpr DefinitionBody; // Only set if the function is declared with {:define}
  public Axiom DefinitionAxiom;
 
  public IList<Axiom> otherDefinitionAxioms;
@@ -2755,25 +2755,41 @@ public override void Emit(TokenTextWriter stream, int level) {
  stream.Write(this, level, "function ");
  EmitAttributes(stream);
  if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline")) {
+ Contract.Assert(DefinitionBody == null);
  // Boogie inlines any function whose .Body field is non-null. The parser populates the .Body field
- // is the :inline attribute is present, but if someone creates the Boogie file directly as an AST, then
+ // if the :inline attribute is present, but if someone creates the Boogie file directly as an AST, then
  // the :inline attribute may not be there. We'll make sure it's printed, so one can see that this means
  // that the body will be inlined.
  stream.Write("{:inline} ");
  }
+ if (DefinitionBody != null && !QKeyValue.FindBoolAttribute(Attributes, "define")) {
+ // Boogie defines any function whose .DefinitionBody field is non-null. The parser populates the .DefinitionBody field
+ // if the :define attribute is present, but if someone creates the Boogie file directly as an AST, then
+ // the :define attribute may not be there. We'll make sure it's printed, so one can see that this means
+ // that the function will be defined.
+ stream.Write("{:define} ");
+ }
  if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
  stream.Write("h{0}^^{1}", this.GetHashCode(), TokenTextWriter.SanitizeIdentifier(this.Name));
  } else {
  stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
  }
  EmitSignature(stream, true);
  if (Body != null) {
+ Contract.Assert(DefinitionBody == null);
  stream.WriteLine();
  stream.WriteLine("{");
  stream.Write(level + 1, "");
  Body.Emit(stream);
  stream.WriteLine();
  stream.WriteLine("}");
+ } else if (DefinitionBody != null) {
+ stream.WriteLine();
+ stream.WriteLine("{");
+ stream.Write(level + 1, "");
+ DefinitionBody.Args[1].Emit(stream);
+ stream.WriteLine();
+ stream.WriteLine("}");
  } else {
  stream.WriteLine(";");
  }
@@ -2791,11 +2807,15 @@ public override void Resolve(ResolutionContext rc) {
  RegisterFormals(InParams, rc);
  RegisterFormals(OutParams, rc);
  ResolveAttributes(rc);
- if (Body != null)
- {
- rc.StateMode = ResolutionContext.State.StateLess;
- Body.Resolve(rc);
- rc.StateMode = ResolutionContext.State.Single;
+ if (Body != null) {
+ Contract.Assert(DefinitionBody == null);
+ rc.StateMode = ResolutionContext.State.StateLess;
+ Body.Resolve(rc);
+ rc.StateMode = ResolutionContext.State.Single;
+ } else if (DefinitionBody != null) {
+ rc.StateMode = ResolutionContext.State.StateLess;
+ DefinitionBody.Resolve(rc);
+ rc.StateMode = ResolutionContext.State.Single;
  }
  rc.PopVarContext();
  Type.CheckBoundVariableOccurrences(TypeParameters,
@@ -2814,11 +2834,21 @@ public override void Typecheck(TypecheckingContext tc) {
  base.Typecheck(tc);
  // TypecheckAttributes(tc);
  if (Body != null) {
+ Contract.Assert(DefinitionBody == null);
  Body.Typecheck(tc);
  if (!cce.NonNull(Body.Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
  tc.Error(Body,
  "function body with invalid type: {0} (expected: {1})",
  Body.Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
+ } else if (DefinitionBody != null) {
+ DefinitionBody.Typecheck(tc);
+
+ // We are matching the type of the function body with output param, and not the type
+ // of DefinitionBody, which is always going to be bool (since it is of the form func_call == func_body)
+ if (!cce.NonNull(DefinitionBody.Args[1].Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
+ tc.Error(DefinitionBody.Args[1],
+ "function body with invalid type: {0} (expected: {1})",
+ DefinitionBody.Args[1].Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
  }
  }
 
@@ -2871,6 +2901,36 @@ public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) {
  DefinitionAxiom = new Axiom(tok, def);
  return DefinitionAxiom;
  }
+
+ // Generates function definition of the form func_call == func_body
+ // For example, for
+ // function {:define} foo(x:int) returns(int) { x + 1 }
+ // this will generate
+ // foo(x):int == x + 1
+ // We need the left hand call part later on to be able to generate
+ // the appropriate SMTlib style function definition. Hence, it is
+ // important that it goes through the resolution and type checking passes,
+ // since otherwise it is hard to connect function parameters to the resolved
+ // variables in the function body.
+ public NAryExpr CreateFunctionDefinition(Expr body) {
+ Contract.Requires(body != null);
+
+ List<Expr> callArgs = new List<Expr>();
+ int i = 0;
+ foreach (Formal/*!*/ f in InParams) {
+ Contract.Assert(f != null);
+ string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;
+ callArgs.Add(new IdentifierExpr(f.tok, nm));
+ i++;
+ }
+
+ Expr call = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, Name)), callArgs);
+ // specify the type of the function, because it might be that
+ // type parameters only occur in the output type
+ call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone());
+ NAryExpr def = Expr.Binary(tok, BinaryOperator.Opcode.Eq, call, body);
+ return def;
+ }
  }
 
  public class Macro : Function {

Source/Core/AbsyQuant.cs

@@ -593,29 +593,29 @@ 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)
+ List<Variable>/*!*/ dummies, 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 ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)
+ 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)
+ 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)
+ 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);
@@ -639,22 +639,22 @@ 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);
  Contract.Requires(tok != null);
  Contract.Requires(dummies.Count > 0);
  }
- public ExistsExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)
+ public ExistsExpr(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);
@@ -898,7 +898,7 @@ public override int GetHashCode() {
 
  public class LambdaExpr : BinderExpr {
  public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
- List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)
+ List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable = false)
  : base(tok, typeParameters, dummies, kv, body, immutable) {
  Contract.Requires(tok != null);
  Contract.Requires(typeParameters != null);

Source/Core/BoogiePL.atg

@@ -520,7 +520,13 @@ Function<.out List<Declaration>/*!*/ ds.>
  if (definition != null) {
  // generate either an axiom or a function body
  if (QKeyValue.FindBoolAttribute(kv, "inline")) {
+ if (QKeyValue.FindBoolAttribute(kv, "define"))
+ SemErr("function cannot have both :inline and :define attributes");
  func.Body = definition;
+ } else if (QKeyValue.FindBoolAttribute(kv, "define")) {
+ if (func.TypeParameters.Count > 0)
+ SemErr("function with :define attribute has to be monomorphic");
+ func.DefinitionBody = func.CreateFunctionDefinition(definition);
  } else {
  ds.Add(func.CreateDefinitionAxiom(definition, kv));
  }

Source/Core/CommandLineOptions.cs

@@ -1621,9 +1621,17 @@ result caching (default: ""<impl. name>:0"").
  {:bvbuiltin ""spec""}
  Rewrite the function to built-in prover function symbol 'fn'.
 
+ {:define}
+ {:define true}
+ Turn this function into a definition (using the define-fun construct)
+ when using the SMT-LIB backend. Can only be used with non-recursive
+ functions. Cannot be combined with :inline attribute.
+ Currently works only with monomorphic functions.
+
  {:inline}
  {:inline true}
  Expand function according to its definition before going to the prover.
+ Cannot be combined with :define attribute.
 
  {:never_pattern true}
  Terms starting with this function symbol will never be

Source/Core/Parser.cs

@@ -427,7 +427,13 @@ void Function(out List<Declaration>/*!*/ ds) {
  if (definition != null) {
  // generate either an axiom or a function body
  if (QKeyValue.FindBoolAttribute(kv, "inline")) {
+ if (QKeyValue.FindBoolAttribute(kv, "define"))
+ SemErr("function cannot have both :inline and :define attributes");
  func.Body = definition;
+ } else if (QKeyValue.FindBoolAttribute(kv, "define")) {
+ if (func.TypeParameters.Count > 0)
+ SemErr("function with :define attribute has to be monomorphic");
+ func.DefinitionBody = func.CreateFunctionDefinition(definition);
  } else {
  ds.Add(func.CreateDefinitionAxiom(definition, kv));
  }
@@ -2426,4 +2432,4 @@ public FatalError(string m): base(m) {}
 }
 
 
-}
+}

Source/Core/StandardVisitor.cs

@@ -325,8 +325,11 @@ public virtual Function VisitFunction(Function node) {
  Contract.Requires(node != null);
  Contract.Ensures(Contract.Result<Function>() != null);
  node = (Function)this.VisitDeclWithFormals(node);
- if (node.Body != null)
+ if (node.Body != null) {
+ Contract.Assert(node.DefinitionBody == null);
  node.Body = this.VisitExpr(node.Body);
+ } else if (node.DefinitionBody != null)
+ node.DefinitionBody = (NAryExpr)this.VisitExpr(node.DefinitionBody);
  return node;
  }
  public virtual GlobalVariable VisitGlobalVariable(GlobalVariable node) {
@@ -892,8 +895,11 @@ public override Function VisitFunction(Function node)
  {
  Contract.Ensures(Contract.Result<Function>() == node);
  node = (Function)this.VisitDeclWithFormals(node);
- if (node.Body != null)
- this.VisitExpr(node.Body);
+ if (node.Body != null) {
+ Contract.Assert(node.DefinitionBody == null);
+ this.VisitExpr(node.Body);
+ } else if (node.DefinitionBody != null)
+ this.VisitExpr(node.DefinitionBody);
  return node;
  }
  public override GlobalVariable VisitGlobalVariable(GlobalVariable node)