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.

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

Run integration tests in single process #3715

Merged
Merged
Changes from 168 commits
Commits
Show all changes
169 commits
Select commit Hold shift + click to select a range
6ab36d7
Fix most issues in Core
keyboardDrummer Mar 1, 2023
7ccf451
Slight more core fixes
keyboardDrummer Mar 1, 2023
2833156
Resolve most errors
keyboardDrummer Mar 1, 2023
ccaaa49
Single screen of errors
keyboardDrummer Mar 1, 2023
65cdf8d
Fewer errors
keyboardDrummer Mar 1, 2023
ee34a06
Only Body and Printer errors
keyboardDrummer Mar 1, 2023
eb87fae
Simplify Method.Body
keyboardDrummer Mar 1, 2023
a3afb04
Fix lit and add comment
keyboardDrummer Mar 1, 2023
e8a1db8
Delay removing included lemma bodies
keyboardDrummer Mar 2, 2023
fa3e1fc
Small refactoring
keyboardDrummer Mar 2, 2023
69b66b6
Merge branch 'master' into removeIncludedLemmaBody
keyboardDrummer Mar 2, 2023
180fc63
Fix woops
keyboardDrummer Mar 2, 2023
1742fa1
Fixed printer errors
keyboardDrummer Mar 2, 2023
5653e00
Fix expect file
keyboardDrummer Mar 2, 2023
a63b1e5
Merge branch 'removeIncludedLemmaBody' into noStaticOptions
keyboardDrummer Mar 2, 2023
92077bc
Fixes
keyboardDrummer Mar 2, 2023
0dffe00
Fixes
keyboardDrummer Mar 2, 2023
445e414
Fix tests
keyboardDrummer Mar 2, 2023
10491b5
Run formatter
keyboardDrummer Mar 2, 2023
0637aaf
Rename
keyboardDrummer Mar 2, 2023
565506d
Merge remote-tracking branch 'origin/master' into noStaticOptions
keyboardDrummer Mar 2, 2023
8e1491d
Merge remote-tracking branch 'origin/master' into removeIncludedLemma…
keyboardDrummer Mar 2, 2023
5ebc7bd
Formatting
keyboardDrummer Mar 2, 2023
ba69454
Fix
keyboardDrummer Mar 2, 2023
8b551ca
Fix tests
keyboardDrummer Mar 2, 2023
d9d0770
Merge remote-tracking branch 'fork/removeIncludedLemmaBody' into noSt…
keyboardDrummer Mar 2, 2023
4f2d775
Ran formatter
keyboardDrummer Mar 2, 2023
7909705
Merge branch 'master' into noStaticOptions
keyboardDrummer Mar 2, 2023
7c57753
Merge remote-tracking branch 'origin/master' into noStaticOptions
keyboardDrummer Mar 7, 2023
7603f80
Merge branch 'master' into noStaticOptions
keyboardDrummer Mar 7, 2023
5609e7e
Merge remote-tracking branch 'origin/master' into noStaticOptions
keyboardDrummer Mar 8, 2023
66dcc83
Invoke integration tests directly
keyboardDrummer Mar 8, 2023
802c8ba
Fix compilation errors
keyboardDrummer Mar 8, 2023
61f3e22
Merge commit '0fa8e632f' into directIntegrationTests
keyboardDrummer Mar 8, 2023
db7d458
Merge commit '7a35c715' into directIntegrationTests
keyboardDrummer Mar 8, 2023
5971403
Some integration tests now pass
keyboardDrummer Mar 8, 2023
8d4a007
It compiles
keyboardDrummer Mar 9, 2023
ac02112
Code review
keyboardDrummer Mar 9, 2023
1287adc
Fix weirdness
keyboardDrummer Mar 9, 2023
6ca5fe0
Ran formatter
keyboardDrummer Mar 9, 2023
5162183
Fix test errors
keyboardDrummer Mar 9, 2023
307cbfa
Remove a static from test generation so that tests can run in parallel
keyboardDrummer Mar 9, 2023
f55a83f
Fix timeout issue by running some tests sequentially
keyboardDrummer Mar 9, 2023
3ebcbab
Merge branch 'master' into xunitEverywhere
keyboardDrummer Mar 9, 2023
9c931d8
Comment out entire test
keyboardDrummer Mar 9, 2023
dff76d3
Merge branch 'xunitEverywhere' of github.com:keyboardDrummer/dafny in…
keyboardDrummer Mar 9, 2023
5873f81
Run formatter
keyboardDrummer Mar 9, 2023
84154bd
Make the CompilationStatusNotificationTest class run sequentially
keyboardDrummer Mar 9, 2023
fa8fea4
Run more tests sequentailly
keyboardDrummer Mar 9, 2023
b02245e
Make more tests sequential
keyboardDrummer Mar 10, 2023
d08a5ba
Merge remote-tracking branch 'origin/master' into xunitEverywhere
keyboardDrummer Mar 10, 2023
25b50e9
Merge branch 'xunitEverywhere' into directIntegrationTests
keyboardDrummer Mar 10, 2023
4773fae
Fixes for unit tests
keyboardDrummer Mar 10, 2023
d235384
Some fixes
keyboardDrummer Mar 10, 2023
50a7043
Fixes related to redirecting stdout and stderr
keyboardDrummer Mar 10, 2023
8bcf45a
Add support for stdin
keyboardDrummer Mar 10, 2023
ff3fce3
Ran formatter
keyboardDrummer Mar 10, 2023
60cc947
Merge remote-tracking branch 'origin/master' into xunitEverywhere
keyboardDrummer Mar 10, 2023
b874a87
Merge branch 'xunitEverywhere' into directIntegrationTests
keyboardDrummer Mar 10, 2023
f577bec
Fix comp errors
keyboardDrummer Mar 10, 2023
5283366
Skip test instead of comment it out
keyboardDrummer Mar 10, 2023
cc03c41
Merge commit '5f9db2e5ab7~1' into directIntegrationTests
keyboardDrummer Mar 17, 2023
44d72ef
Merge branch 'xunitEverywhere' into directIntegrationTests
keyboardDrummer Mar 17, 2023
0f15a16
Merge commit '5f9db2e5ab7' into directIntegrationTests
keyboardDrummer Mar 17, 2023
fd48bee
Merge remote-tracking branch 'origin/master' into directIntegrationTests
keyboardDrummer Mar 17, 2023
e89d0eb
Merge branch 'master' into directIntegrationTests
keyboardDrummer Mar 17, 2023
d886039
Small improvements
keyboardDrummer Mar 17, 2023
9add5ae
Add Boogie submodule
keyboardDrummer Mar 19, 2023
0a0fca3
Merge branch 'master' into directIntegrationTests
keyboardDrummer Mar 19, 2023
a17f323
Use Boogie projects
keyboardDrummer Mar 19, 2023
e336e93
Merge branch 'directIntegrationTests' of github.com:keyboardDrummer/d…
keyboardDrummer Mar 19, 2023
16f41d9
Update configuration
keyboardDrummer Mar 19, 2023
d0228e5
submodule change
keyboardDrummer Mar 19, 2023
706e677
Merge remote-tracking branch 'origin/master' into directIntegrationTests
keyboardDrummer Mar 27, 2023
c80fcf6
Checkout submodules
keyboardDrummer Mar 27, 2023
e53b0b9
Enable submodules for integration tests reusable
keyboardDrummer Mar 27, 2023
42f4e6a
Update to new Boogie and API
keyboardDrummer Mar 28, 2023
9013d76
Use newer gradle
keyboardDrummer Mar 28, 2023
553812f
Merge remote-tracking branch 'origin/master' into directIntegrationTests
keyboardDrummer Mar 28, 2023
0c8e7b0
Directly call multi back-end testing code, fix JustRun.dfy
keyboardDrummer Mar 31, 2023
4002bc1
Directly call multi back-end testing code, fix JustRun.dfy
keyboardDrummer Mar 31, 2023
d69a74d
Get UnicodeStrings.dfy to pass
keyboardDrummer Apr 3, 2023
82e5e01
Fix CSharpBackend running
keyboardDrummer Apr 3, 2023
96978ad
Add errorWriter in more places
keyboardDrummer Apr 3, 2023
f730b8d
Fix various issues
keyboardDrummer Apr 3, 2023
2782fe0
Fix various issues
keyboardDrummer Apr 3, 2023
684d018
Merge branch 'directIntegrationTests' of github.com:keyboardDrummer/d…
keyboardDrummer Apr 3, 2023
df1a020
Merge remote-tracking branch 'origin/master' into directIntegrationTests
keyboardDrummer Apr 3, 2023
cbb5bdd
Fix comp issue
keyboardDrummer Apr 3, 2023
866be4e
Move DafnyFile to separate file
keyboardDrummer Apr 4, 2023
5e2f2e5
Rename Main to DafnyMain
keyboardDrummer Apr 4, 2023
8e6479c
Stack size related changes
keyboardDrummer Apr 4, 2023
9e526cc
Various fixes
keyboardDrummer Apr 4, 2023
b1d3e10
Trigger CI
keyboardDrummer Apr 4, 2023
e1c0847
Fix Boogie
keyboardDrummer Apr 4, 2023
bb5e9cd
Fix Dafny server counterexample file collision
keyboardDrummer Apr 4, 2023
cd5c5d8
Add missing token assignment
keyboardDrummer Apr 4, 2023
8ea20a5
Merge branch 'master' into directIntegrationTests
keyboardDrummer Apr 4, 2023
b7cdc6c
Cleanup
keyboardDrummer Apr 4, 2023
2492683
Ran formatter
keyboardDrummer Apr 4, 2023
9ff2c68
Fix for Python compiler when else statement contain only a havoc assi…
keyboardDrummer Apr 5, 2023
bd1b180
Cleanup
keyboardDrummer Apr 5, 2023
57bb88a
Merge remote-tracking branch 'fork/elseWithHavocPythonFix' into direc…
keyboardDrummer Apr 5, 2023
ba286ab
Remove usage of Console.Error
keyboardDrummer Apr 5, 2023
9b2f493
Merge branch 'directIntegrationTests' of github.com:keyboardDrummer/d…
keyboardDrummer Apr 5, 2023
1d9a8cf
Trigger CI
keyboardDrummer Apr 5, 2023
687ff00
Merge branch 'master' into elseWithHavocPythonFix
keyboardDrummer Apr 5, 2023
25afde7
Change lit integration writer creation
keyboardDrummer Apr 5, 2023
d0b5846
Remove unsafe usage of MainMethodLitCommand
keyboardDrummer Apr 5, 2023
5ec91ca
Merge branch 'master' into directIntegrationTests
keyboardDrummer Apr 5, 2023
e467696
Trigger CI
keyboardDrummer Apr 5, 2023
fa40552
Merge branch 'directIntegrationTests' of github.com:keyboardDrummer/d…
keyboardDrummer Apr 5, 2023
16a46eb
Fix warning
keyboardDrummer Apr 5, 2023
71a544e
Ran formatter
keyboardDrummer Apr 5, 2023
28e1a08
Fix 1553 test
keyboardDrummer Apr 6, 2023
9b3db67
Add UndisposableTextWriter
keyboardDrummer Apr 6, 2023
7185abf
Fix problems
keyboardDrummer Apr 6, 2023
64ed99b
Remove obsolete RUN command
keyboardDrummer Apr 6, 2023
dd2b82d
Stop creating large stacks after initialization
keyboardDrummer Apr 6, 2023
8ce63f7
Trigger CI
keyboardDrummer Apr 6, 2023
c683d6a
Synchronise writers to see if that prevents crashes
keyboardDrummer Apr 6, 2023
9bab7d0
Use indirect invocation so CI can pass
keyboardDrummer Apr 7, 2023
714861b
Merge remote-tracking branch 'origin' into directIntegrationTests
keyboardDrummer Apr 7, 2023
d0fc2cf
Merge fix
keyboardDrummer Apr 7, 2023
4a16b5c
Move test files
keyboardDrummer Apr 7, 2023
c0c29b1
Move some more files to new Test/statements folder
keyboardDrummer Apr 7, 2023
becad02
Merge branch 'master' into elseWithHavocPythonFix
keyboardDrummer Apr 7, 2023
f62941d
Test fixes
keyboardDrummer Apr 7, 2023
8f05f36
Fix test
keyboardDrummer Apr 7, 2023
1a790e2
Move tests
keyboardDrummer Apr 10, 2023
697607e
Revert "Use Boogie projects"
keyboardDrummer Apr 10, 2023
47f95ec
Remove Boogie submodule
keyboardDrummer Apr 10, 2023
539d6c9
Update to Boogie 2.16.5
keyboardDrummer Apr 10, 2023
57a463f
Ran formatter
keyboardDrummer Apr 10, 2023
625a6f0
Revert solution file
keyboardDrummer Apr 11, 2023
1221526
Small changes
keyboardDrummer Apr 11, 2023
b5c9e48
Merge remote-tracking branch 'fork/elseWithHavocPythonFix' into direc…
keyboardDrummer Apr 11, 2023
fc8eb97
Merge commit 'f4836e93e' into directIntegrationTests
keyboardDrummer Apr 11, 2023
591ba60
Code review
keyboardDrummer Apr 11, 2023
3dc4e8a
Fix build
keyboardDrummer Apr 11, 2023
35ce43f
Fix customBoogie patch
keyboardDrummer Apr 13, 2023
bcb33cd
Merge remote-tracking branch 'origin/master' into directIntegrationTests
keyboardDrummer May 2, 2023
744587f
Ran formatter
keyboardDrummer May 2, 2023
0b1e844
Merge branch 'master' into directIntegrationTests
keyboardDrummer May 2, 2023
89f98ef
Turn off running with the lib backend since it doesn't work
keyboardDrummer May 5, 2023
7fe9e59
Update libraries to latest master
keyboardDrummer May 5, 2023
55d37fc
Cleanup
keyboardDrummer May 5, 2023
d2957ac
Merge branch 'master' into directIntegrationTests
keyboardDrummer May 5, 2023
09fe703
Add error writer support
keyboardDrummer May 5, 2023
78f9259
Merge branch 'directIntegrationTests' of github.com:keyboardDrummer/d…
keyboardDrummer May 5, 2023
21e2ffd
Fix 3883 test
keyboardDrummer May 5, 2023
513f374
Fix comp errors
keyboardDrummer May 7, 2023
289a6df
Fix expect file
keyboardDrummer May 8, 2023
324564d
Remove ByMethodTok assignment from test gen code
keyboardDrummer May 8, 2023
6fff097
Merge branch 'master' into directIntegrationTests
keyboardDrummer May 8, 2023
2355a05
Trigger CI
keyboardDrummer May 8, 2023
fde4b5e
Merge branch 'directIntegrationTests' of github.com:keyboardDrummer/d…
keyboardDrummer May 8, 2023
61dd21d
Fix formatting
keyboardDrummer May 8, 2023
e4632c2
Remove test project to test project references
keyboardDrummer May 8, 2023
bb66297
Fix warning
keyboardDrummer May 8, 2023
8448af8
Merge branch 'master' into directIntegrationTests
keyboardDrummer May 8, 2023
514cd02
Fix warnings
keyboardDrummer May 8, 2023
e4d39e7
Merge branch 'directIntegrationTests' of github.com:keyboardDrummer/d…
keyboardDrummer May 8, 2023
bb50259
Merge remote-tracking branch 'origin/master' into directIntegrationTests
keyboardDrummer May 9, 2023
79f4d68
Cleanup and format
keyboardDrummer May 9, 2023
20a84e3
Resolve warnings
keyboardDrummer May 9, 2023
9cf986d
Cleanup and csproj file remove unneeded reference
keyboardDrummer May 9, 2023
1948a8d
Merge branch 'master' into directIntegrationTests
keyboardDrummer May 9, 2023
31591ac
Merge remote-tracking branch 'origin/master' into directIntegrationTests
keyboardDrummer May 11, 2023
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
2 changes: 1 addition & 1 deletion .github/workflows/check-deep-tests-reusable.yml
Original file line number Diff line number Diff line change
@@ -16,7 +16,7 @@ jobs:
uses: actions/checkout@v3
with:
path: dafny
submodules: true
submodules: recursive
- uses: actions/github-script@v6
if: github.repository_owner == 'dafny-lang'
with:
1 change: 1 addition & 0 deletions .github/workflows/deep-tests.yml
Original file line number Diff line number Diff line change
@@ -32,6 +32,7 @@ jobs:
uses: actions/checkout@v3
with:
ref: ${{ inputs.sha }}
submodules: recursive

