Skip to content

Commit

Permalink
Apply simplification to Imp and Iff connectives (#4533)
Browse files Browse the repository at this point in the history
Boogie applies simplification to `Bpl.And` and `Bpl.Or`, but [not
to](https://github.com/boogie-org/boogie/blob/f088818450b0e9928a674e832435617a70c37ea7/Source/Core/AST/AbsyExpr.cs#L338-L352)
`Bpl.Imp` and `Bpl.Iff`. Dafny provides [wrapper
methods](https://github.com/dafny-lang/dafny/blob/37e00f70c3007002c4470a2d0129d66724473850/Source/DafnyCore/Verifier/Translator.BoogieFactory.cs#L772-L798)
to apply these connectives which also apply simplification to `Imp` and
`Iff`; however they do not seem to be used consistently and are missing
some cases.

This PR replaces all direct usages of the Boogie methods `Bpl.And`,
`Bpl.Or`, `Bpl.Imp` and `Bpl.Iff` with wrappers from Dafny, and adds
code to avoid adding `true` axioms in cases where I noticed this
happens. (A better solution might be to provide a single point for
adding axioms where this check could be added.)

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

---------

Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
  • Loading branch information
zafer-esen and atomb authored Apr 2, 2024
1 parent c931468 commit 2cc052c
Showing 30 changed files with 703 additions and 646 deletions.
46 changes: 36 additions & 10 deletions Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs
Original file line number Diff line number Diff line change
@@ -628,7 +628,7 @@ public Bpl.Expr ProperPrefix(Bpl.IToken tok, Bpl.Expr e0, Bpl.Expr e1) {
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
Bpl.Expr len0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
Bpl.Expr len1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
var result = Bpl.Expr.And(
var result = BplAnd(
Bpl.Expr.Lt(len0, len1),
FunctionCall(tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0));
result.tok = tok;
@@ -698,10 +698,15 @@ static Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.True) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.True) {
return b;
} else if (b == Bpl.Expr.True) {
} else if (bNoLit == Bpl.Expr.True) {
return a;
} else if (aNoLit == Bpl.Expr.False || bNoLit == Bpl.Expr.False) {
return Bpl.Expr.False;
} else {
return Bpl.Expr.Binary(a.tok, Bpl.BinaryOperator.Opcode.And, a, b);
}
@@ -721,24 +726,42 @@ static Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.False) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.False) {
return b;
} else if (b == Bpl.Expr.False) {
} else if (bNoLit == Bpl.Expr.False) {
return a;
} else if (aNoLit == Bpl.Expr.True) {
return a;
} else if (bNoLit == Bpl.Expr.True) {
return b;
} else {
return Bpl.Expr.Binary(a.tok, Bpl.BinaryOperator.Opcode.Or, a, b);
}
}

Bpl.Expr BplIff(Bpl.Expr a, Bpl.Expr b) {
static Bpl.Expr BplIff(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.True) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.True) {
return b;
} else if (b == Bpl.Expr.True) {
} else if (bNoLit == Bpl.Expr.True) {
return a;
} else if (aNoLit == Bpl.Expr.False) {
return Bpl.Expr.Not(b);
} else if (bNoLit == Bpl.Expr.False) {
return Bpl.Expr.Not(a);
} else if (aNoLit == bNoLit) {
return Bpl.Expr.True;
} else if (aNoLit == Bpl.Expr.Not(b) || bNoLit == Bpl.Expr.Not(a)) {
return Bpl.Expr.False;
} else {
return Bpl.Expr.Iff(a, b);
}
@@ -749,9 +772,12 @@ static Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.True || b == Bpl.Expr.True) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.True || bNoLit == Bpl.Expr.True) {
return b;
} else if (a == Bpl.Expr.False) {
} else if (aNoLit == Bpl.Expr.False) {
return Bpl.Expr.True;
} else {
return Bpl.Expr.Imp(a, b);
20 changes: 10 additions & 10 deletions Source/DafnyCore/Verifier/BoogieGenerator.DataTypes.cs
Original file line number Diff line number Diff line change
@@ -43,7 +43,7 @@ void AddDatatype(DatatypeDecl dt) {
cases_body = BplOr(cases_body, disj);
tr = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { disj, isPredicate }, tr);
}
var body = Bpl.Expr.Imp(isPredicate, cases_body);
var body = BplImp(isPredicate, cases_body);
var ax = BplForall(boundVariables, tr, body);
var axiom = new Bpl.Axiom(dt.tok, ax, "Questionmark data type disjunctivity");
sink.AddTopLevelDeclaration(axiom);
@@ -124,7 +124,7 @@ private void AddInductiveDatatypeAxioms(Dictionary<DatatypeCtor, Bpl.Function> c
eqs = BplAnd(eqs, eq);
}

