Skip to content

Commit

Permalink
Move resolution of UnaryOpExpr to resolver (#2096)
Browse files Browse the repository at this point in the history 
* refactor(translator): Move resolution of UnaryOpExpr to resolver

* Source/Dafny/AST/DafnyAst.cs:

  (ResolvedOpcode):
    New enum.
  (ResolvedOp):
    New property (computed on demand, cached).
  (ResolveOp):
    New function to force the computation of ResolvedOp.

* Source/Dafny/Compilers/SinglePassCompiler.cs:

  (UnaryOpCodeMap):
    New map from resolved unary operators to compiler-level resolved unary
    operators (compilers treat all cardinalities in the same way).

  (TrExpr):
    Simplify `UnaryOpExpr` case using `UnaryOpCodeMap`.

* Source/Dafny/Resolver.cs:

  (FigureOutNativeType):
    Simplify `UnaryOpExpr` case and fix GH-2095.

  (CheckTypeInference_Visitor.VisitOneExpr):
    Force resolution of unary operators.

* Source/Dafny/Resolver/BoundsDiscovery.cs:

  (DiscoverAllBounds_Aux_SingleVar):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Triggers/TriggerExtensions.cs:

  (ShallowEq(BinaryExpr, BinaryExpr)):
    Remove redundant contracts.

  (ShallowEq(UnaryOpExpr, UnaryOpExpr)):
    Compare resolved operators.

* Source/Dafny/Verifier/Translator.ExpressionTranslator.cs:

  (TrExpr):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Verifier/Translator.cs:

  (TrSplitExpr):
    Use `ResolvedOp` (should be a no-op because we're already in Bool context).

* Update Source/Dafny/AST/DafnyAst.cs

* Update Source/Dafny/Resolver.cs

Co-authored-by: Marianna Rapoport <[email protected]>

Co-authored-by: Marianna Rapoport <[email protected]>
  • Loading branch information
@cpitclaudel @amaurremi
cpitclaudel and amaurremi authored May 12, 2022
1 parent 82a1ec3 commit 1647032
Show file tree
Hide file tree
Showing 8 changed files with 96 additions and 67 deletions.
38 changes: 38 additions & 0 deletions Source/Dafny/AST/DafnyAst.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10874,6 +10874,44 @@ public enum Opcode {
}
public readonly Opcode Op;

public enum ResolvedOpcode {
YetUndetermined,
BVNot,
BoolNot,
SeqLength,
SetCard,
MultiSetCard,
MapCard,
Fresh,
Allocated,
Lit
}

private ResolvedOpcode _ResolvedOp = ResolvedOpcode.YetUndetermined;
public ResolvedOpcode ResolvedOp => ResolveOp();

public ResolvedOpcode ResolveOp() {
if (_ResolvedOp == ResolvedOpcode.YetUndetermined) {
Contract.Assert(Type != null);
Contract.Assert(Type is not TypeProxy);
_ResolvedOp = (Op, E.Type.NormalizeExpand()) switch {
(Opcode.Not, BoolType _) => ResolvedOpcode.BoolNot,
(Opcode.Not, BitvectorType _) => ResolvedOpcode.BVNot,
(Opcode.Cardinality, SeqType _) => ResolvedOpcode.SeqLength,
(Opcode.Cardinality, SetType _) => ResolvedOpcode.SetCard,
(Opcode.Cardinality, MultiSetType _) => ResolvedOpcode.MultiSetCard,
(Opcode.Cardinality, MapType _) => ResolvedOpcode.MapCard,
(Opcode.Fresh, _) => ResolvedOpcode.Fresh,
(Opcode.Allocated, _) => ResolvedOpcode.Allocated,
(Opcode.Lit, _) => ResolvedOpcode.Lit,
_ => ResolvedOpcode.YetUndetermined // Unreachable
};
Contract.Assert(_ResolvedOp != ResolvedOpcode.YetUndetermined);
}

return _ResolvedOp;
}

public UnaryOpExpr(IToken tok, Opcode op, Expression e)
: base(tok, e) {
Contract.Requires(tok != null);
Expand Down
29 changes: 13 additions & 16 deletions Source/Dafny/Compilers/SinglePassCompiler.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1061,6 +1061,16 @@ protected abstract ConcreteSyntaxTree CreateIIFE0(Type resultType, Bpl.IToken re
protected abstract ConcreteSyntaxTree CreateIIFE1(int source, Type resultType, Bpl.IToken resultTok, string bvName,
ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts); // Immediately Invoked Function Expression
public enum ResolvedUnaryOp { BoolNot, BitwiseNot, Cardinality }

protected static readonly Dictionary<UnaryOpExpr.ResolvedOpcode, ResolvedUnaryOp> UnaryOpCodeMap = new() {
[UnaryOpExpr.ResolvedOpcode.BVNot] = ResolvedUnaryOp.BitwiseNot,
[UnaryOpExpr.ResolvedOpcode.BoolNot] = ResolvedUnaryOp.BoolNot,
[UnaryOpExpr.ResolvedOpcode.SeqLength] = ResolvedUnaryOp.Cardinality,
[UnaryOpExpr.ResolvedOpcode.SetCard] = ResolvedUnaryOp.Cardinality,
[UnaryOpExpr.ResolvedOpcode.MultiSetCard] = ResolvedUnaryOp.Cardinality,
[UnaryOpExpr.ResolvedOpcode.MapCard] = ResolvedUnaryOp.Cardinality
};

protected abstract void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool inLetExprBody,
ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts);

Expand Down Expand Up @@ -4532,23 +4542,10 @@ void writeObj(ConcreteSyntaxTree w) {

} else if (expr is UnaryOpExpr) {
var e = (UnaryOpExpr)expr;
switch (e.Op) {
case UnaryOpExpr.Opcode.Not:
if (e.Type.IsBitVectorType) {
var bvType = e.Type.AsBitVectorType;
var wrTruncOperand = EmitBitvectorTruncation(bvType, false, wr);
EmitUnaryExpr(ResolvedUnaryOp.BitwiseNot, e.E, inLetExprBody, wrTruncOperand, wStmts);
} else {
EmitUnaryExpr(ResolvedUnaryOp.BoolNot, e.E, inLetExprBody, wr, wStmts);
}
break;
case UnaryOpExpr.Opcode.Cardinality:
EmitUnaryExpr(ResolvedUnaryOp.Cardinality, e.E, inLetExprBody, wr, wStmts);
break;
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot) {
wr = EmitBitvectorTruncation(e.Type.AsBitVectorType, false, wr);
}

EmitUnaryExpr(UnaryOpCodeMap[e.ResolvedOp], e.E, inLetExprBody, wr, wStmts);
} else if (expr is ConversionExpr) {
var e = (ConversionExpr)expr;
Contract.Assert(e.ToType.IsRefType == e.E.Type.IsRefType);
Expand Down
30 changes: 15 additions & 15 deletions Source/Dafny/Resolver.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3796,20 +3796,15 @@ Type AsUnconstrainedType(Type t) {
if (e is LiteralExpr l) {
return l.Value;
} else if (e is UnaryOpExpr un) {
if (un.Op == UnaryOpExpr.Opcode.Not) {
object e0 = GetAnyConst(un.E, consts);
if (e0 is bool) {
return !(bool)e0;
}
if (un.Type.IsBitVectorType) {
int width = un.Type.AsBitVectorType.Width;
return ((BigInteger.One << width) - 1) ^ (BigInteger)e0;
}
} else if (un.Op == UnaryOpExpr.Opcode.Cardinality) {
object e0 = GetAnyConst(un.E, consts);
if (e0 is string ss) {
return (BigInteger)(ss.Length);
}
if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot && GetAnyConst(un.E, consts) is bool b) {
return !b;
}
if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot && GetAnyConst(un.E, consts) is BigInteger i) {
return ((BigInteger.One << un.Type.AsBitVectorType.Width) - 1) ^ i;
}
// TODO: This only handles strings; generalize to other collections?
if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.SeqLength && GetAnyConst(un.E, consts) is string ss) {
return (BigInteger)(ss.Length);
}
} else if (e is MemberSelectExpr m) {
if (m.Member is ConstantField c && c.IsStatic && c.Rhs != null) {
Expand Down Expand Up @@ -6839,7 +6834,9 @@ protected override void VisitOneExpr(Expression expr) {
"a non-trivial type test is allowed only for reference types (tried to test if '{1}' is a '{0}')", e.ToType, fromType);
}
} else if (CheckTypeIsDetermined(expr.tok, expr.Type, "expression")) {
if (expr is BinaryExpr) {
if (expr is UnaryOpExpr uop) {
uop.ResolveOp(); // Force resolution eagerly at this point to catch potential bugs
} else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
e.ResolvedOp = ResolveOp(e.Op, e.E0.Type, e.E1.Type);
// Check for useless comparisons with "null"
Expand Down Expand Up @@ -14946,6 +14943,9 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator
}

// We do not have enough information to compute `e.ResolvedOp` yet.
// For binary operators the computation happens in `CheckTypeInference`.
// For unary operators it happens lazily in the getter of `e.ResolvedOp`.
} else if (expr is ConversionExpr) {
var e = (ConversionExpr)expr;
ResolveExpression(e.E, opts);
Expand Down
5 changes: 2 additions & 3 deletions Source/Dafny/Resolver/BoundsDiscovery.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,10 +149,9 @@ public partial class Resolver {
if (unary != null) {
var ide = unary.E.Resolved as IdentifierExpr;
if (ide != null && ide.Var == (IVariable)bv) {
if (unary.Op == UnaryOpExpr.Opcode.Not) {
Contract.Assert(bv.Type.IsBoolType);
if (unary.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) {
bounds.Add(new ComprehensionExpr.ExactBoundedPool(Expression.CreateBoolLiteral(Token.NoToken, false)));
} else if (unary.Op == UnaryOpExpr.Opcode.Allocated) {
} else if (unary.ResolvedOp == UnaryOpExpr.ResolvedOpcode.Allocated) {
bounds.Add(new ComprehensionExpr.ExplicitAllocatedBoundedPool());
}
}
Expand Down
4 changes: 1 addition & 3 deletions Source/Dafny/Triggers/TriggerExtensions.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -365,8 +365,6 @@ private static bool ShallowEq(TernaryExpr expr1, TernaryExpr expr2) {
}

private static bool ShallowEq(BinaryExpr expr1, BinaryExpr expr2) {
Contract.Requires(expr1.ResolvedOp != BinaryExpr.ResolvedOpcode.YetUndetermined);
Contract.Requires(expr2.ResolvedOp != BinaryExpr.ResolvedOpcode.YetUndetermined);
return expr1.ResolvedOp == expr2.ResolvedOp;
}

Expand All @@ -379,7 +377,7 @@ private static bool ShallowEq(TypeTestExpr expr1, TypeTestExpr expr2) {
}

private static bool ShallowEq(UnaryOpExpr expr1, UnaryOpExpr expr2) {
return expr1.Op == expr2.Op;
return expr1.ResolvedOp == expr2.ResolvedOp;
}

private static bool ShallowEq(UnaryExpr expr1, UnaryExpr expr2) {
Expand Down
2 changes: 1 addition & 1 deletion Source/Dafny/Util.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1106,7 +1106,7 @@ public static bool UsesSpecFeatures(Expression expr) {
return true;
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
if (e is UnaryOpExpr unaryOpExpr && (unaryOpExpr.Op == UnaryOpExpr.Opcode.Fresh || unaryOpExpr.Op == UnaryOpExpr.Opcode.Allocated)) {
if (e is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Fresh or UnaryOpExpr.Opcode.Allocated }) {
return true;
}
if (expr is TypeTestExpr tte && !IsTypeTestCompilable(tte)) {
Expand Down
53 changes: 25 additions & 28 deletions Source/Dafny/Verifier/Translator.ExpressionTranslator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -705,35 +705,32 @@ public Boogie.Expr TrExpr(Expression expr) {
} else if (expr is UnaryOpExpr) {
var e = (UnaryOpExpr)expr;
Boogie.Expr arg = TrExpr(e.E);
switch (e.Op) {
case UnaryOpExpr.Opcode.Lit:
switch (e.ResolvedOp) {
case UnaryOpExpr.ResolvedOpcode.Lit:
return MaybeLit(arg);
case UnaryOpExpr.Opcode.Not:
if (expr.Type.IsBitVectorType) {
var bvWidth = expr.Type.AsBitVectorType.Width;
var bvType = translator.BplBvType(bvWidth);
Boogie.Expr r = FunctionCall(GetToken(expr), "not_bv" + bvWidth, bvType, arg);
if (translator.IsLit(arg)) {
r = MaybeLit(r, bvType);
}
return r;
} else {
return Boogie.Expr.Unary(GetToken(expr), UnaryOperator.Opcode.Not, arg);
}
case UnaryOpExpr.Opcode.Cardinality:
var eType = e.E.Type.NormalizeExpand();
if (eType is SeqType) {
return translator.FunctionCall(GetToken(expr), BuiltinFunction.SeqLength, null, arg);
} else if (eType is SetType && ((SetType)eType).Finite) {
return translator.FunctionCall(GetToken(expr), BuiltinFunction.SetCard, null, arg);
} else if (eType is MultiSetType) {
return translator.FunctionCall(GetToken(expr), BuiltinFunction.MultiSetCard, null, arg);
} else if (eType is MapType && ((MapType)eType).Finite) {
return translator.FunctionCall(GetToken(expr), BuiltinFunction.MapCard, null, arg);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected sized type
case UnaryOpExpr.ResolvedOpcode.BVNot:
var bvWidth = expr.Type.AsBitVectorType.Width;
var bvType = translator.BplBvType(bvWidth);
Boogie.Expr r = FunctionCall(GetToken(expr), "not_bv" + bvWidth, bvType, arg);
if (translator.IsLit(arg)) {
r = MaybeLit(r, bvType);
}
case UnaryOpExpr.Opcode.Fresh:
return r;
case UnaryOpExpr.ResolvedOpcode.BoolNot:
return Boogie.Expr.Unary(GetToken(expr), UnaryOperator.Opcode.Not, arg);
case UnaryOpExpr.ResolvedOpcode.SeqLength:
Contract.Assert(e.E.Type.NormalizeExpand() is SeqType);
return translator.FunctionCall(GetToken(expr), BuiltinFunction.SeqLength, null, arg);
case UnaryOpExpr.ResolvedOpcode.SetCard:
Contract.Assert(e.E.Type.NormalizeExpand() is SetType { Finite: true });
return translator.FunctionCall(GetToken(expr), BuiltinFunction.SetCard, null, arg);
case UnaryOpExpr.ResolvedOpcode.MultiSetCard:
Contract.Assert(e.E.Type.NormalizeExpand() is MultiSetType);
return translator.FunctionCall(GetToken(expr), BuiltinFunction.MultiSetCard, null, arg);
case UnaryOpExpr.ResolvedOpcode.MapCard:
Contract.Assert(e.E.Type.NormalizeExpand() is MapType { Finite: true });
return translator.FunctionCall(GetToken(expr), BuiltinFunction.MapCard, null, arg);
case UnaryOpExpr.ResolvedOpcode.Fresh:
var freshLabel = ((FreshExpr)e).AtLabel;
var eeType = e.E.Type.NormalizeExpand();
if (eeType is SetType) {
Expand Down Expand Up @@ -770,7 +767,7 @@ public Boogie.Expr TrExpr(Expression expr) {
Boogie.Expr oIsFresh = Boogie.Expr.Not(OldAt(freshLabel).IsAlloced(GetToken(expr), TrExpr(e.E)));
return Boogie.Expr.Binary(GetToken(expr), BinaryOperator.Opcode.And, oNull, oIsFresh);
}
case UnaryOpExpr.Opcode.Allocated: {
case UnaryOpExpr.ResolvedOpcode.Allocated: {
var aType = e.E.Type.NormalizeExpand();
return translator.MkIsAlloc(TrExpr(e.E), aType, HeapExpr);
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Dafny/Verifier/Translator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11142,7 +11142,7 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos

} else if (expr is UnaryOpExpr) {
var e = (UnaryOpExpr)expr;
if (e.Op == UnaryOpExpr.Opcode.Not) {
if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) {
var ss = new List<SplitExprInfo>();
if (TrSplitExpr(e.E, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {
foreach (var s in ss) {
Expand Down

0 comments on commit 1647032

Please sign in to comment.