- name: Get short sha
run: echo "sha_short=`git rev-parse --short HEAD`" >> $GITHUB_ENV
2 changes: 1 addition & 1 deletion .github/workflows/integration-tests-reusable.yml
Original file line number Diff line number Diff line change
@@ -98,7 +98,7 @@ jobs:
uses: actions/checkout@v3
with:
path: dafny
submodules: false # Until the libraries work again
submodules: true # Until the libraries work again
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AFAICT a lot of the test failures are due to not using a recent commit from the libraries repo, if you update that pointer it should fix them (because we updated that code to work with Dafny 4)

# - name: Clean up libraries for testing
# run: |
# rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override
2 changes: 2 additions & 0 deletions .github/workflows/msbuild.yml
Original file line number Diff line number Diff line change
@@ -32,6 +32,7 @@ jobs:
uses: actions/checkout@v3
with:
path: dafny
submodules: recursive
- name: Restore tools
working-directory: dafny
run: dotnet tool restore
@@ -86,6 +87,7 @@ jobs:
uses: actions/checkout@v3
with:
path: dafny
submodules: recursive

- name: Setup dotnet
uses: actions/setup-dotnet@v3
2 changes: 2 additions & 0 deletions .github/workflows/runtime-tests.yml
Original file line number Diff line number Diff line change
@@ -24,6 +24,8 @@ jobs:
steps:
- name: Checkout Dafny
uses: actions/checkout@v3
with:
submodules: true
- name: Set up JDK 18
uses: actions/setup-java@v3
with:
8 changes: 4 additions & 4 deletions Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs
Original file line number Diff line number Diff line change
@@ -26,7 +26,7 @@ public override Expression CloneExpr(Expression expr) {
var e = (FunctionCallExpr)expr;
#if DEBUG_PRINT
if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) {
Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e));
Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e));
}
#endif
// Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix.
@@ -37,7 +37,7 @@ public override Expression CloneExpr(Expression expr) {
if (f != null && focalPredicates.Contains(f)) {
#if DEBUG_PRINT
var r = CloneCallAndAddK(e);
Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r));
Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r));
return r;
#else
return CloneCallAndAddK(e);
@@ -58,14 +58,14 @@ public override Expression CloneExpr(Expression expr) {
if (fce != null) {
#if DEBUG_PRINT
if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) {
Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce));
Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce));
}
#endif
var f = fce.Function as ExtremePredicate;
if (f != null && focalPredicates.Contains(f)) {
#if DEBUG_PRINT
var r = CloneCallAndAddK(fce);
Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r));
Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r));
return r;
#else
return CloneCallAndAddK(fce);
4 changes: 4 additions & 0 deletions Source/DafnyCore/AST/Grammar/Printer.cs
Original file line number Diff line number Diff line change
@@ -194,6 +194,10 @@ public static string ToStringWithoutNewline(System.IO.StringWriter wr) {
return sb.ToString(0, len);
}

