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

Eliminate redundant computation in VC experession translation #1009

Merged
merged 2 commits into from
Mar 12, 2025
Merged

Eliminate redundant computation in VC experession translation #1009

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f56e48c
first commit
shazqadeer Mar 9, 2025
138624f
second commit
shazqadeer Mar 9, 2025
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
7 changes: 6 additions & 1 deletion Source/VCExpr/VCExprAST.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,7 +373,7 @@ public abstract class VCExprNAry : VCExpr
{
public override string ToString()
{
return $"${Op}(${String.Join(", ", Arguments)})";
return $"{Op}({String.Join(", ", Arguments)})";
}

[Pure]
Expand Down Expand Up @@ -1765,6 +1765,11 @@ public override Result Accept<Result, Arg>(
//Contract.Requires(expr != null);
return visitor.VisitBoogieFunctionOp(expr, arg);
}

public override string ToString()
{
return Func.Name;
}
}

/////////////////////////////////////////////////////////////////////////////////
Expand Down
83 changes: 4 additions & 79 deletions Source/VCExpr/VCExprASTVisitors.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1112,29 +1112,6 @@ public SubstitutingVCExprVisitor(VCExpressionGenerator gen)
Contract.Requires(gen != null);
}

// when descending across a binder, we have to check that no collisions
// or variable capture can occur. if this might happen, we replace the
// term and type variables bound by the binder with fresh variables
private bool CollisionPossible(IEnumerable<TypeVariable /*!*/> /*!*/ typeParams,
IEnumerable<VCExprVar /*!*/> /*!*/ boundVars, VCExprSubstitution /*!*/ substitution)
{
Contract.Requires(Cce.NonNullElements(typeParams));
Contract.Requires(Cce.NonNullElements(boundVars));
Contract.Requires(substitution != null);
// variables can be shadowed by a binder
if (typeParams.Any(var => substitution.ContainsKey(var)) ||
boundVars.Any(var => substitution.ContainsKey(var)))
{
return true;
}
// compute the codomain of the substitution
FreeVariableCollector coll = substitution.Codomains;
Contract.Assert(coll != null);
// variables could be captured when applying the substitution
return typeParams.Any(var => coll.FreeTypeVars.Contains(var)) ||
boundVars.Any(var => coll.FreeTermVars.Contains(var));
}

// can be overwritten if names of bound variables are to be changed
protected virtual string ChooseNewVariableName(string oldName)
{
Expand Down Expand Up @@ -1184,51 +1161,18 @@ protected virtual string ChooseNewVariableName(string oldName)
Contract.Requires(substitution != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);

// the default is to refresh bound variables only if necessary
// because of collisions
return Visit(node, substitution, false);
}

public VCExpr /*!*/ Visit(VCExprQuantifier /*!*/ node, VCExprSubstitution /*!*/ substitution,
bool refreshBoundVariables)
{
Contract.Requires(node != null);
Contract.Requires(substitution != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);

substitution.PushScope();
try
{
List<TypeVariable /*!*/> /*!*/
typeParams = node.TypeParameters;
Contract.Assert(Cce.NonNullElements(typeParams));
bool refreshAllVariables = refreshBoundVariables ||
CollisionPossible(node.TypeParameters, node.BoundVars, substitution);
if (refreshAllVariables)
{
// we introduce fresh type variables to ensure that none gets captured
typeParams = new List<TypeVariable /*!*/>();
foreach (TypeVariable /*!*/ var in node.TypeParameters)
{
Contract.Assert(var != null);
TypeVariable /*!*/
freshVar =
new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name));
Contract.Assert(freshVar != null);
typeParams.Add(freshVar);
substitution[var] = freshVar;
// this might overwrite other elements of the substitution, deliberately
}
}

List<VCExprVar /*!*/> /*!*/
boundVars = node.BoundVars;
Contract.Assert(Cce.NonNullElements(boundVars));
if (refreshAllVariables || !substitution.TypeSubstIsEmpty)
if (!substitution.TypeSubstIsEmpty)
{
// collisions are possible, or we also substitute type variables. in this case
// the bound term variables have to be replaced with fresh variables with the
// right types
// replace each bound term variable with a fresh variable of correct type
boundVars = new List<VCExprVar /*!*/>();
IDictionary<TypeVariable /*!*/, Type /*!*/> /*!*/
typeSubst = substitution.ToTypeSubst;
Expand All @@ -1243,7 +1187,6 @@ protected virtual string ChooseNewVariableName(string oldName)
Contract.Assert(freshVar != null);
boundVars.Add(freshVar);
substitution[var] = freshVar;
// this might overwrite other elements of the substitution, deliberately
}
}

Expand Down Expand Up @@ -1283,16 +1226,6 @@ public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution)
}

public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution)
{
Contract.Requires(substitution != null);
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
// the default is to refresh bound variables only if necessary
// because of collisions
return Visit(node, substitution, false);
}

public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables)
{
Contract.Requires(substitution != null);
Contract.Requires(node != null);
Expand All @@ -1301,19 +1234,12 @@ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refres
substitution.PushScope();
try
{
bool refreshAllVariables =
refreshBoundVariables ||
!substitution.TypeSubstIsEmpty ||
CollisionPossible(new List<TypeVariable /*!*/>(), node.BoundVars, substitution);

List<VCExprVar /*!*/> /*!*/
newBoundVars = node.BoundVars;
Contract.Assert(Cce.NonNullElements(newBoundVars));
if (refreshAllVariables)
if (!substitution.TypeSubstIsEmpty)
{
// collisions are possible, or we also substitute type variables. in this case
// the bound term variables have to be replaced with fresh variables with the
// right types
// replace each bound term variable with a fresh variable of correct type
newBoundVars = new List<VCExprVar /*!*/>();
IDictionary<TypeVariable /*!*/, Type /*!*/> /*!*/
typeSubst = substitution.ToTypeSubst;
Expand All @@ -1328,7 +1254,6 @@ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refres
Contract.Assert(freshVar != null);
newBoundVars.Add(freshVar);
substitution[var] = freshVar;
// this might overwrite other elements of the substitution, deliberately
}
}

Expand Down
Loading