var ax = BplForall(new List<Variable> { aVar, bVar }, trigger, Bpl.Expr.Imp(ante, Bpl.Expr.Iff(dtEqual, eqs)));
var ax = BplForall(new List<Variable> { aVar, bVar }, trigger, BplImp(ante, BplIff(dtEqual, eqs)));
AddOtherDefinition(constructorFunctions[ctor], new Bpl.Axiom(dt.tok, ax, $"Datatype extensional equality definition: {ctor.FullName}"));
}
}
@@ -143,7 +143,7 @@ private void AddExtensionalityAxiom(IndDatatypeDecl dt) {
var lhs = FunctionCall(dt.tok, dtEqualName, Bpl.Type.Bool, a, b);
var rhs = Bpl.Expr.Eq(a, b);

var ax = BplForall(new List<Variable> { aVar, bVar }, BplTrigger(lhs), Bpl.Expr.Iff(lhs, rhs));
var ax = BplForall(new List<Variable> { aVar, bVar }, BplTrigger(lhs), BplIff(lhs, rhs));
sink.AddTopLevelDeclaration(new Bpl.Axiom(dt.tok, ax, $"Datatype extensionality axiom: {dt.FullName}"));
}
}
@@ -423,7 +423,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var queryPredicate = FunctionCall(ctor.tok, queryField.Name, Bpl.Type.Bool, th);
var ctorId = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, th);
var rhs = Bpl.Expr.Eq(ctorId, constructorIdReference);
var body = Bpl.Expr.Iff(queryPredicate, rhs);
var body = BplIff(queryPredicate, rhs);
var tr = BplTrigger(queryPredicate);
var ax = BplForall(thVar, tr, body);
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, ax, "Questionmark and identifier"));
@@ -517,7 +517,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
Bpl.Variable iVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "i", Bpl.Type.Int));
bvs.Add(iVar);
Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, iVar);
Bpl.Expr ante = Bpl.Expr.And(
Bpl.Expr ante = BplAnd(
Bpl.Expr.Le(Bpl.Expr.Literal(0), ie),
Bpl.Expr.Lt(ie, FunctionCall(arg.tok, BuiltinFunction.SeqLength, null, args[i])));
var seqIndex = FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie);
@@ -526,7 +526,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
q = new Bpl.ForallExpr(ctor.tok, bvs, new Trigger(lhs.tok, true, new List<Bpl.Expr> { seqIndex, ct }),
Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
BplImp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive seq element rank"));
}

@@ -553,7 +553,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inSet, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(inSet, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inSet, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive set element rank"));
} else if (argType is MultiSetType) {
// axiom (forall params, d: Datatype {arg[d], #dt.ctor(params)} :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
@@ -569,7 +569,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inMultiset, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive multiset element rank"));
} else if (argType is MapType) {
var finite = ((MapType)argType).Finite;
@@ -589,7 +589,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inDomain, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive map key rank"));
}
{
@@ -613,7 +613,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inDomain, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive map value rank"));
}
}
32 changes: 16 additions & 16 deletions Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs
Original file line number Diff line number Diff line change
@@ -82,7 +82,7 @@ void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Ex
bool endsWithWinningTopComparison = N == contextDecreases.Count && N < calleeDecreases.Count;
Bpl.Expr decrExpr = DecreasesCheck(toks, types0, types1, callee, caller, builder, "", endsWithWinningTopComparison, false);
if (allowance != null) {
decrExpr = Bpl.Expr.Or(allowance, decrExpr);
decrExpr = BplOr(allowance, decrExpr);
}
builder.Add(Assert(tok, decrExpr, new PODesc.Terminates(inferredDecreases, false, hint)));
}
@@ -125,7 +125,7 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1,
// we only need to check lower bound for integers--sets, sequences, booleans, references, and datatypes all have natural lower bounds
Bpl.Expr prefixIsLess = Bpl.Expr.False;
for (int i = 0; i < k; i++) {
prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);
prefixIsLess = BplOr(prefixIsLess, Less[i]);
};

