CIVL cleanup: simplified Absy construction and consistent use of Asse…

…rtCmd (#311)
boogie-org · Nov 11, 2020 · 5be260b · 5be260b
1 parent 2f029a2
commit 5be260b
Show file tree

Hide file tree

Showing 34 changed files with 409 additions and 420 deletions.
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
@@ -83,24 +83,19 @@ public CivlTypeChecker(Program program)
         }
       }
 
-      var skipProcedure = new Procedure(
-        Token.NoToken,
+      var skipProcedure = DeclHelper.Procedure(
         AddNamePrefix("Skip"),
-        new List<TypeVariable>(),
         new List<Variable>(),
         new List<Variable>(),
         new List<Requires>(),
         new List<IdentifierExpr>(),
         new List<Ensures>());
-      var skipImplementation = new Implementation(
-          Token.NoToken,
-          skipProcedure.Name,
-          new List<TypeVariable>(),
-          new List<Variable>(),
-          new List<Variable>(),
-          new List<Variable>(),
-          new List<Block> {new Block(Token.NoToken, "init", new List<Cmd>(), new ReturnCmd(Token.NoToken))})
-        {Proc = skipProcedure};
+      var skipImplementation = DeclHelper.Implementation(
+        skipProcedure,
+        new List<Variable>(),
+        new List<Variable>(),
+        new List<Variable>(),
+        new List<Block> {BlockHelper.Block("init", new List<Cmd>())});
       SkipAtomicAction = new AtomicAction(skipProcedure, skipImplementation, LayerRange.MinMax, MoverType.Both);
     }
 

diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs
@@ -76,6 +76,21 @@ public static OldExpr Old(Expr expr)
       return new OldExpr(Token.NoToken, expr);
     }
 
+    public static ExistsExpr ExistsExpr(List<Variable> dummies, Expr body)
+    {
+      return new ExistsExpr(Token.NoToken, dummies, body);
+    }
+
+    public static ExistsExpr ExistsExpr(List<Variable> dummies, Trigger triggers, Expr body)
+    {
+      return new ExistsExpr(Token.NoToken, dummies, triggers, body);
+    }
+
+    public static ForallExpr ForallExpr(List<Variable> dummies, Expr body)
+    {
+      return new ForallExpr(Token.NoToken, dummies, body);
+    }
+
     public static void FlattenAnd(Expr x, List<Expr> xs)
     {
       if (x is NAryExpr naryExpr && naryExpr.Fun.FunctionName == "&&")
@@ -97,7 +112,7 @@ public static class CmdHelper
     public static CallCmd CallCmd(Procedure callee, List<Expr> ins, List<IdentifierExpr> outs)
     {
       return new CallCmd(Token.NoToken, callee.Name, ins, outs)
-        {Proc = callee};
+        { Proc = callee };
     }
 
     public static CallCmd CallCmd(Procedure callee, List<Variable> ins, List<Variable> outs)
@@ -110,6 +125,12 @@ public static AssumeCmd AssumeCmd(Expr expr)
       return new AssumeCmd(Token.NoToken, expr);
     }
 
+    public static AssertCmd AssertCmd(IToken tok, Expr expr, string msg)
+    {
+      return new AssertCmd(tok, expr)
+        { ErrorData = msg };
+    }
+
     public static AssignCmd AssignCmd(Variable v, Expr x)
     {
       var lhs = new SimpleAssignLhs(Token.NoToken, Expr.Ident(v));
@@ -121,6 +142,42 @@ public static AssignCmd AssignCmd(IList<IdentifierExpr> lhss, IList<Expr> rhss)
       var assignLhss = lhss.Select(lhs => new SimpleAssignLhs(Token.NoToken, lhs)).ToList<AssignLhs>();
       return new AssignCmd(Token.NoToken, assignLhss, rhss);
     }
+
+    public static HavocCmd HavocCmd(List<IdentifierExpr> vars)
+    {
+      return new HavocCmd(Token.NoToken, vars);
+    }
+  }
+
+  public static class BlockHelper
+  {
+    public static Block Block(string label, List<Cmd> cmds)
+    {
+      return new Block(Token.NoToken, 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));
+    }
+  }
+
+  public static class DeclHelper
+  {
+    public static Procedure Procedure(string name,
+      List<Variable> inParams, List<Variable> outParams,
+      List<Requires> requires, List<IdentifierExpr> modifies, List<Ensures> ensures,
+      QKeyValue kv = null)
+    {
+      return new Procedure(Token.NoToken, name, new List<TypeVariable>(), inParams, outParams, requires, modifies, ensures, kv);
+    }
+
+    public static Implementation Implementation(Procedure proc,
+      List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables,
+      List<Block> blocks, QKeyValue kv = null)
+    {
+      return new Implementation(Token.NoToken, proc.Name, new List<TypeVariable>(), inParams, outParams, localVariables, blocks, kv) { Proc = proc };
+    }
   }
 
   public static class VarHelper
@@ -215,10 +272,5 @@ from acc in accumulator
           from item in sequence
           select acc.Concat(new[] {item}));
     }
-
-    public static Dictionary<TKey, TValue> ToDictionary<TKey, TValue>(this IEnumerable<TKey> keys, Func<TKey, TValue> f)
-    {
-      return keys.ToDictionary(k => k, k => f(k));
-    }
   }
 }
diff --git a/Source/Concurrency/GlobalSnapshotInstrumentation.cs b/Source/Concurrency/GlobalSnapshotInstrumentation.cs
@@ -27,37 +27,37 @@ public GlobalSnapshotInstrumentation(CivlTypeChecker civlTypeChecker)
 
     public List<Cmd> CreateUpdatesToOldGlobalVars()
     {
-      List<AssignLhs> lhss = new List<AssignLhs>();
+      List<IdentifierExpr> lhss = new List<IdentifierExpr>();
       List<Expr> rhss = new List<Expr>();
       foreach (Variable g in oldGlobalMap.Keys)
       {
-        lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldGlobalMap[g])));
+        lhss.Add(Expr.Ident(oldGlobalMap[g]));
         rhss.Add(Expr.Ident(g));
       }
 
       var cmds = new List<Cmd>();
       if (lhss.Count > 0)
       {
-        cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+        cmds.Add(CmdHelper.AssignCmd(lhss, rhss));
       }
 
       return cmds;
     }
 
     public List<Cmd> CreateInitCmds()
     {
-      List<AssignLhs> lhss = new List<AssignLhs>();
+      List<IdentifierExpr> lhss = new List<IdentifierExpr>();
       List<Expr> rhss = new List<Expr>();
       foreach (Variable g in oldGlobalMap.Keys)
       {
-        lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldGlobalMap[g])));
+        lhss.Add(Expr.Ident(oldGlobalMap[g]));
         rhss.Add(Expr.Ident(g));
       }
 
       var initCmds = new List<Cmd>();
       if (lhss.Count > 0)
       {
-        initCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+        initCmds.Add(CmdHelper.AssignCmd(lhss, rhss));
       }
 
       return initCmds;