Introduce {:isolate} and {:isolate "paths"} attributes for assert…

… and return commands (#952) ### Changes - Introduce the `{:isolate}` attribute on AssertCmd and `ReturnCmd` - Introduce the `{:isolate "paths"}` attribute on AssertCmd and `ReturnCmd` - Introduce new tokens that allow precisely describing where a particular Split comes from. - Fix a bug that caused too many VCs to be created when using `/vcsSplitOnEveryAssert` together with focus - Fix incorrect token bug for VCs originating from focus. ### Testing - Created a folder `Test/implementationDivision` that has tests for `{:isolate}`, `{:isolate "paths"}`, `{:focus}` and `{:split_here}` --------- Co-authored-by: Mikaël Mayer <[email protected]>
boogie-org · Oct 7, 2024 · 25160fa · 25160fa
1 parent 9a8ce8d
commit 25160fa
Show file tree

Hide file tree

Showing 77 changed files with 1,663 additions and 858 deletions.
diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs
@@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars)
 
   public static class BlockHelper
   {
+    public static readonly IToken /*!*/ ReportedNoToken = new Token();
+
     public static Block Block(string label, List<Cmd> cmds)
     {
-      return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd);
+      return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd);
     }
 
     public static Block Block(string label, List<Cmd> cmds, List<Block> gotoTargets)
     {
-      return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
+      return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
     }
   }
 

diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
@@ -368,10 +368,9 @@ int FreshAnon()
       return anon++;
     }
 
-    HashSet<string /*!*/> allLabels = new HashSet<string /*!*/>();
+    private readonly HashSet<string /*!*/> allLabels = new();
 
-    Errors /*!*/
-      errorHandler;
+    private readonly Errors /*!*/ errorHandler;
 
     [ContractInvariantMethod]
     void ObjectInvariant()
@@ -3445,6 +3444,8 @@ public override void Emit(TokenTextWriter stream, int level)
 
   public class ReturnCmd : TransferCmd
   {
+    public QKeyValue Attributes { get; set; }
+
     public ReturnCmd(IToken /*!*/ tok)
       : base(tok)
     {
@@ -3476,6 +3477,8 @@ public class GotoCmd : TransferCmd
     [Rep] public List<String> LabelNames;
     [Rep] public List<Block> LabelTargets;
 
+    public QKeyValue Attributes { get; set; }
+
     [ContractInvariantMethod]
     void ObjectInvariant()
     {

diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Block.cs
@@ -128,7 +128,11 @@ public bool IsLive(Variable v)
     return liveVarsBefore.Contains(v);
   }
 
-  public Block(IToken tok)
+  public static Block ShallowClone(Block block) {
+    return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd);
+  }
+
+  public Block(IToken tok, TransferCmd cmd)
     : this(tok, "", new List<Cmd>(), new ReturnCmd(tok))
   {
   }

diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs
@@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
         Contract.Assert(a != null);
         // These probably won't have IDs, but copy if they do.
         if (callId is not null) {
-          a.CopyIdWithModificationsFrom(tok, req,
+          (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req,
             id => new TrackedCallRequiresAssumed(callId, id));
         }
 
@@ -1066,7 +1066,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
       #endregion
 
       if (callId is not null) {
-        assume.CopyIdWithModificationsFrom(tok, e,
+        (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e,
           id => new TrackedCallEnsures(callId, id));
       }
 

diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs
@@ -51,23 +51,25 @@ public void AddStringAttribute(IToken tok, string name, string parameter)
     Attributes = new QKeyValue(tok, name, new List<object>() {parameter}, Attributes);
   }
 
+
 }
 
-public static class CarriesAttributesExtensions
-{
-  public static void CopyIdFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src)
+public static class CarriesAttributesExtensions {
+  
+  public static void CopyIdFrom(this ICarriesAttributes destination, IToken tok, ICarriesAttributes src)
   {
     var id = src.FindStringAttribute("id");
     if (id is not null) {
-      dest.AddStringAttribute(tok, "id", id);
+      destination.AddStringAttribute(tok, "id", id);
     }
   }
 
-  public static void CopyIdWithModificationsFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src, Func<string,TrackedNodeComponent> modifier)
+  public static void CopyIdWithModificationsFrom(this ICarriesAttributes destination, IToken tok, 
+    ICarriesAttributes src, Func<string,TrackedNodeComponent> modifier)
   {
     var id = src.FindStringAttribute("id");
     if (id is not null) {
-      dest.AddStringAttribute(tok, "id", modifier(id).SolverLabel);
+      destination.AddStringAttribute(tok, "id", modifier(id).SolverLabel);
     }
   }
 }
diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs
@@ -462,19 +462,19 @@ void BlocksWriters(TokenTextWriter stream) {
   }
 
   public void EmitImplementation(TokenTextWriter stream, int level, IEnumerable<Block> blocks,
-    bool showLocals) {
+    bool showLocals, string nameSuffix = "") {
     EmitImplementation(stream, level, writer => {
       foreach (var block in blocks) {
         block.Emit(writer, level + 1);
       }
-    }, showLocals);
+    }, showLocals, nameSuffix);
   }
 
