Skip to content

Commit

Permalink
For function postcondition violations, point to the problematic expre…
Browse files Browse the repository at this point in the history 
…ssion branch (#5681)

I'm putting this PR on hold, since it increases the size of the
generated Boogie. Example: https://diff.corp.amazon.com/compare/9ap5cvpm

### Description
If the result of an expression does not satisfy the constraints of its
context, then an error is reported in the branch of the expression that
does not satisfy the context.

Effected contexts:
- Function postconditions
- Witness expressions
- Expression default values
- Subset type checks for function call arguments
- Assignment to a subset type local

Example of improved error reporting:
```dafny

function ElseError(x: int): int // previous primary error location
  ensures ElseError(x) == 0 // related error location
{
  if x == 0 then
    0 
  else 
    1 // new primary error location
}
function ThenError(x: int): int // previous primary error location
  ensures ThenError(x) == 0 // related error location
{
  if x == 0 then
    1 // new primary error location
  else 
    0 
}

function CaseError(x: int): int // previous primary error location
  ensures CaseError(x) == 1 // related error location
{
  match x {
    case 0 => 1
    case 1 => 0 // new primary error location
    case _ => 1 
  }
}

function LetError(x: int): int // previous primary error location
  ensures LetError(x) == 1 // related error location
{
  var r := 3;
  r // new primary error location
}
```

### How has this been tested?
- Added CLI test `ast/functions/ensuresReporting.dfy`
- `ast/subsetTypes/errorReporting.dfy`
- `ast/expression/functionCall.dfy`
- `ast/statement/localAssignment.dfy`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Stefan Zetzsche <[email protected]>
  • Loading branch information
@keyboardDrummer @stefan-aws
keyboardDrummer and stefan-aws authored Sep 4, 2024
1 parent c9fe1be commit ef1e3bc
Show file tree
Hide file tree
Showing 61 changed files with 825 additions and 535 deletions.
4 changes: 2 additions & 2 deletions Source/DafnyCore/Options/DafnyProject.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@
namespace Microsoft.Dafny;

public class DafnyProject : IEquatable<DafnyProject> {
public static Option<FileInfo> FindProjectOption = new("--find-project",
"Given a filesystem path, search for a project file by traversing up the file tree.");
public static Option<bool> FindProjectOption = new("--find-project",
"Uses the first specified input file as a starting path, from which to search for a project file by traversing up the file tree.");

static DafnyProject() {
OptionRegistry.RegisterOption(FindProjectOption, OptionScope.Cli);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5951,7 +5951,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext
}
if (callee != null) {
// produce a FunctionCallExpr instead of an ApplyExpr(MemberSelectExpr)
var rr = new FunctionCallExpr(e.Lhs.tok, callee.Name, mse.Obj, e.tok, e.CloseParen, e.Bindings, atLabel) {
var rr = new FunctionCallExpr(e.Lhs.Tok, callee.Name, mse.Obj, e.tok, e.CloseParen, e.Bindings, atLabel) {
Function = callee,
TypeApplication_AtEnclosingClass = mse.TypeApplication_AtEnclosingClass,
TypeApplication_JustFunction = mse.TypeApplication_JustMember
Expand Down
200 changes: 113 additions & 87 deletions Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
View file

Large diffs are not rendered by default.

405 changes: 405 additions & 0 deletions Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs
View file

Large diffs are not rendered by default.

290 changes: 0 additions & 290 deletions Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,296 +13,6 @@ namespace Microsoft.Dafny;

public partial class BoogieGenerator {

void AddWellformednessCheck(Function f) {
Contract.Requires(f != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(f.EnclosingClass != null);
Contract.Requires(currentModule == null && codeContext == null && isAllocContext != null);
Contract.Ensures(currentModule == null && codeContext == null && isAllocContext != null);

Contract.Assert(InVerificationScope(f));

proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.SpecWellformedness));
currentModule = f.EnclosingClass.EnclosingModuleDefinition;
codeContext = f;

Bpl.Expr prevHeap = null;
Bpl.Expr currHeap = null;
var ordinaryEtran = new ExpressionTranslator(this, predef, f.tok, f);
ExpressionTranslator etran;
var inParams_Heap = new List<Bpl.Variable>();
if (f is TwoStateFunction) {
var prevHeapVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "previous$Heap", predef.HeapType), true);
var currHeapVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "current$Heap", predef.HeapType), true);
inParams_Heap.Add(prevHeapVar);
inParams_Heap.Add(currHeapVar);
prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar);
currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar);
etran = new ExpressionTranslator(this, predef, currHeap, prevHeap, f);
} else {
etran = ordinaryEtran;
}

