Move modifies inference immediately after resolution

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<Procedure>();
@@ -66,8 +66,11 @@ public void DoModSetAnalysis(Program program)
 
     foreach (Procedure x in modSets.Keys)
     {
-      x.Modifies = new List<IdentifierExpr>();
-      foreach (Variable v in modSets[x])
+      if (x.Modifies == null)
+      {
+        x.Modifies = new List<IdentifierExpr>();
+      }
+      foreach (Variable v in modSets[x].Except(x.Modifies.Select(y => y.Decl)))
       {
         x.Modifies.Add(new IdentifierExpr(v.tok, v));
       }

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; }

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)

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:<n>
   /soundLoopUnrolling
                 sound loop unrolling
-  /doModSetAnalysis
+  /inferModifies
                 automatically infer modifies clauses
   /printModel:<n>
                 0 (default) - do not print Z3's error model

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<string> 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<IReadOnlyList<IVerificationTask>> GetVerificationTasks(Program
       }
 
       EliminateDeadVariables(program);
-      CollectModSets(program);
+      CollectModifies(program);
       CoalesceBlocks(program);
       Inline(program);
 

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;

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)

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;
+}

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

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

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