diff options
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 13 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 75 |
2 files changed, 88 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 34fa0487..c0f8ea7a 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -33,6 +33,7 @@ namespace Microsoft.Dafny public bool Compile = true;
public bool ForceCompile = false;
public bool SpillTargetCode = false;
+ public bool RuntimeChecking = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -90,6 +91,14 @@ namespace Microsoft.Dafny ps.GetNumericArgument(ref InductionHeuristic, 7);
return true;
+ case "runtimeChecking":
+ int runtimeChecking = 0; // 0 is default, no runtime checking
+ if (ps.GetNumericArgument(ref runtimeChecking, 2))
+ {
+ RuntimeChecking = runtimeChecking == 1;
+ }
+ return true;
+
default:
break;
}
@@ -148,6 +157,10 @@ namespace Microsoft.Dafny 1,2,3,4,5 - levels in between, ordered as follows as far as
how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6
6 (default) - most discriminating
+ /runtimeChecking:<n>
+ 0 (default) - ignore Dafny specifications during compilation
+ 1 - translate Dafny specifications to CodeContracts during
+ compilation for runtime checking
");
base.Usage(); // also print the Boogie options
}
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 3534dcbf..be423b46 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -23,6 +23,7 @@ namespace Microsoft.Dafny using VC;
using System.CodeDom.Compiler;
using AI = Microsoft.AbstractInterpretationFramework;
+ using Microsoft.Win32; // needed for ccrewrite
public class DafnyDriver
{
@@ -231,10 +232,33 @@ namespace Microsoft.Dafny }
cp.GenerateInMemory = false;
cp.ReferencedAssemblies.Add("System.Numerics.dll");
+ string ccrewriter = findCCRewriter();
+ bool ccrewrite = DafnyOptions.O.RuntimeChecking && ccrewriter != null;
+ if (ccrewrite)
+ {
+ cp.CompilerOptions += " /D:CONTRACTS_FULL";
+ }
var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
if (cr.Errors.Count == 0) {
Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);
+ if (ccrewrite)
+ {
+ Process p = new Process();
+ string ccrewriterOpts = "-nologo -callSiteRequires - shortBranches -throwOnFailure";
+ p.StartInfo.FileName = "cmd.exe";
+ p.StartInfo.Arguments = "/C \"\"" + ccrewriter + "\" " +
+ ccrewriterOpts + " \"" + cp.OutputAssembly + "\"\"";
+ p.StartInfo.UseShellExecute = false;
+ p.StartInfo.RedirectStandardOutput = true;
+ p.Start();
+ p.WaitForExit();
+ Console.WriteLine("Rewrote assembly into {0}", cr.PathToAssembly);
+ }
+ else if (ccrewriter == null)
+ {
+ Console.WriteLine("Error: cannot rewrite, because there is no CodeContracts rewriter");
+ }
} else {
Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);
foreach (var ce in cr.Errors) {
@@ -787,5 +811,56 @@ namespace Microsoft.Dafny return PipelineOutcome.VerificationCompleted;
}
+
+ #region Runtime checking
+
+ /********** Find Code Contracts rewriter **********/
+ private static string findCCRewriter()
+ {
+ using (RegistryKey rk = Registry.CurrentUser.OpenSubKey(@"SOFTWARE"))
+ {
+ foreach (string skN0 in rk.GetSubKeyNames())
+ if (skN0 == "Microsoft")
+ using (RegistryKey sk0 = rk.OpenSubKey(skN0))
+ {
+ foreach (string skN1 in sk0.GetSubKeyNames())
+ if (skN1 == "VisualStudio")
+ using (RegistryKey sk1 = sk0.OpenSubKey(skN1))
+ {
+ foreach (string skN2 in sk1.GetSubKeyNames())
+ using (RegistryKey sk2 = sk1.OpenSubKey(skN2))
+ {
+ foreach (string skN3 in sk2.GetSubKeyNames())
+ if (skN3 == "CodeTools")
+ using (RegistryKey sk3 = sk2.OpenSubKey(skN3))
+ {
+ foreach (string skN4 in sk3.GetSubKeyNames())
+ if (skN4 == "CodeContracts")
+ using (RegistryKey sk4 = sk3.OpenSubKey(skN4))
+ {
+ if ((string)sk4.GetValue("DisplayName") ==
+ "Microsoft Code Contracts")
+ {
+ string ccrewriter =
+ (string)sk4.GetValue("InstallDir") +
+ "Bin\\ccrewrite.exe";
+ if (File.Exists(ccrewriter))
+ return ccrewriter;
+ else
+ return null;
+ }
+ else
+ return null;
+ }
+ }
+ }
+ }
+ }
+ return null;
+ }
+ }
+
+ #endregion
+
}
}
|