Bpl.Expr zero = null;
@@ -140,9 +140,9 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1,
if (zero != null) {
Bpl.Expr bounded = Bpl.Expr.Le(zero, ee1[k]);
for (int i = 0; i < k; i++) {
bounded = Bpl.Expr.Or(bounded, Less[i]);
bounded = BplOr(bounded, Less[i]);
}
Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), new PODesc.DecreasesBoundedBelow(N, k, zeroStr, suffixMsg));
Bpl.Cmd cmd = Assert(toks[k], BplOr(bounded, Eq[k]), new PODesc.DecreasesBoundedBelow(N, k, zeroStr, suffixMsg));
builder.Add(cmd);
}
}
@@ -154,10 +154,10 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1,
Bpl.Expr eq = Eq[i];
if (allowNoChange) {
// decrCheck = atmost && (eq ==> decrCheck)
decrCheck = Bpl.Expr.And(less, Bpl.Expr.Imp(eq, decrCheck));
decrCheck = BplAnd(less, BplImp(eq, decrCheck));
} else {
// decrCheck = less || (eq && decrCheck)
decrCheck = Bpl.Expr.Or(less, Bpl.Expr.And(eq, decrCheck));
decrCheck = BplOr(less, BplAnd(eq, decrCheck));
}
}
return decrCheck;
@@ -236,9 +236,9 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
less = Bpl.Expr.Lt(b0, b1);
atmost = Bpl.Expr.Le(b0, b1);
} else if (ty0 is BoolType) {
eq = Bpl.Expr.Iff(e0, e1);
less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
atmost = Bpl.Expr.Imp(e0, e1);
eq = BplIff(e0, e1);
less = BplAnd(Bpl.Expr.Not(e0), e1);
atmost = BplImp(e0, e1);
} else if (ty0 is CharType) {
eq = Bpl.Expr.Eq(e0, e1);
var operand0 = FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, e0);
@@ -263,17 +263,17 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
less = Bpl.Expr.Lt(b0, b1);
atmost = Bpl.Expr.Le(b0, b1);
if (ty0.IsNumericBased(Type.NumericPersuasion.Int) && includeLowerBound) {
less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), less);
atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);
less = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), less);
atmost = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);
}

} else if (ty0.IsNumericBased(Type.NumericPersuasion.Real)) {
eq = Bpl.Expr.Eq(e0, e1);
less = Bpl.Expr.Le(e0, Bpl.Expr.Sub(e1, Bpl.Expr.Literal(BaseTypes.BigDec.FromInt(1))));
atmost = Bpl.Expr.Le(e0, e1);
if (includeLowerBound) {
less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), less);
atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), atmost);
less = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), less);
atmost = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), atmost);
}

} else if (ty0 is IteratorDecl.EverIncreasingType) {
@@ -342,9 +342,9 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
Contract.Assert(ty0.IsRefType); // otherwise, unexpected type
var b0 = Bpl.Expr.Neq(e0, predef.Null);
var b1 = Bpl.Expr.Neq(e1, predef.Null);
eq = Bpl.Expr.Iff(b0, b1);
less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);
atmost = Bpl.Expr.Imp(b0, b1);
eq = BplIff(b0, b1);
less = BplAnd(Bpl.Expr.Not(b0), b1);
atmost = BplImp(b0, b1);
}
}
}
Loading

0 comments on commit 2cc052c

Please sign in to comment.