-  public void EmitImplementation(TokenTextWriter stream, int level, Action<TokenTextWriter> printBlocks, bool showLocals)
+  private void EmitImplementation(TokenTextWriter stream, int level, Action<TokenTextWriter> printBlocks, bool showLocals, string nameSuffix = "")
   {
     stream.Write(this, level, "implementation ");
     EmitAttributes(stream);
-    stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
+    stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(Name) + nameSuffix);
     EmitSignature(stream, false);
     stream.WriteLine();
 

diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs
@@ -498,14 +498,17 @@ public static Graph<Implementation> BuildCallGraph(CoreOptions options, Program
     return callGraph;
   }
 
-  public static Graph<Block> GraphFromBlocks(List<Block> blocks, bool forward = true)
+  public static Graph<Block> GraphFromBlocksSubset(IReadOnlyList<Block> blocks, IReadOnlySet<Block> subset = null, bool forward = true)
   {
     var result = new Graph<Block>();
     if (!blocks.Any())
     {
       return result;
     }
     void AddEdge(Block a, Block b) {
+      if (subset != null && (!subset.Contains(a) || !subset.Contains(b))) {
+        return;
+      }
       Contract.Assert(a != null && b != null);
       if (forward) {
         result.AddEdge(a, b);
@@ -514,7 +517,7 @@ void AddEdge(Block a, Block b) {
       }
     }
 
-    result.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
+    result.AddSource(blocks[0]);
     foreach (var block in blocks)
     {
       if (block.TransferCmd is GotoCmd gtc)
@@ -525,6 +528,10 @@ void AddEdge(Block a, Block b) {
     }
     return result;
   }
+
+  public static Graph<Block> GraphFromBlocks(IReadOnlyList<Block> blocks, bool forward = true) {
+    return GraphFromBlocksSubset(blocks, null, forward);
+  }
 
   public static Graph<Block /*!*/> /*!*/ GraphFromImpl(Implementation impl, bool forward = true)
   {

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
@@ -1032,14 +1032,17 @@ TransferCmd<out TransferCmd/*!*/ tc>
 = (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;
      Token y;  List<IToken>/*!*/ xs;
      List<String> ss = new List<String>();
+     QKeyValue kv = null;
   .)
   ( "goto"             (. y = t; .)
     Idents<out xs>     (. foreach(IToken/*!*/ s in xs){
                             Contract.Assert(s != null);
                             ss.Add(s.val); }
                           tc = new GotoCmd(y, ss);
                        .)
-  | "return"           (. tc = new ReturnCmd(t); .)
+  | "return"
+    { Attribute<ref kv> }         
+    (. tc = new ReturnCmd(t) { Attributes = kv }; .)
   ) ";"
   .
 
@@ -1688,6 +1691,7 @@ SpecBlock<out Block/*!*/ b>
      List<IToken>/*!*/ xs;
      List<String> ss = new List<String>();
      b = dummyBlock;
+     QKeyValue kv = null;
      Expr/*!*/ e;
   .)
   Ident<out x> ":"
@@ -1706,8 +1710,13 @@ SpecBlock<out Block/*!*/ b>
                             ss.Add(s.val); }
                           b = new Block(x,x.val,cs,new GotoCmd(y,ss));
                        .)
-  | "return" Expression<out e>
-                       (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)
+  | "return" 
+    { Attribute<ref kv> }
+    Expression<out e>
+                       (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) {
+                            Attributes = kv
+                          }); 
+                       .)
   )
   ";"
   .

diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs
@@ -10,6 +10,8 @@ namespace Microsoft.Boogie
   public interface CoreOptions : PrintOptions {
     public TextWriter OutputWriter { get; }
 
+    bool UseBaseNameForFileName { get; }
+
     public enum TypeEncoding
     {
       Predicates,

diff --git a/Source/Core/Generic/ListExtensions.cs b/Source/Core/Generic/ListExtensions.cs
@@ -0,0 +1,31 @@
+using System.Collections;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace Microsoft.Boogie;
+
+public static class ListExtensions {
+  public static IReadOnlyList<T> Reversed<T>(this IReadOnlyList<T> list) {
+    return new ReversedReadOnlyList<T>(list);
+  }
+}
+
+class ReversedReadOnlyList<T> : IReadOnlyList<T> {
+  private readonly IReadOnlyList<T> inner;
+
+  public ReversedReadOnlyList(IReadOnlyList<T> inner) {
+    this.inner = inner;
+  }
+
+  public IEnumerator<T> GetEnumerator() {
+    return Enumerable.Range(0, inner.Count).Select(index => this[index]).GetEnumerator();
+  }
+
+  IEnumerator IEnumerable.GetEnumerator() {
+    return GetEnumerator();
+  }
+
+  public int Count => inner.Count;
+
+  public T this[int index] => inner[^(index + 1)];
+}
diff --git a/Source/Core/Util.cs → Source/Core/Generic/Util.cs b/Source/Core/Util.cs → Source/Core/Generic/Util.cs
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
@@ -1536,6 +1536,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 		Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;
 		Token y;  List<IToken>/*!*/ xs;
 		List<String> ss = new List<String>();
+		QKeyValue kv = null;
 
 		if (la.kind == 55) {
 			Get();
@@ -1548,7 +1549,10 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 
 		} else if (la.kind == 56) {
 			Get();
-			tc = new ReturnCmd(t); 
+			while (la.kind == 26) {
+				Attribute(ref kv);
+			}
+			tc = new ReturnCmd(t) { Attributes = kv }; 
 		} else SynErr(148);
 		Expect(10);
 	}
@@ -2558,6 +2562,7 @@ void SpecBlock(out Block/*!*/ b) {
 		List<IToken>/*!*/ xs;
 		List<String> ss = new List<String>();
 		b = dummyBlock;
+		QKeyValue kv = null;
 		Expr/*!*/ e;
 
 		Ident(out x);
@@ -2583,8 +2588,14 @@ void SpecBlock(out Block/*!*/ b) {
 
 		} else if (la.kind == 56) {
 			Get();
+			while (la.kind == 26) {
+				Attribute(ref kv);
+			}
 			Expression(out e);
-			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); 
+			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) {
+			 Attributes = kv
+			}); 
+
 		} else SynErr(174);
 		Expect(10);
 	}

diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs
@@ -33,8 +33,7 @@ public string /*!*/
 
     public Token next; // ML 2005-03-11 Tokens are kept in linked list
 
-    public static readonly IToken /*!*/
-      NoToken = new Token();
+    public static readonly IToken /*!*/ NoToken = new Token();
 
     public Token()
     {

diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
@@ -523,14 +523,14 @@ private Dictionary<Block, HashSet<Block>> ComputeGlobalControlDependences()
       foreach (var impl in prog.NonInlinedImplementations())
       {
         var blockGraph = prog.ProcessLoops(options, impl);
-        localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok));
+        localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok, new ReturnCmd(prog.tok)));
         foreach (var keyValue in localCtrlDeps[impl])
         {
           globalCtrlDep.Add(keyValue.Key, keyValue.Value);
         }
       }
 
-      var callGraph = Program.BuildCallGraph(options, prog);
+      Graph<Implementation> callGraph = Program.BuildCallGraph(options, prog);
 
       // Add inter-procedural control dependence nodes based on calls
       foreach (var impl in prog.NonInlinedImplementations())
@@ -548,7 +548,7 @@ private Dictionary<Block, HashSet<Block>> ComputeGlobalControlDependences()
             var indirectCallees = ComputeIndirectCallees(callGraph, directCallee);
             foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl]))
             {
-              foreach (var c in indirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item))
+              foreach (var c in indirectCallees.Select(item => item.Blocks).SelectMany(Item => Item))
               {
                 globalCtrlDep[control].Add(c);
               }
@@ -562,17 +562,18 @@ private Dictionary<Block, HashSet<Block>> ComputeGlobalControlDependences()
 
       // Finally reverse the dependences
 
-      var result = new Dictionary<Block, HashSet<Block>>();
-      foreach (var keyValue in globalCtrlDep)
+      Dictionary<Block, HashSet<Block>> result = new Dictionary<Block, HashSet<Block>>();
+
+      foreach (var KeyValue in globalCtrlDep)
       {
-        foreach (var v in keyValue.Value)
+        foreach (var v in KeyValue.Value)
         {
           if (!result.ContainsKey(v))
           {
             result[v] = new HashSet<Block>();
           }
 
-          result[v].Add(keyValue.Key);
+          result[v].Add(KeyValue.Key);
         }
       }
 

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.2.5</Version>
+    <Version>3.3.0</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
@@ -105,7 +105,7 @@ static void PassifyAllImplementations(ExecutionEngineOptions options, ProcessedP
 
       foreach(var implementation in processedProgram.Program.Implementations) {
         vcGenerator.PrepareImplementation(new ImplementationRun(implementation, options.OutputWriter),
-          callback, out _, out _, out _);
+          callback, out _, out _);
       }
     }
 

diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs
@@ -177,8 +177,9 @@ public virtual void ReportBplError(IToken tok, string message, bool error, TextW
       message = $"{category}: {message}";
     }
 
-    var s = tok != null 
-      ? $"{ExecutionEngine.GetFileNameForConsole(Options, tok.filename)}({tok.line},{tok.col}): {message}" 
+    var s = tok != null
+      ? string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(Options, tok.filename), tok.line,
+        tok.col, message)
       : message;
 
     if (error)