public void PrintProgramLargeStack(Program prog, bool afterResolver) {
DafnyMain.LargeStackFactory.StartNew(() => PrintProgram(prog, afterResolver)).Wait();
}

public void PrintProgram(Program prog, bool afterResolver) {
Contract.Requires(prog != null);
this.afterResolver = afterResolver;
4 changes: 2 additions & 2 deletions Source/DafnyCore/AST/Types/Types.cs
Original file line number Diff line number Diff line change
@@ -1285,7 +1285,7 @@ public static Type Join(Type a, Type b, BuiltIns builtIns) {
Contract.Requires(builtIns != null);
var j = JoinX(a, b, builtIns);
if (builtIns.Options.Get(CommonOptionBag.TypeInferenceDebug)) {
Console.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j);
builtIns.Options.OutputWriter.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j);
}
return j;
}
@@ -1506,7 +1506,7 @@ public static Type Meet(Type a, Type b, BuiltIns builtIns) {
}
}
if (builtIns.Options.Get(CommonOptionBag.TypeInferenceDebug)) {
Console.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j);
builtIns.Options.OutputWriter.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j);
}
return j;
}
2 changes: 1 addition & 1 deletion Source/DafnyCore/Auditor/Auditor.cs
Original file line number Diff line number Diff line change
@@ -137,7 +137,7 @@ internal override void PostResolve(Program program) {
_ => $"Internal error: unknown format {reportFormat}"
};
if (reportFileName is null) {
Console.Write(text);
Options.OutputWriter.Write(text);
} else {
if (compareReport) {
try {
2 changes: 1 addition & 1 deletion Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
Original file line number Diff line number Diff line change
@@ -110,7 +110,7 @@ void EmitDafnySourceAttribute(Program program, ConcreteSyntaxTree wr) {
stringWriter.NewLine = Environment.NewLine;
var oldValue = Options.ShowEnv;
Options.ShowEnv = ExecutionEngineOptions.ShowEnvironment.DuringPrint;
new Printer(stringWriter, Options, PrintModes.Serialization).PrintProgram(program, true);
new Printer(stringWriter, Options, PrintModes.Serialization).PrintProgramLargeStack(program, true);
Options.ShowEnv = oldValue;
var programString = stringWriter.GetStringBuilder().Replace("\"", "\"\"").ToString();

101 changes: 37 additions & 64 deletions Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs
Original file line number Diff line number Diff line change
@@ -5,6 +5,7 @@
using System.Linq;
using System.Reflection;
using System.Runtime.Loader;
using System.Text;
using System.Text.Json;
using Microsoft.CodeAnalysis;
using Microsoft.CodeAnalysis.CSharp;
@@ -44,7 +45,6 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location),
MetadataReference.CreateFromFile(Assembly.Load("mscorlib").Location));

var inMemory = runAfterCompile;
compilation = compilation.WithOptions(compilation.Options.WithOutputKind(callToMain != null ? OutputKind.ConsoleApplication : OutputKind.DynamicallyLinkedLibrary));

var tempCompilationResult = new CSharpCompilationResult();
@@ -93,54 +93,40 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
var outputDir = targetFilename == null ? Directory.GetCurrentDirectory() : Path.GetDirectoryName(Path.GetFullPath(targetFilename));
var outputPath = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".dll");
var outputJson = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".runtimeconfig.json");
if (inMemory) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might be worth mentioning this change of behavior in a release note (that C# always emits source code now). I can't find any note of it in documentation, and I do like making this more consistent with the other backends, but it could be surprising to some customers that have been using Dafny for a long time.

using var stream = new MemoryStream();
var emitResult = compilation.Emit(stream);
if (emitResult.Success) {
tempCompilationResult.CompiledAssembly = Assembly.Load(stream.GetBuffer());
} else {
outputWriter.WriteLine("Errors compiling program:");
var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
foreach (var ce in errors) {
outputWriter.WriteLine(ce.ToString());
outputWriter.WriteLine();
}
return false;
var emitResult = compilation.Emit(outputPath);

if (emitResult.Success) {
tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath);
if (Options.CompileVerbose) {
outputWriter.WriteLine("Compiled assembly into {0}.dll", compilation.AssemblyName);
}
} else {
var emitResult = compilation.Emit(outputPath);

if (emitResult.Success) {
tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath);
if (Options.CompileVerbose) {
outputWriter.WriteLine("Compiled assembly into {0}.dll", compilation.AssemblyName);
}
try {
var configuration = JsonSerializer.Serialize(
new {
runtimeOptions = new {
tfm = "net6.0",
framework = new {
name = "Microsoft.NETCore.App",
version = "6.0.0",
rollForward = "LatestMinor"
}
try {
var configuration = JsonSerializer.Serialize(
new {
runtimeOptions = new {
tfm = "net6.0",
framework = new {
name = "Microsoft.NETCore.App",
version = "6.0.0",
rollForward = "LatestMinor"
}
}, new JsonSerializerOptions() { WriteIndented = true });
File.WriteAllText(outputJson, configuration + Environment.NewLine);
} catch (Exception e) {
outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}");
return false;
}
} else {
outputWriter.WriteLine("Errors compiling program into {0}", compilation.AssemblyName);
var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
foreach (var ce in errors) {
outputWriter.WriteLine(ce.ToString());
outputWriter.WriteLine();
}
}
}, new JsonSerializerOptions() { WriteIndented = true });
File.WriteAllText(outputJson, configuration + Environment.NewLine);
} catch (Exception e) {
outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}");
return false;
}
} else {
outputWriter.WriteLine("Errors compiling program into {0}", compilation.AssemblyName);
var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
foreach (var ce in errors) {
outputWriter.WriteLine(ce.ToString());
outputWriter.WriteLine();
}

return false;
}