// parameters of the procedure
var typeInParams = MkTyParamFormals(GetTypeParams(f), true);
var inParams = new List<Bpl.Variable>();
var outParams = new List<Bpl.Variable>();
if (!f.IsStatic) {
var th = new Bpl.IdentifierExpr(f.tok, "this", TrReceiverType(f));
Bpl.Expr wh = BplAnd(
ReceiverNotNull(th),
(f is TwoStateFunction ? etran.Old : etran).GoodRef(f.tok, th, ModuleResolver.GetReceiverType(f.tok, f)));
Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", TrReceiverType(f), wh), true);
inParams.Add(thVar);
}
foreach (Formal p in f.Ins) {
Bpl.Type varType = TrType(p.Type);
Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), varType), p.Type,
p.IsOld ? etran.Old : etran, f is TwoStateFunction ? ISALLOC : NOALLOC);
inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), varType, wh), true));
}
if (f.Result != null) {
Formal p = f.Result;
Contract.Assert(!p.IsOld);
Bpl.Type varType = TrType(p.Type);
Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), varType), p.Type, etran, NOALLOC);
outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), varType, wh), true));
}
// the procedure itself
var req = new List<Bpl.Requires>();
// free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
req.Add(Requires(f.tok, true, null, etran.HeightContext(f), null, null, null));
if (f is TwoStateFunction) {
// free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
var a0 = Bpl.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
var a1 = HeapSucc(prevHeap, currHeap);
var a2 = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, currHeap);
req.Add(Requires(f.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null));
}

foreach (var typeBoundAxiom in TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) {
req.Add(Requires(f.tok, true, null, typeBoundAxiom, null, null, null));
}

// modifies $Heap
var mod = new List<Bpl.IdentifierExpr> {
ordinaryEtran.HeapCastToIdentifierExpr,
};
// check that postconditions hold
var ens = new List<Bpl.Ensures>();
var context = new BodyTranslationContext(f.ContainsHide);
foreach (AttributedExpression ensures in f.Ens) {
var functionHeight = currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f);
var splits = new List<SplitExprInfo>();
bool splitHappened /*we actually don't care*/ = TrSplitExpr(context, ensures.E, splits, true, functionHeight, true, true, etran);
var (errorMessage, successMessage) = CustomErrorMessage(ensures.Attributes);
foreach (var s in splits) {
if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, currentModule)) {
AddEnsures(ens, EnsuresWithDependencies(s.Tok, false, ensures.E, s.E, errorMessage, successMessage, null));
}
}
}
var proc = new Bpl.Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List<Bpl.TypeVariable>(),
Concat(Concat(typeInParams, inParams_Heap), inParams), outParams,
false, req, mod, ens, etran.TrAttributes(f.Attributes, null));
AddVerboseNameAttribute(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness);
sink.AddTopLevelDeclaration(proc);

if (InsertChecksums) {
InsertChecksum(f, proc, true);
}

Contract.Assert(proc.InParams.Count == typeInParams.Count + inParams_Heap.Count + inParams.Count);
// Changed the next line to strip from inParams instead of proc.InParams
// They should be the same, but hence the added contract
var implInParams = Bpl.Formal.StripWhereClauses(inParams);
var implOutParams = Bpl.Formal.StripWhereClauses(outParams);
var locals = new List<Variable>();
var builder = new BoogieStmtListBuilder(this, options, context);
var builderInitializationArea = new BoogieStmtListBuilder(this, options, context);
builder.Add(new CommentCmd("AddWellformednessCheck for function " + f));
if (f is TwoStateFunction) {
// $Heap := current$Heap;
var heap = ordinaryEtran.HeapCastToIdentifierExpr;
builder.Add(Bpl.Cmd.SimpleAssign(f.tok, heap, etran.HeapExpr));
etran = ordinaryEtran; // we no longer need the special heap names
}
builder.AddCaptureState(f.tok, false, "initial state");

DefineFrame(f.tok, etran.ReadsFrame(f.tok), f.Reads.Expressions, builder, locals, null);
InitializeFuelConstant(f.tok, builder, etran);

var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, builder);

// Check well-formedness of any default-value expressions (before assuming preconditions).
delayer.DoWithDelayedReadsChecks(true, wfo => {
foreach (var formal in f.Ins.Where(formal => formal.DefaultValue != null)) {
var e = formal.DefaultValue;
CheckWellformed(e, wfo, locals, builder, etran.WithReadsFrame(etran.readsFrame, null)); // No frame scope for default values
builder.Add(new Bpl.AssumeCmd(e.tok, etran.CanCallAssumption(e)));
CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, e, builder);

if (formal.IsOld) {
Bpl.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true);
if (wh != null) {
var desc = new PODesc.IsAllocated("default value", "in the two-state function's previous state", e);
builder.Add(Assert(GetToken(e), wh, desc));
}
}
}
});

// Check well-formedness of the preconditions (including termination), and then
// assume each one of them. After all that (in particular, after assuming all
// of them), do the postponed reads checks.
delayer.DoWithDelayedReadsChecks(false, wfo => {
foreach (AttributedExpression p in f.Req) {
if (p.Label != null) {
p.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(p.E);
CheckWellformed(p.E, wfo, locals, builder, etran);
} else {
CheckWellformedAndAssume(p.E, wfo, locals, builder, etran, "requires clause");
}
}
});

// Check well-formedness of the reads clause. Note that this is done after assuming
// the preconditions. In other words, the well-formedness of the reads clause is
// allowed to assume the precondition (yet, the requires clause is checked to
// read only those things indicated in the reads clause).
delayer.DoWithDelayedReadsChecks(false, wfo => {
CheckFrameWellFormed(wfo, f.Reads.Expressions, locals, builder, etran);
});

