diff --git a/Source/Core/Analysis/ModSetCollector.cs b/Source/Core/Analysis/ModSetCollector.cs index ecf440d84..42f0dd09b 100644 --- a/Source/Core/Analysis/ModSetCollector.cs +++ b/Source/Core/Analysis/ModSetCollector.cs @@ -26,7 +26,7 @@ public ModSetCollector(CoreOptions options) private bool moreProcessingRequired; - public void DoModSetAnalysis(Program program) + public void CollectModifies(Program program) { Contract.Requires(program != null); var implementedProcs = new HashSet(); @@ -66,8 +66,11 @@ public void DoModSetAnalysis(Program program) foreach (Procedure x in modSets.Keys) { - x.Modifies = new List(); - foreach (Variable v in modSets[x]) + if (x.Modifies == null) + { + x.Modifies = new List(); + } + foreach (Variable v in modSets[x].Except(x.Modifies.Select(y => y.Decl))) { x.Modifies.Add(new IdentifierExpr(v.tok, v)); } diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index d62bac5a3..075ed432d 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -55,7 +55,7 @@ public enum VerbosityLevel bool OverlookBoogieTypeErrors { get; } uint TimeLimit { get; } uint ResourceLimit { get; } - bool DoModSetAnalysis { get; set; } + bool InferModifies { get; set; } bool DebugStagedHoudini { get; } int LoopUnrollCount { get; } bool DeterministicExtractLoops { get; } diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index eb08f21a9..88d21e2cc 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -751,7 +751,7 @@ public class TypecheckingContext : CheckingContext public LayerRange ExpectedLayerRange; public bool GlobalAccessOnlyInOld; public int InsideOld; - public bool CheckModifies => Proc != null && (!Options?.DoModSetAnalysis ?? true); + public bool CheckModifies => Proc != null && (!Options?.InferModifies ?? true); public TypecheckingContext(IErrorSink errorSink, CoreOptions options) : base(errorSink) diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 067e476ac..7f2d0bd26 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -416,9 +416,9 @@ public bool SIBoolControlVC { public bool ExpandLambdas { get; set; } = true; // not useful from command line, only to be set to false programatically - public bool DoModSetAnalysis { - get => doModSetAnalysis; - set => doModSetAnalysis = value; + public bool InferModifies { + get => inferModifies; + set => inferModifies = value; } public bool UseAbstractInterpretation { get; set; } @@ -576,7 +576,7 @@ void ObjectInvariant5() private bool proverHelpRequested = false; private bool restartProverPerVc = false; private bool useArrayAxioms = false; - private bool doModSetAnalysis = false; + private bool inferModifies = false; private bool runDiagnosticsOnTimeout = false; private bool traceDiagnosticsOnTimeout = false; private bool siBoolControlVc = false; @@ -1362,7 +1362,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("reflectAdd", x => ReflectAdd = x) || ps.CheckBooleanFlag("useArrayAxioms", x => useArrayAxioms = x) || ps.CheckBooleanFlag("relaxFocus", x => RelaxFocus = x) || - ps.CheckBooleanFlag("doModSetAnalysis", x => doModSetAnalysis = x) || + ps.CheckBooleanFlag("inferModifies", x => inferModifies = x) || ps.CheckBooleanFlag("runDiagnosticsOnTimeout", x => runDiagnosticsOnTimeout = x) || ps.CheckBooleanFlag("traceDiagnosticsOnTimeout", x => traceDiagnosticsOnTimeout = x) || ps.CheckBooleanFlag("boolControlVC", x => siBoolControlVc = x, true) || @@ -1809,7 +1809,7 @@ extract reducible loops into recursive procedures and inline irreducible loops using the bound supplied by /loopUnroll: /soundLoopUnrolling sound loop unrolling - /doModSetAnalysis + /inferModifies automatically infer modifies clauses /printModel: 0 (default) - do not print Z3's error model diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 6b9b1b709..030f0ca11 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -229,11 +229,11 @@ public void CoalesceBlocks(Program program) } - public void CollectModSets(Program program) + public void CollectModifies(Program program) { - if (Options.DoModSetAnalysis) + if (Options.InferModifies) { - new ModSetCollector(Options).DoModSetAnalysis(program); + new ModSetCollector(Options).CollectModifies(program); } } @@ -339,7 +339,7 @@ public Program ParseBoogieProgram(IList fileNames, bool suppressTraceOut if (program.TopLevelDeclarations.Any(d => d.HasCivlAttribute())) { Options.Libraries.Add("base"); - Options.DoModSetAnalysis = true; + Options.InferModifies = true; } foreach (var libraryName in Options.Libraries) @@ -403,6 +403,8 @@ public PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, return PipelineOutcome.TypeCheckingError; } + CollectModifies(program); + errorCount = program.Typecheck(Options); if (errorCount != 0) { @@ -443,8 +445,6 @@ public PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, return PipelineOutcome.FatalError; } - CollectModSets(program); - civlTypeChecker = new CivlTypeChecker(Options, program); civlTypeChecker.TypeCheck(); if (civlTypeChecker.checkingContext.ErrorCount != 0) @@ -728,7 +728,7 @@ public async Task> GetVerificationTasks(Program } EliminateDeadVariables(program); - CollectModSets(program); + CollectModifies(program); CoalesceBlocks(program); Inline(program); diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 7cfe2ef9d..3b0fe1e03 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -516,7 +516,7 @@ public Program GetProgram(ExecutionEngine engine, string code) { engine.ResolveAndTypecheck(program, bplFileName, out _); engine.EliminateDeadVariables(program); - engine.CollectModSets(program); + engine.CollectModifies(program); engine.CoalesceBlocks(program); engine.Inline(program); return program; diff --git a/Test/civl/large-samples/cache-coherence.bpl b/Test/civl/large-samples/cache-coherence.bpl index c14927ea8..822f42b53 100644 --- a/Test/civl/large-samples/cache-coherence.bpl +++ b/Test/civl/large-samples/cache-coherence.bpl @@ -72,19 +72,22 @@ var {:layer 1,3} absMem: [MemAddr]Value; /* The proof is done in two layers. -At layer 1, cachePermissions and dirPermissions are introduced allowing dirBusy and cacheBusy -to be hidden. At this layer, absMem is also introduced. The main purpose of this layer is to -create atomic actions with suitable mover types. Specifically, we want the following: +Layer 1 to layer 2: +absMem is introduced to enable specification of the cache coherence property. +cachePermissions and dirPermissions are introduced allowing dirBusy and cacheBusy to be hidden. +The main purpose of this proof is to create atomic actions with suitable mover types. +Specifically, we want the following: - Memory operations (read and write) to be both movers. - Shared invalidate request at cache to be left mover. - Response to read request at cache to be left mover. - Initiation and conclusion of cache and directory operations to be right and left movers, respectively. -At layer 2, we do an invariance proof to hide the directory and all the caches so that the read -and write operations at cache are described as atomic operations over absMem. This specfication -method naturally captures the cache coherence property. To achieve this specfication, the variables -mem, dir, cache, cachePermissions, and dirPermissions are hidden. The yield invariant at this level -is a global invariant connecting directory and cache states. +Layer 2 to layer 3: +We do an invariance proof to hide the directory and all the caches so that the read +and write operations at cache are described as atomic operations over absMem. +This specfication method naturally captures the cache coherence property. +To achieve this specfication, the variables mem, dir, cache, cachePermissions, and dirPermissions are hidden. +The yield invariant at this level is a global invariant connecting directory and cache states. */ /// Yield invariants @@ -116,21 +119,20 @@ invariant (var line := cache[i][Hash(ma)]; (line->state == Invalid() || line->st /// Cache /* -There are 5 top-level operations on the cache. -cache_read and cache_write read and write a cache entry, respectively; -they may nondeterministically choose not to do the operation. -cache_evict_req initiates eviction of a cache line. -cache_read_shd_req and cache_read_exc_req initiate bringing a memory address into the cache -in Shared and Exclusive mode, respectively. +There are 5 top-level operations on the cache: +- cache_read and cache_write read and write a cache entry, respectively. +- cache_evict_req initiates eviction of a cache line. +- cache_read_shd_req and cache_read_exc_req initiate bringing a memory address into the cache + in Shared and Exclusive mode, respectively. The last three operations make asynchronous calls to corresponding operations on the directory to achieve their goals. -To specify the protocol, we introduce absMem, a global variable capturing the logical view of -memory at layer 1. -The verification demonstrates that cache_read and cache_read do the appropriate operation -on absMem. -At layer 3, all operations other than cache_read and cache_write disappear by becoming "skip" -since all the concrete state is hidden by layer 2. +We introduce at layer 1 a global variable absMem to capture the logical view of memory. +The presence of absMem allows us to specify the cache coherence property in a natural way. +The verification demonstrates that at layer 3: +- cache_read is abstracted by an atomic action that reads from absMem. +- cache_write is abstracted by an atomic action that writes to absMem. +- all other operations are abstracted by "skip". */ yield procedure {:layer 2} cache_read(i: CacheId, ma: MemAddr) returns (result: Option Value) diff --git a/Test/civl/regression-tests/modifies-bug.bpl b/Test/civl/regression-tests/modifies-bug.bpl new file mode 100644 index 000000000..daed74379 --- /dev/null +++ b/Test/civl/regression-tests/modifies-bug.bpl @@ -0,0 +1,13 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var {:layer 0,1} g: int; +yield right procedure {:layer 1} P() +{ + call A(); +} + +yield procedure {:layer 0} A(); +refines right action {:layer 1} _ { + g := 1; +} diff --git a/Test/civl/regression-tests/modifies-bug.bpl.expect b/Test/civl/regression-tests/modifies-bug.bpl.expect new file mode 100644 index 000000000..92e2c1a19 --- /dev/null +++ b/Test/civl/regression-tests/modifies-bug.bpl.expect @@ -0,0 +1,2 @@ +modifies-bug.bpl(7,4): Error: modified variable does not appear in modifies clause of mover procedure: g +1 type checking errors detected in modifies-bug.bpl diff --git a/Test/smack/git-issue-203-define.bpl b/Test/smack/git-issue-203-define.bpl index 1310d8fd8..fdddd2728 100644 --- a/Test/smack/git-issue-203-define.bpl +++ b/Test/smack/git-issue-203-define.bpl @@ -1,7 +1,7 @@ // generated by SMACK version 2.4.0 for boogie // via /usr/local/bin/smack two_arrays.c --loop-limit=11 --unroll=11 --verifier=boogie --debug --bpl=pero.bpl -// RUN: %parallel-boogie -doModSetAnalysis -timeLimit:1200 -errorLimit:1 -loopUnroll:15 "%s" > "%t" +// RUN: %parallel-boogie -inferModifies -timeLimit:1200 -errorLimit:1 -loopUnroll:15 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Basic types diff --git a/Test/smack/git-issue-203.bpl b/Test/smack/git-issue-203.bpl index 319540032..a6686991b 100644 --- a/Test/smack/git-issue-203.bpl +++ b/Test/smack/git-issue-203.bpl @@ -1,7 +1,7 @@ // generated by SMACK version 2.4.0 for boogie // via /usr/local/bin/smack two_arrays.c --loop-limit=11 --unroll=11 --verifier=boogie --debug --bpl=pero.bpl -// RUN: %parallel-boogie -doModSetAnalysis -timeLimit:1200 -errorLimit:1 -loopUnroll:15 "%s" > "%t" +// RUN: %parallel-boogie -inferModifies -timeLimit:1200 -errorLimit:1 -loopUnroll:15 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Basic types