compilationResult = tempCompilationResult;
@@ -151,37 +137,24 @@ private class CSharpCompilationResult {
public Assembly CompiledAssembly;
}

public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string/*?*/ targetFilename, ReadOnlyCollection<string> otherFileNames,
object compilationResult, TextWriter outputWriter) {
public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain,
string targetFilename /*?*/, ReadOnlyCollection<string> otherFileNames,
object compilationResult, TextWriter outputWriter, TextWriter errorWriter) {

var crx = (CSharpCompilationResult)compilationResult;

foreach (var otherFileName in otherFileNames) {
if (Path.GetExtension(otherFileName) == ".dll") {
AssemblyLoadContext.Default.LoadFromAssemblyPath(Path.GetFullPath(otherFileName));
var targetDirectory = Path.GetDirectoryName(crx.CompiledAssembly.Location);
File.Copy(otherFileName, Path.Combine(targetDirectory!, Path.GetFileName(otherFileName)), true);
}
}

if (crx.CompiledAssembly == null) {
throw new Exception("Cannot call run target program on a compilation that failed");
}
var entry = crx.CompiledAssembly.EntryPoint;
if (entry == null) {
throw new Exception("Cannot call run target on a compilation whose assembly has no entry.");
}
try {
Console.OutputEncoding = System.Text.Encoding.UTF8; // Force UTF-8 output in dafny run (#2999)
object[] parameters = entry.GetParameters().Length == 0 ? new object[] { } : new object[] { Options.MainArgs.ToArray() };
entry.Invoke(null, parameters);
return true;
} catch (System.Reflection.TargetInvocationException e) {
outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message);
outputWriter.WriteLine(e.InnerException.ToString());
} catch (System.Exception e) {
outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message);
outputWriter.WriteLine(e.ToString());
}
return false;
var psi = PrepareProcessStartInfo("dotnet", new[] { crx.CompiledAssembly.Location }.Concat(Options.MainArgs));
return RunProcess(psi, outputWriter, errorWriter) == 0;
}