// If the function is marked as {:concurrent}, check that the reads clause is empty.
if (Attributes.Contains(f.Attributes, Attributes.ConcurrentAttributeName)) {
var desc = new PODesc.ConcurrentFrameEmpty(f, "reads");
CheckFrameEmpty(f.tok, etran, etran.ReadsFrame(f.tok), builder, desc, null);
}

// check well-formedness of the decreases clauses (including termination, but no reads checks)
foreach (Expression p in f.Decreases.Expressions) {
CheckWellformed(p, new WFOptions(null, false),
locals, builder, etran);
}
// Generate:
// if (*) {
// check well-formedness of postcondition
// assume false; // don't go on to check the postconditions
// } else {
// check well-formedness of body
// // fall through to check the postconditions themselves
// }
// Here go the postconditions (termination checks included, but no reads checks)
BoogieStmtListBuilder postCheckBuilder = new BoogieStmtListBuilder(this, options, context);
// Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example)
{
var args = new List<Bpl.Expr>();
foreach (var p in GetTypeParams(f)) {
args.Add(TrTypeParameter(p));
}
if (f.IsFuelAware()) {
args.Add(etran.layerInterCluster.GetFunctionFuel(f));
}

if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) {
args.Add(GetRevealConstant(f));
}
if (f is TwoStateFunction) {
args.Add(etran.Old.HeapExpr);
}
if (f.ReadsHeap) {
args.Add(etran.HeapExpr);
}
if (!f.IsStatic) {
args.Add(new Bpl.IdentifierExpr(f.tok, etran.This));
}
foreach (var p in f.Ins) {
args.Add(new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), TrType(p.Type)));
}
Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType));
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);

var wh = GetWhereClause(f.tok, funcAppl, f.ResultType, etran, NOALLOC);
if (wh != null) {
postCheckBuilder.Add(TrAssumeCmd(f.tok, wh));
}
}
// Now for the ensures clauses
foreach (AttributedExpression p in f.Ens) {
// assume the postcondition for the benefit of checking the remaining postconditions
CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran, "ensures clause");
}
// Here goes the body (and include both termination checks and reads checks)
BoogieStmtListBuilder bodyCheckBuilder = new BoogieStmtListBuilder(this, options, context);
if (f.Body == null || !RevealedInScope(f)) {
// don't fall through to postcondition checks
bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False));
} else {
var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
var args = new List<Bpl.Expr>();
foreach (var p in GetTypeParams(f)) {
args.Add(TrTypeParameter(p));
}
if (f.IsFuelAware()) {
args.Add(etran.layerInterCluster.GetFunctionFuel(f));
}

if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) {
args.Add(GetRevealConstant(f));
}
if (f is TwoStateFunction) {
args.Add(etran.Old.HeapExpr);
}
if (f.ReadsHeap) {
args.Add(etran.HeapExpr);
}
foreach (Variable p in implInParams) {
args.Add(new Bpl.IdentifierExpr(f.tok, p));
}
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);

var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder);
bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => {
CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran, "function call result");
if (f.Result != null) {
var cmd = TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcAppl, TrVar(f.tok, f.Result)));
proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f));
bodyCheckBuilder.Add(cmd);
}
});

// Enforce 'older' conditions
var (olderParameterCount, olderCondition) = OlderCondition(f, funcAppl, implInParams);
if (olderParameterCount != 0) {
bodyCheckBuilder.Add(Assert(f.tok, olderCondition, new PODesc.IsOlderProofObligation(olderParameterCount, f.Ins.Count + (f.IsStatic ? 0 : 1))));
}
}
// Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch
postCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False));
builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok)));

var s0 = builderInitializationArea.Collect(f.tok);
var s1 = builder.Collect(f.tok);
var implBody = new StmtList(new List<BigBlock>(s0.BigBlocks.Concat(s1.BigBlocks)), f.tok);

if (EmitImplementation(f.Attributes)) {
// emit the impl only when there are proof obligations.
QKeyValue kv = etran.TrAttributes(f.Attributes, null);
var impl = AddImplementationWithAttributes(GetToken(f), proc,
Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), inParams_Heap), implInParams),
implOutParams,
locals, implBody, kv);
if (InsertChecksums) {
InsertChecksum(f, impl);
}
}

Contract.Assert(currentModule == f.EnclosingClass.EnclosingModuleDefinition);
Contract.Assert(codeContext == f);
Reset();
}

void AddFunctionAxiom(Bpl.Function boogieFunction, Function f, Expression body) {
Contract.Requires(f != null);
Contract.Requires(body != null);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ void AddFunction_Top(Function f, bool includeAllMethods) {
AddClassMember_Function(f);

if (InVerificationScope(f)) {
AddWellformednessCheck(f);
new FunctionWellformednessChecker(this).Check(f);
if (f.OverriddenFunction != null) { //it means that f is overriding its associated parent function
AddFunctionOverrideCheckImpl(f);
}
Expand Down
Loading

0 comments on commit ef1e3bc

Please sign in to comment.