simplified assert translation by adding pure action Assert

Author: shazqadeer

Source/Concurrency/YieldingProcDuplicator.cs

@@ -173,19 +173,7 @@ public override Cmd VisitAssertCmd(AssertCmd node)
         assertCmd.Expr = Expr.True;
         return assertCmd;
       }
-      if (layerNum != enclosingYieldingProc.Layer)
-      {
-        return assertCmd;
-      }
-      bool insideLoopInvariantOfYieldingLoop = enclosingYieldingProc.IsYieldingLoopHeaderAtProcedureLayer(enclosingBlock) && inPredicatePhase;
-      if (insideLoopInvariantOfYieldingLoop)
-      {
-        return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd;
-      }
-      else
-      {
-        return doRefinementCheck ? assertCmd : new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes);
-      }
+      return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd;
     }
 
     public override Cmd VisitCallCmd(CallCmd call)

Source/Core/base.bpl

@@ -338,3 +338,8 @@ datatype Unit { Unit() }
 function {:inline} UnitSet(): Set Unit {
   Set_Add(Set_Empty(), Unit())
 }
+
+pure action Assert(b: bool)
+{
+  assert b;
+}

Test/civl/large-samples/GC.bpl

@@ -301,7 +301,7 @@ preserves call Yield_Iso();
 preserves call Yield_Lock();
 requires {:layer 95, 96, 99} tid->i == i;
 {
-    assert {:layer 100} mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]);
+    call {:layer 100} Assert(mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]));
     call WriteBarrier(tid, i, y);
     call Yield_Iso() | Yield_WriteField(tid, x, y);
     call WriteFieldRaw(tid, x, f, y) | Yield_Lock();
@@ -1936,7 +1936,8 @@ refines AtomicLockAcquire;
 preserves call Yield_Lock();
 {
     var status:bool;
-    assert {:layer 95} tid->i != 0;
+
+    call {:layer 95} Assert(tid->i != 0);
     while (true)
         invariant {:yields} true;
         invariant call Yield_Lock();

Test/civl/large-samples/cache-coherence.bpl

@@ -357,7 +357,7 @@ refines atomic action {:layer 2} _ {
   call Set_Put(cachePermissions, drp);
 }
 {
-  assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma))));
+  call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma)))));
   call cache_evict_resp#0(i, ma);
   call {:layer 1} Set_Put(cachePermissions, drp);
 }
@@ -397,7 +397,7 @@ refines left action {:layer 2} _ {
   call Set_Put(cachePermissions, drp);
 }
 {
-  assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma))));
+  call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma)))));
   call cache_read_resp#0(i, ma, v, s);
   call {:layer 1} Set_Put(cachePermissions, drp);
 }
@@ -722,7 +722,7 @@ refines left action {:layer 2} _ {
   call Set_Put(dirPermissions, dp);
 }
 {
-  assert {:layer 1} dp == WholeDirPermission(ma);
+  call {:layer 1} Assert(dp == WholeDirPermission(ma));
   call dir_req_end#0(ma, dirState);
   call {:layer 1} Set_Put(dirPermissions, dp);
 }

Test/civl/large-samples/shared-vector.bpl

@@ -157,8 +157,8 @@ preserves call Yield(loc_iv);
     return;
   }
 
-  assert {:layer 2} Map_Contains(IntArrayPool, One(loc_iv));
-  assert {:layer 2} (var vec := Map_At(IntArrayPool, One(loc_iv)); Vec_Contains(vec, i) && Vec_Contains(vec, j));
+  call {:layer 2} Assert(Map_Contains(IntArrayPool, One(loc_iv)));
+  call {:layer 2} Assert((var vec := Map_At(IntArrayPool, One(loc_iv)); Vec_Contains(vec, i) && Vec_Contains(vec, j)));
 
   // deadlock avoidance
   if (i < j) {

Test/civl/paxos/PaxosImpl.bpl

@@ -178,7 +178,7 @@ refines left action {:layer 2} _ {
   status[r] := Proposed(v);
 } 
 {
-  assert {:layer 1} voteInfo[r] == MapConst(false);
+  call {:layer 1} Assert(voteInfo[r] == MapConst(false));
   call {:layer 1} status := Copy(status[r := Proposed(v)]);
 }
 
@@ -296,7 +296,7 @@ refines left action {:layer 2} _ {
   status[r] := Decided(v);
 }
 {
-  assert {:layer 1} status[r] == Proposed(v);
+  call {:layer 1} Assert(status[r] == Proposed(v));
   call {:layer 1} status := Copy(status[r := Decided(v)]);
 }
 
@@ -363,8 +363,8 @@ requires call YieldInv();
 {
   var voteResponse: VoteResponse;
 
-  assert {:layer 1} IsActive(status[r], v);
-  assert {:layer 1} !voteInfo[r][n];
+  call {:layer 1} Assert(IsActive(status[r], v));
+  call {:layer 1} Assert(!voteInfo[r][n]);
   call voteResponse := VoteUpdate(r, n, v);
   call SendVoteResponse(r, voteResponse);
   if (voteResponse is VoteAccept) {

Test/civl/regression-tests/Pure2.bpl

@@ -66,7 +66,7 @@ preserves call YieldInv();
 preserves call YieldWait(tid);
 {
   var oldValue: int;
-  assert {:layer 1} mutex == Some(tid->val);
+  call {:layer 1} Assert(mutex == Some(tid->val));
   call oldValue := FetchSub(1);
   if (oldValue == 1) {
     call {:layer 1} mutex := Copy(None());

Test/civl/regression-tests/Pure2.bpl.expect

@@ -75,8 +75,7 @@ requires {:layer 1} mutatorOrGcTid(tid->val);
 preserves call YieldLock();
 preserves call YieldStoreBufferLockAddrAbsent(tid);
 {
-    assert {:layer 1} mutatorOrGcTid(tid->val);
-    assert {:layer 1} lock == tid->val;
+    call {:layer 1} Assert(lock == tid->val);
     call LockZero(tid->val);
     call YieldLock() | YieldStoreBufferLockAddrPresent(tid);
     call FlushStoreBufferEntryForLock(tid->val);
@@ -114,9 +113,8 @@ refines AtomicSetCollectorPhase;
 requires {:layer 1} mutatorOrGcTid(tid->val);
 preserves call YieldLock();
 {
-    assert {:layer 1} mutatorOrGcTid(tid->val);
-    assert {:layer 1} lock == tid->val;
-    assert {:layer 1} collectorPhase == collectorPhaseDelayed;
+    call {:layer 1} Assert(lock == tid->val);
+    call {:layer 1} Assert(collectorPhase == collectorPhaseDelayed);
     call PrimitiveSetCollectorPhase(tid->val, phase);
 }