Refactored code that generates an axiom for a function, and changed the pretty printing to always reflect when a function body is inlined

4 files changed, 42 insertions, 58 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index ae1ee472..967ac4e3 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1971,6 +1971,13 @@ namespace Microsoft.Boogie {
       }

       stream.Write(this, level, "function ");

       EmitAttributes(stream);

+      if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline")) {

+        // 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

+        // 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 (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

         stream.Write("h{0}^^{1}", this.GetHashCode(), TokenTextWriter.SanitizeIdentifier(this.Name));

       } else {

@@ -2042,6 +2049,39 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Absy>() != null);

       return visitor.VisitFunction(this);

     }

+

+    public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) {

+      Contract.Requires(definition != null);

+

+      VariableSeq dummies = new VariableSeq();

+      ExprSeq callArgs = new ExprSeq();

+      int i = 0;

+      foreach (Formal/*!*/ f in InParams) {

+        Contract.Assert(f != null);

+        string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

+        dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

+        callArgs.Add(new IdentifierExpr(f.tok, nm));

+        i++;

+      }

+      TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq();

+      foreach (TypeVariable/*!*/ t in TypeParameters) {

+        Contract.Assert(t != null);

+        quantifiedTypeVars.Add(new TypeVariable(Token.NoToken, t.Name));

+      }

+

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

+      Expr def = Expr.Eq(call, definition);

+      if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

+        def = new ForallExpr(tok, quantifiedTypeVars, dummies,

+                             kv,

+                             new Trigger(tok, true, new ExprSeq(call), null),

+                             def);

+      }

+      return new Axiom(tok, def);

+    }

   }

 

   public class Macro : Function {

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 95ed548f..bf76df14 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -513,34 +513,7 @@ Function<out DeclarationSeq/*!*/ ds>
       if (QKeyValue.FindBoolAttribute(kv, "inline")) {

         func.Body = definition;

       } else {

-        VariableSeq dummies = new VariableSeq();

-        ExprSeq callArgs = new ExprSeq();

-        int i = 0;

-        foreach(Formal/*!*/ f in arguments){

-          Contract.Assert(f != null);

-          string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

-          dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

-          callArgs.Add(new IdentifierExpr(f.tok, nm));

-          i++;

-        }

-        TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();

-        foreach(TypeVariable/*!*/ t in typeParams){

-          Contract.Assert(t != null);

-          quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

-        }

-

-        Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

-        // specify the type of the function, because it might be that

-        // type parameters only occur in the output type

-        call = Expr.CoerceType(z, call, (Type)retTyd.Type.Clone());

-        Expr def = Expr.Eq(call, definition);

-        if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

-          def = new ForallExpr(z, quantifiedTypeVars, dummies,

-                               kv,

-                               new Trigger(z, true, new ExprSeq(call), null),

-                               def);

-        }

-        ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

+        ds.Add(func.CreateDefinitionAxiom(definition, kv));

       }

     }

   .)

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 80ab7d9f..5810fe49 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -418,34 +418,7 @@ private class BvBounds : Expr {
 		 if (QKeyValue.FindBoolAttribute(kv, "inline")) {

 		   func.Body = definition;

 		 } else {

-		   VariableSeq dummies = new VariableSeq();

-		   ExprSeq callArgs = new ExprSeq();

-		   int i = 0;

-		   foreach(Formal/*!*/ f in arguments){

-		     Contract.Assert(f != null);

-		     string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;

-		     dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));

-		     callArgs.Add(new IdentifierExpr(f.tok, nm));

-		     i++;

-		   }

-		   TypeVariableSeq/*!*/ quantifiedTypeVars = new TypeVariableSeq ();

-		   foreach(TypeVariable/*!*/ t in typeParams){

-		     Contract.Assert(t != null);

-		     quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));

-		   }

-		

-		   Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);

-		   // specify the type of the function, because it might be that

-		   // type parameters only occur in the output type

-		   call = Expr.CoerceType(z, call, (Type)retTyd.Type.Clone());

-		   Expr def = Expr.Eq(call, definition);

-		   if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {

-		     def = new ForallExpr(z, quantifiedTypeVars, dummies,

-		                          kv,

-		                          new Trigger(z, true, new ExprSeq(call), null),

-		                          def);

-		   }

-		   ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));

+		   ds.Add(func.CreateDefinitionAxiom(definition, kv));

 		 }

 		}

 		

diff --git a/Test/inline/Answer b/Test/inline/Answer
index ff2a5e71..aaaa138c 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1517,12 +1517,10 @@ function {:inline true} foo(x: int) : bool
 

 function {:inline false} foo2(x: int) : bool;

 

-// autogenerated definition axiom

 axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));

 

 function foo3(x: int) : bool;

 

-// autogenerated definition axiom

 axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));

 

 Boogie program verifier finished with 0 verified, 0 errors