diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index 5e2a19351..d0d472ff5 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -55,12 +55,11 @@ public enum VerbosityLevel uint ResourceLimit { get; } bool DoModSetAnalysis { get; } bool DebugStagedHoudini { get; } + int LoopUnrollCount { get; } bool DeterministicExtractLoops { get; } string VariableDependenceIgnore { get; } bool PruneInfeasibleEdges { get; } bool ModifyTopologicalSorting { get; } - bool ExtractLoopsUnrollIrreducible { get; } - int RecursionBound { get; } int InlineDepth { get; } bool TraceTimes { get; } bool FreeVarLambdaLifting { get; } diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index ec04e7144..171797990 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -544,11 +544,6 @@ public bool PrintInlined { // disable model generation, used by Corral/SI public bool StratifiedInliningWithoutModels { get; set; } - // Sets the recursion bound, used for loop extraction, etc. - public int RecursionBound { get; set; } = 500; - - public bool ExtractLoopsUnrollIrreducible { get; set; } = true; // unroll irreducible loops? (set programmatically) - public CoreOptions.TypeEncoding TypeEncodingMethod { get; set; } = CoreOptions.TypeEncoding.Monomorphic; public bool ReflectAdd { get; set; } = false; @@ -1118,13 +1113,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps) } return true; - case "recursionBound": - if (ps.ConfirmArgumentCount(1)) - { - RecursionBound = Int32.Parse(cce.NonNull(args[ps.i])); - } - return true; case "enableUnSatCoreExtraction": if (ps.ConfirmArgumentCount(1)) { @@ -1806,6 +1795,10 @@ checking errors /loopUnroll: unroll loops, following up to n back edges (and then some) + default is -1, which means loops are not unrolled + /extractLoops + extract reducible loops into recursive procedures and + inline irreducible loops using the bound supplied by /loopUnroll: /soundLoopUnrolling sound loop unrolling /doModSetAnalysis diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index d6b2b3a24..576020815 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1118,10 +1118,6 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, if (msgIfVerifies != null) { tw.WriteLine(msgIfVerifies); } - - break; - case VcOutcome.ReachedBound: - tw.WriteLine($"Stratified Inlining: Reached recursion bound of {options.RecursionBound}"); break; case VcOutcome.Errors: case VcOutcome.TimedOut: @@ -1166,28 +1162,24 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, } } } - break; case VcOutcome.OutOfResource: if (implName != null && implTok != null) { string msg = "Verification out of resource (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); } - break; case VcOutcome.OutOfMemory: if (implName != null && implTok != null) { string msg = "Verification out of memory (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); } - break; case VcOutcome.SolverException: if (implName != null && implTok != null) { string msg = "Verification encountered solver exception (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); } - break; case VcOutcome.Inconclusive: @@ -1195,7 +1187,6 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options, string msg = "Verification inconclusive (" + implName + ")"; errorInfo = ErrorInformation.Create(implTok, msg); } - break; } @@ -1211,9 +1202,6 @@ private static string OutcomeIndication(VcOutcome vcOutcome, List !e.IsAuxiliaryCexForDiagnosingTimeouts); Interlocked.Add(ref stats.ErrorCount, cnt); - break; } } @@ -1295,38 +1272,27 @@ private static void UpdateCachedStatistics(PipelineStatistics stats, VcOutcome v default: Contract.Assert(false); // unexpected outcome throw new cce.UnreachableException(); - case VcOutcome.ReachedBound: - Interlocked.Increment(ref stats.CachedVerifiedCount); - - break; case VcOutcome.Correct: Interlocked.Increment(ref stats.CachedVerifiedCount); - break; case VcOutcome.TimedOut: Interlocked.Increment(ref stats.CachedTimeoutCount); - break; case VcOutcome.OutOfResource: Interlocked.Increment(ref stats.CachedOutOfResourceCount); - break; case VcOutcome.OutOfMemory: Interlocked.Increment(ref stats.CachedOutOfMemoryCount); - break; case VcOutcome.SolverException: Interlocked.Increment(ref stats.CachedSolverExceptionCount); - break; case VcOutcome.Inconclusive: Interlocked.Increment(ref stats.CachedInconclusiveCount); - break; case VcOutcome.Errors: int cnt = errors.Count(e => !e.IsAuxiliaryCexForDiagnosingTimeouts); Interlocked.Add(ref stats.CachedErrorCount, cnt); - break; } } diff --git a/Source/ExecutionEngine/ExecutionEngineOptions.cs b/Source/ExecutionEngine/ExecutionEngineOptions.cs index d18eda87e..f7e4806df 100644 --- a/Source/ExecutionEngine/ExecutionEngineOptions.cs +++ b/Source/ExecutionEngine/ExecutionEngineOptions.cs @@ -38,7 +38,6 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions bool ExpandLambdas { get; } bool PrintLambdaLifting { get; } bool UseAbstractInterpretation { get; } - int LoopUnrollCount { get; } bool SoundLoopUnrolling { get; } bool Verify { get; } bool ContractInfer { get; } diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs index ce2cea26d..c653223e6 100644 --- a/Source/Houdini/StagedHoudini.cs +++ b/Source/Houdini/StagedHoudini.cs @@ -339,17 +339,6 @@ private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2) return o1; } - // Neither outcome is correct, so if one outcome is ReachedBound, return the other in case it is "worse" - if (vcOutcome1 == VcOutcome.ReachedBound) - { - return o2; - } - - if (vcOutcome2 == VcOutcome.ReachedBound) - { - return o1; - } - // Both outcomes must be timeout or memout; arbitrarily choose the first return o1; } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 44eec8d9b..a69166cb7 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1617,7 +1617,6 @@ public enum VcOutcome OutOfResource, OutOfMemory, Inconclusive, - ReachedBound, SolverException } diff --git a/Source/VCGeneration/LoopExtractor.cs b/Source/VCGeneration/LoopExtractor.cs index 3fdf987e3..be25d0ae5 100644 --- a/Source/VCGeneration/LoopExtractor.cs +++ b/Source/VCGeneration/LoopExtractor.cs @@ -34,40 +34,42 @@ public static (Dictionary> loops, HashSet(); - foreach (var blk in impl.Blocks) - { - origBlocks.Add(blk.Label, blk); - } + // statically unroll loops in this procedure - // unroll - Block start = impl.Blocks[0]; - impl.Blocks = LoopUnroll.UnrollLoops(start, options.RecursionBound, false); + // First, build a map of the current blocks + var origBlocks = new Dictionary(); + foreach (var blk in impl.Blocks) + { + origBlocks.Add(blk.Label, blk); + } - // Now construct the "map back" information - // Resulting block label -> original block - var blockMap = new Dictionary(); - foreach (var blk in impl.Blocks) + // unroll + Block start = impl.Blocks[0]; + impl.Blocks = LoopUnroll.UnrollLoops(start, options.LoopUnrollCount, false); + + // Now construct the "map back" information + // Resulting block label -> original block + var blockMap = new Dictionary(); + foreach (var blk in impl.Blocks) + { + var sl = LoopUnroll.sanitizeLabel(blk.Label); + if (sl == blk.Label) { - var sl = LoopUnroll.sanitizeLabel(blk.Label); - if (sl == blk.Label) - { - blockMap.Add(blk.Label, blk); - } - else - { - Contract.Assert(origBlocks.ContainsKey(sl)); - blockMap.Add(blk.Label, origBlocks[sl]); - } + blockMap.Add(blk.Label, blk); + } + else + { + Contract.Assert(origBlocks.ContainsKey(sl)); + blockMap.Add(blk.Label, origBlocks[sl]); } - - fullMap[impl.Name] = blockMap; } + + fullMap[impl.Name] = blockMap; } } }