Extend trust options

Source/Concurrency/CivlRewriter.cs

@@ -26,7 +26,6 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
       // Gate sufficiency checks
       Action.AddGateSufficiencyCheckers(civlTypeChecker, decls);
 
-      // Commutativity checks
       civlTypeChecker.AtomicActions.ForEach(x =>
       {
         decls.AddRange(new Declaration[] { x.Impl, x.Impl.Proc, x.InputOutputRelation });
@@ -37,19 +36,27 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
         }
       });
 
+      // Commutativity checks
       if (!options.TrustMoverTypes)
       {
         MoverCheck.AddCheckers(civlTypeChecker, decls);
       }
 
       // Desugaring of yielding procedures
-      YieldingProcChecker.AddCheckers(civlTypeChecker, decls);
-
-      if (!options.TrustSequentialization)
+      if (!options.TrustInvariants)
       {
-        Sequentialization.AddCheckers(civlTypeChecker, decls);
+         YieldingProcChecker.AddInvariantCheckers(civlTypeChecker, decls);
       }
-
+
+      if (!options.TrustRefinement)
+      {
+         YieldingProcChecker.AddRefinementCheckers(civlTypeChecker, decls);
+         if (!options.TrustSequentialization)
+         {
+            Sequentialization.AddCheckers(civlTypeChecker, decls);
+         }
+      }
+
       foreach (var action in civlTypeChecker.AtomicActions)
       {
         action.AddTriggerAssumes(program, options);

Source/Concurrency/ConcurrencyOptions.cs

@@ -8,5 +8,6 @@ public interface ConcurrencyOptions : CoreOptions
   int TrustLayersUpto { get; }
   bool TrustNoninterference { get; }
   bool TrustRefinement { get; }
+  bool TrustInvariants { get; }
   bool WarnNotEliminatedVars { get; }
 }

Source/Concurrency/YieldingProcChecker.cs

@@ -5,11 +5,11 @@ namespace Microsoft.Boogie
 {
   public class YieldingProcChecker
   {
-    public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
+    public static void AddInvariantCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
     {
       Program program = civlTypeChecker.program;
 
-      // Generate the noninterference checks for every layer
+      // Generate the invariant checks for every layer
       foreach (int layerNum in civlTypeChecker.AllRefinementLayers)
       {
         if (civlTypeChecker.Options.TrustLayersDownto <= layerNum ||
@@ -38,12 +38,13 @@ public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration
         }
         decls.AddRange(duplicator.Collect());
       }
+    }
+
+    public static void AddRefinementCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
+    {
+      Program program = civlTypeChecker.program;
 
       // Generate the refinement checks for every layer
-      if (civlTypeChecker.Options.TrustRefinement)
-      {
-        return;
-      }
       foreach (int layerNum in civlTypeChecker.AllRefinementLayers)
       {
         if (civlTypeChecker.Options.TrustLayersDownto <= layerNum ||

Source/ExecutionEngine/CommandLineOptions.cs

@@ -443,6 +443,11 @@ public bool TrustRefinement {
       set => trustRefinement = value;
     }
 
+    public bool TrustInvariants {
+      get => trustInvariants;
+      set => trustInvariants = value;
+    }
+
     public int TrustLayersUpto { get; set; } = -1;
 
     public int TrustLayersDownto { get; set; } = int.MaxValue;
@@ -593,6 +598,7 @@ void ObjectInvariant5()
     private bool trustMoverTypes = false;
     private bool trustNoninterference = false;
     private bool trustRefinement = false;
+    private bool trustInvariants = false;
     private bool trustSequentialization = false;
     private int enhancedErrorMessages = 0;
     private int stagedHoudiniThreads = 1;
@@ -1384,6 +1390,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("trustMoverTypes", x => trustMoverTypes = x) ||
               ps.CheckBooleanFlag("trustNoninterference", x => trustNoninterference = x) ||
               ps.CheckBooleanFlag("trustRefinement", x => trustRefinement = x) ||
+              ps.CheckBooleanFlag("trustInvariants", x => trustInvariants = x) ||
               ps.CheckBooleanFlag("trustSequentialization", x => trustSequentialization = x) ||
               ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) ||
               ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) ||
@@ -1891,6 +1898,8 @@ print Boogie program after it has been instrumented with
                 do not perform noninterference checks
   /trustRefinement
                 do not perform refinement checks
+  /trustInvariants
+                do not perform invariant checks
   /trustLayersUpto:<n>
                 do not verify layers <n> and below
   /trustLayersDownto:<n>