Translation fixes for {:extern} when used for exports and for --test-assumptions=externs
#5939
Conversation
keyboardDrummer
added
the
run-integration-tests
keyboardDrummer
changed the title
{:extern} and --test-assumptions bugs
keyboardDrummer
changed the title
{:extern} and --test-assumptions bugs{:extern} when used for exports and for --test-assumptions=externs
There was a problem hiding this comment.
Nice use of project files for tests :)
| Type = newFunc.ResultType | ||
| }; | ||
| var resultVar = origFunc.Result ?? new Formal(tok, "#result", origFunc.ResultType, false, false, null); | ||
| var localName = origFunc.Result?.Name ?? "__BLA__result"; |
There was a problem hiding this comment.
It's an acronym for "believable left-hand-side alias", but I'll remove it since it's not well known
There was a problem hiding this comment.
Well it's known to at least one more person now, so thank you for that :)
| @@ -884,7 +884,7 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete | |||
| // We write an extern class as a base class that the actual extern class | |||
| // needs to extend, so the extern methods and functions need to be abstract | |||
| // in the base class | |||
| protected override bool IncludeExternMembers { get => true; } | |||
| protected override bool IncludeImportedMembers => true; | |||
There was a problem hiding this comment.
Consider using "ExternImported" rather than just "Imported" throughout, only because if we also start saying just "Exported" for the other direction, it will be easily confused with export sets.
There was a problem hiding this comment.
Worth a comment what's actually being tested here since it's not obvious. I think it's the fact that it previously didn't work because some extern-exported Dafny bodies were dropped.
I think you're also not actually testing the --test-assumptions fixes AFAICT? At a minimum you'd want to have a Dafny call to Builder that doesn't satisfy Pre.
| @@ -1529,15 +1529,28 @@ public void Compile(Program program, ConcreteSyntaxTree wrx) { | |||
| EmitFooter(program, wrx); | |||
| } | |||
|
|
|||
| protected (bool classIsExtern, bool included) GetIsExternAndIncluded(ClassLikeDecl cl) { | |||
|
|
|||
| public bool IsImported(IAttributeBearingDeclaration me) { | |||
There was a problem hiding this comment.
Would prefer IsExternallyImported since you made the other change, but could be changed in a future PR
| Statement callStmt; | ||
| if (origFunc.Result?.Name is null) { | ||
| var local = new LocalVariable(decl.RangeToken, localName, newFunc.ResultType, false); | ||
| local.type = newFunc.ResultType; | ||
| var locs = new List<LocalVariable> { local }; | ||
| var varDeclStmt = new VarDeclStmt(decl.RangeToken, locs, new AssignStatement(decl.RangeToken, lhss, rhss) { | ||
| ResolvedStatements = new List<Statement>() { assignStmt } | ||
| }); | ||
| localExpr.Var = local; | ||
| callStmt = varDeclStmt; | ||
| } else { | ||
| localExpr.Var = origFunc.Result; | ||
| callStmt = assignStmt; | ||
| } |
There was a problem hiding this comment.
Not completely following why this logic became unnecessary?
There was a problem hiding this comment.
Despite writing the previous code, I don't understand well either, but this was conditional on origFunc.Result == null and above I do var resultVar = origFunc.Result ?? new Formal(tok, "#result", newFunc.ResultType, false, false, null); which handles the same thing.
|
|
||
| var tok = f.ByMethodTok; | ||
| var resultVar = f.Result ?? new Formal(tok, "#result", f.ResultType, false, false, null); | ||
| // var resultVar = f.Result ?? new Formal(tok, "#result", f.ResultType, false, false, null); |
There was a problem hiding this comment.
| // var resultVar = f.Result ?? new Formal(tok, "#result", f.ResultType, false, false, null); |
| [Option("run-fails", HelpText = "Whether the running program should return a non-zero exit code")] | ||
| public bool RunShouldFail { get; set; } = false; |
There was a problem hiding this comment.
Good feature to add, but would strongly prefer --expect-exit-code instead, since we already have that option on for-each-resolver
There was a problem hiding this comment.
I can't pass in an exit code because I don't know what it will be. Dafny does not define what the exit code will be for programs that do not pass runtime contract checks. It could be different per target. All I know is that it won't be a success exit code.
I'm not inclined to let Define specify what the exit code will be for contract failures, because exit codes are not a scalable way of providing diagnostic information.
since we already have that option on for-each-resolver
That's the exit code that Dafny returns, which is also not specified AFAIK but at least it does not depend on target language runtimes. IMO this inconsistency is not confusing so we can keep it.
There was a problem hiding this comment.
Ah fair! I can live with this then.
Description
{:extern}to export members--test-assumptions=externsHow has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.