public CsharpBackend(DafnyOptions options) : base(options) {
4 changes: 2 additions & 2 deletions Source/DafnyCore/Compilers/CoverageInstrumenter.cs
Original file line number Diff line number Diff line change
@@ -72,7 +72,7 @@ public void WriteLegendFile() {
if (legend != null) {
var filename = compiler.Options.CoverageLegendFile;
Contract.Assert(filename != null);
TextWriter wr = filename == "-" ? System.Console.Out : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create));
TextWriter wr = filename == "-" ? compiler.Options.OutputWriter : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create));
{
for (var i = 0; i < legend.Count; i++) {
var e = legend[i];
@@ -82,4 +82,4 @@ public void WriteLegendFile() {
legend = null;
}
}
}
}
2 changes: 1 addition & 1 deletion Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
Original file line number Diff line number Diff line change
@@ -905,7 +905,7 @@ protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) {
}

protected void Warn(string msg, IToken tok) {
Console.Error.WriteLine("WARNING: {3} ({0}:{1}:{2})", tok.Filepath, tok.line, tok.col, msg);
Options.ErrorWriter.WriteLine("WARNING: {3} ({0}:{1}:{2})", tok.Filepath, tok.line, tok.col, msg);
}

// Because we use reference counting (via shared_ptr), the TypeName of a class differs
11 changes: 6 additions & 5 deletions Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs
Original file line number Diff line number Diff line change
@@ -19,7 +19,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
bool runAfterCompile, TextWriter outputWriter, out object compilationResult) {
var assemblyLocation = System.Reflection.Assembly.GetExecutingAssembly().Location;
Contract.Assert(assemblyLocation != null);
var codebase = System.IO.Path.GetDirectoryName(assemblyLocation);
var codebase = Path.GetDirectoryName(assemblyLocation);
Contract.Assert(codebase != null);
compilationResult = null;
var psi = PrepareProcessStartInfo("g++", new List<string> {
@@ -37,13 +37,14 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
"-o", ComputeExeName(targetFilename),
targetFilename
});
return 0 == RunProcess(psi, outputWriter, "Error while compiling C++ files.");
return 0 == RunProcess(psi, outputWriter, outputWriter, "Error while compiling C++ files.");
}

public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection<string> otherFileNames,
object compilationResult, TextWriter outputWriter) {
public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain /*?*/,
string targetFilename, ReadOnlyCollection<string> otherFileNames,
object compilationResult, TextWriter outputWriter, TextWriter errorWriter) {
var psi = PrepareProcessStartInfo(ComputeExeName(targetFilename), Options.MainArgs);
return 0 == RunProcess(psi, outputWriter);
return 0 == RunProcess(psi, outputWriter, errorWriter);
}

public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { ".h" };
9 changes: 5 additions & 4 deletions Source/DafnyCore/Compilers/Dafny/DafnyBackend.cs
Original file line number Diff line number Diff line change
@@ -41,13 +41,14 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
* The Dafny backend is different from the other backends in that the output code needs to be compiled
* by the Dafny compiler itself to another backend for execution.
*/
public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain,
string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, /*?*/
string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter,
TextWriter errorWriter) {
Contract.Requires(targetFilename != null || otherFileNames.Count == 0);

return RunTargetDafnyProgram(targetFilename, outputWriter, false);
return RunTargetDafnyProgram(targetFilename, outputWriter, errorWriter, false);
}

public DafnyBackend(DafnyOptions options) : base(options) {
}
}
}
Loading