Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refactored the define attribute on functions #236

Merged
merged 31 commits into from
Jun 4, 2020
Merged

Refactored the define attribute on functions #236

Show file tree
Hide file tree
Changes from 27 commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
ab5df04
fixup! Add support for function definitions
Feb 22, 2020
f29eedd
Add support for function definitions
Feb 15, 2020
f321806
fixup! Add support for function definitions
Feb 15, 2020
d746ece
fixup! Add support for function definitions
Feb 21, 2020
8b416f9
fixup! Add support for function definitions
Feb 21, 2020
18e18ab
fixup! Add support for function definitions
Feb 22, 2020
a4aed19
fixup! Add support for function definitions
Feb 22, 2020
778d897
Refactored support for function definitions
zvonimir May 28, 2020
e61b35a
Minor fix, no need to pass false as immutable to forall constructor
zvonimir May 28, 2020
d9be498
Fixed indentation in parser
zvonimir May 28, 2020
2cbc782
Moved data type processing into a separate function
zvonimir May 28, 2020
32d5c3d
Moved processing of function definitions into a separate file
zvonimir May 28, 2020
5fabe6f
Prevent function arguments from being declared in SMT queries
zvonimir May 28, 2020
d6820fe
Cleaned up the code and added some comments
zvonimir May 28, 2020
c45d561
Fixed a problem with missing function definition dependencies
zvonimir May 29, 2020
770b21b
Renamed DefBody into DefinitionBody
zvonimir May 29, 2020
6fae2eb
Function cannot have both inline and define enabled
zvonimir May 29, 2020
2978973
Added assertions and more comments
zvonimir May 29, 2020
2dbc8c3
Added more complex regressions that use function definitions
zvonimir May 29, 2020
a3f14e4
Added more regressions
zvonimir May 29, 2020
11d834f
Minor fix since I messed up expected output for a regression
zvonimir May 29, 2020
c3c56bf
Merge branch 'master' into define-func
zvonimir May 29, 2020
440921e
Fixed expected regression results based on updates to CIVL
zvonimir May 29, 2020
c3a1f48
Merge branch 'master' into define-func
zvonimir May 29, 2020
b90bb21
Added useArrayTheory to SMACK regression that uses function definitions
zvonimir May 29, 2020
7795d0f
Function definitions work only with monomorphic functions
zvonimir May 29, 2020
719c84f
Added checking and error reporting for polymorphic functions
zvonimir May 29, 2020
723f921
Minor fix to wording of error messages
zvonimir Jun 2, 2020
83bbd83
Added regression that checks for recursion in function definitions
zvonimir Jun 2, 2020
6728ce2
Minor fix
zvonimir Jun 3, 2020
5260c33
Check for function monomorphism before creating definition body
zvonimir Jun 3, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 68 additions & 8 deletions Source/Core/Absy.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I concede that this makes the code clearer, but it does require you to duplicate code - wherever Body was used before, there are now two cases. I did not attempt to check that you caught every such case, so I have to trust you did.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, you are absolutely right, and this is a valid point. I made sure I checked off all such occurrences and I don't think I missed any.
The original plan I discussed with Shaz was not to duplicate code, but to use Body for both. However, Body is being leveraged in rarely used codes (AbstractHoudini and FixedPointVC) that we do not quite understand. Hence, I was hesitant to reuse it until someone either cleans up AbstractHoudini and FixedPointVC or completely removes them. My time was running out and I did not get to that.

public Axiom DefinitionAxiom;

public IList<Axiom> otherDefinitionAxioms;
Expand Down Expand Up @@ -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} ");
}
zvonimir marked this conversation as resolved.
Show resolved Hide resolved
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(";");
}
Expand All @@ -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,
Expand All @@ -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);
}
}

Expand Down Expand Up @@ -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 is goes through the resolution and type checking passes,
zvonimir marked this conversation as resolved.
Show resolved Hide resolved
// since otherwise it is hard to connect function parameters to the resolved
// variables in the function body.
public NAryExpr CreateFunctionDefinition(Expr body) {
zvonimir marked this conversation as resolved.
Show resolved Hide resolved
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 {
Expand Down
16 changes: 8 additions & 8 deletions Source/Core/AbsyQuant.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
Expand Down Expand Up @@ -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);
Expand Down
6 changes: 6 additions & 0 deletions Source/Core/BoogiePL.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")) {
func.DefinitionBody = func.CreateFunctionDefinition(definition);
if (func.TypeParameters.Count > 0)
zvonimir marked this conversation as resolved.
Show resolved Hide resolved
SemErr("function with define attribute has to be monomorphic");
zvonimir marked this conversation as resolved.
Show resolved Hide resolved
} else {
ds.Add(func.CreateDefinitionAxiom(definition, kv));
}
Expand Down
8 changes: 8 additions & 0 deletions Source/Core/CommandLineOptions.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
zvonimir marked this conversation as resolved.
Show resolved Hide resolved
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
Expand Down
8 changes: 7 additions & 1 deletion Source/Core/Parser.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")) {
func.DefinitionBody = func.CreateFunctionDefinition(definition);
if (func.TypeParameters.Count > 0)
SemErr("function with define attribute has to be monomorphic");
} else {
ds.Add(func.CreateDefinitionAxiom(definition, kv));
}
Expand Down Expand Up @@ -2426,4 +2432,4 @@ public FatalError(string m): base(m) {}
}


}
}
12 changes: 9 additions & 3 deletions Source/Core/StandardVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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)
Expand Down
Loading