diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-10-27 14:30:43 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-10-27 14:30:43 -0700 |
| commit | c4333fa28b0ebd00e4b159dcafe87fc2a0264c59 (patch) | |
| tree | 2dcc3a50619bd9bb33a06e0eeaad6e837a4249fb /Source/Dafny/Rewriter.cs | |
| parent | 7f1c0547467e5752d8832961f803dfdcf2a8a2f2 (diff) | |
Added an attribute :timeLimitMultiplier for setting relative time outs.
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 56e28047..9db7a0ec 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -988,6 +988,54 @@ namespace Microsoft.Dafny return reqs;
}
}
+
+
+
+ /// <summary>
+ /// Replace all occurrences of attribute {:timeLimitMultiplier X} with {:timeLimit Y}
+ /// where Y = X*default-time-limit or Y = X*command-line-time-limit
+ /// </summary>
+ public class TimeLimitRewriter : IRewriter
+ {
+ public void PreResolve(ModuleDefinition m) {
+ foreach (var d in m.TopLevelDecls) {
+ if (d is ClassDecl) {
+ var c = (ClassDecl)d;
+ foreach (MemberDecl member in c.Members) {
+ if (member is Function || member is Method) {
+ // Check for the timeLimitMultiplier attribute
+ if (Attributes.Contains(member.Attributes, "timeLimitMultiplier")) {
+ Attributes attrs = member.Attributes;
+ for (; attrs != null; attrs = attrs.Prev) {
+ if (attrs.Name == "timeLimitMultiplier") {
+ if (attrs.Args.Count == 1 && attrs.Args[0] is LiteralExpr) {
+ var arg = attrs.Args[0] as LiteralExpr;
+ System.Numerics.BigInteger value = (System.Numerics.BigInteger)arg.Value;
+ if (value.Sign > 0) {
+ int current_limit = DafnyOptions.O.ProverKillTime > 0 ? DafnyOptions.O.ProverKillTime : 10; // Default to 10 seconds
+ attrs.Args[0] = new LiteralExpr(attrs.Args[0].tok, value * current_limit);
+ attrs.Name = "timeLimit";
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ public void PostResolve(ModuleDefinition m)
+ {
+ // Nothing to do here
+ }
+
+ public void PostCyclicityResolve(ModuleDefinition m) {
+ // Nothing to do here
+ }
+
+ }
}
|