Reads without init events (#624)

benchmarks/c/miscellaneous/uninitRead.c

@@ -0,0 +1,17 @@
+#include <stdint.h>
+#include <assert.h>
+
+/*
+    This test shows that we can read from uninitialized memory.
+    EXPECTED: FAIL
+    PREVIOUSLY: We returned PASS because the array read had no possible rf-edge and thus the program had no valid executions.
+*/
+
+#define SIZE 10
+volatile int array[SIZE];
+
+int main()
+{
+    assert (array[SIZE] == 42);
+    return 0;
+}

cat/c11-orig.cat

@@ -0,0 +1,128 @@
+C "C++11"
+
+(* All c11_*.cat files are C11 models
+Overhauling SC atomics in C11 and OpenCL.
+M. Batty, A. Donaldson, J. Wickerson. In Proc.
+43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016.
+
+Rewritten by Luc Maranget for herd7
+
+*)
+
+include "c11_cos.cat"
+include "c11_los.cat"
+
+let asw = IW * (M \ IW)
+let sb = po
+let mo = co
+
+let cacq = ACQ | (SC & (R | F)) | ACQ_REL | (F & CON)
+let crel = REL | (SC & (W | F)) | ACQ_REL
+let ccon = R & CON
+
+let fr = rf^-1 ; mo
+
+let dd = (data | addr)+
+
+let fsb = sb & (F * _)
+let sbf = sb & (_ * F)
+
+(* release_acquire_fenced_synchronizes_with,
+   hypothetical_release_sequence_set,
+   release_sequence_set *)
+
+(* OLD: let rs = [crel] ; fsb? ; [A & W] ;
+         (((mo ; [rmw]) | coi) & ~(coe ; [!rmw] ; mo))? *)
+
+let rs_prime = int | (_ * (R & W))
+let rs = mo & rs_prime \ ((mo \ rs_prime) ; mo)
+
+(* OLD: let swra = ext (rs ; rf ; [A] ; sbf? ; [cacq]) *)
+let swra =
+ ext &
+ ([crel] ; fsb? ; [A & W] ; rs? ; rf ;
+ [R & A] ; sbf? ; [cacq])
+
+//let swul = ext & ([UL] ; lo ; [LK])
+let pp_asw = asw \ (asw ; sb)
+//let sw = pp_asw | swul | swra
+let sw = pp_asw | swra
+
+(* with_consume_cad_set,
+   dependency_ordered_before *)
+let cad = ((rf & sb) | dd)+
+let dob =
+ (ext &
+  ([W & crel] ; fsb? ; [A & W] ;
+   rs?; rf; [ccon]));
+ cad?
+
+(* happens_before,
+   inter_thread_happens_before,
+   consistent_hb *)
+let ithbr = sw | dob | (sw ; sb)
+let ithb = (ithbr | (sb ; ithbr))+
+let hb = sb | ithb
+acyclic hb as Hb
+
+(* coherent_memory_use *)
+let hbl = hb & loc
+
+irreflexive ((rf^-1)? ; mo ; rf? ; hb) as Coh
+
+(* visible_side_effect_set *)
+let vis = (hbl & (W * R)) \ (hbl; [W] ; hbl)
+
+(* consistent_atomic_rf *)
+irreflexive (rf ; hb) as Rf
+
+(* consistent_non_atomic_rf  *)
+empty ((rf ; [R\A]) \ vis) as NaRf
+// NOTE FW is a dynamic tag which we don't yet support
+//empty [FW\A];hbl;[W] as NaRf (* implicit read of Na final writes.. *)
+
+irreflexive (rf | (mo ; mo ; rf^-1) | (mo ; rf)) as Rmw
+
+
+(* locks_only_consistent_lo *)
+//irreflexive (lo ; hb) as Lo1
+
+(* locks_only_consistent_locks *)
+//irreflexive ([LS] ; lo^-1 ; [LS] ; ~(lo ; [UL] ; lo)) as Lo2
+
+
+(* data_races *)
+//let Mutex = UL|LS
+//let cnf = (((W * _) | (_ * W)) & loc) \ ((Mutex * _) | (_ * Mutex))
+//let dr = ext & (cnf \ hb \ (hb^-1) \ (A * A))
+
+(* unsequenced_races *)
+//let ur = int & ((W * M) | (M * W)) & loc & ~id & ~(sb+) & ~((sb+)^-1)
+
+(* locks_only_good_mutex_use,  locks_only_bad_mutexes *)
+
+//let bl = ([LS]; (sb & lo); [LK]) & ~(lo; [UL]; lo)
+
+//let losbwoul = (sb & lo & ~(lo; [UL]; lo))
+
+//let lu = [UL] & ~([UL] ; losbwoul^-1 ; [LS] ; losbwoul ; [UL])
+
+let r1 = hb
+let r2 = fsb? ; mo ; sbf?
+let r3 = rf^-1; [SC] ; mo
+let r4 = rf^-1 ; hbl ; [W]
+let r5 = fsb ; fr
+let r6 = fr ; sbf
+let r7 = fsb ; fr ; sbf
+
+let scp = r1|r2|r3|r4|r5|r6|r7
+
+acyclic (((SC * SC) & scp) \ id) as Spartial
+
+//undefined_unless empty dr as Dr
+//undefined_unless empty ur as unsequencedRace
+//undefined_unless empty bl as badLock
+//undefined_unless empty lu as badUnlock
+
+// Atomicity
+empty rmw & (fre; coe) as atomic

cat/c11.cat

@@ -9,6 +9,11 @@ Rewritten by Luc Maranget for herd7
 
 *)
 
+(*
+   This is an adapted version of C11 that supports an execution model where explicit init events
+   may be missing. As a consequence, reads may have no rf-edge if they read from initial memory.
+*)
+
 include "c11_cos.cat"
 include "c11_los.cat"
 
@@ -20,7 +25,8 @@ let cacq = ACQ | (SC & (R | F)) | ACQ_REL | (F & CON)
 let crel = REL | (SC & (W | F)) | ACQ_REL
 let ccon = R & CON
 
-let fr = rf^-1 ; mo
+// To be compatible with reads from uninit memory, we use our default definition of fr
+//let fr = rf^-1 ; mo
 
 let dd = (data | addr)+
 
@@ -68,7 +74,9 @@ acyclic hb as Hb
 (* coherent_memory_use *)
 let hbl = hb & loc
 
-irreflexive ((rf^-1)? ; mo ; rf? ; hb) as Coh
+// irreflexive ((rf^-1)? ; mo ; rf? ; hb) as Coh
+// To support reads from uninitialized memory
+irreflexive ((fr | mo) ; rf? ; hb) as Coh
 
 (* visible_side_effect_set *)
 let vis = (hbl & (W * R)) \ (hbl; [W] ; hbl)

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java

@@ -15,6 +15,8 @@ public class OptionNames {
     // Modeling Options
     public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds";
     public static final String RECURSION_BOUND = "modeling.recursionBound";
+    public static final String MEMORY_IS_ZEROED = "modeling.memoryIsZeroed";
+    public static final String INIT_DYNAMIC_ALLOCATIONS = "modeling.initDynamicAllocations";
 
     // Compilation Options
     public static final String USE_RC11_TO_ARCH_SCHEME = "compilation.rc11ToArch";

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java

@@ -10,6 +10,7 @@
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.FenceWithId;
+import com.dat3m.dartagnan.program.event.core.Load;
 import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
 import com.dat3m.dartagnan.program.event.core.RMWStoreExclusive;
 import com.dat3m.dartagnan.program.filter.Filter;
@@ -35,6 +36,7 @@
 import java.util.*;
 
 import static com.dat3m.dartagnan.configuration.OptionNames.ENABLE_ACTIVE_SETS;
+import static com.dat3m.dartagnan.configuration.OptionNames.MEMORY_IS_ZEROED;
 import static com.dat3m.dartagnan.program.event.Tag.*;
 import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF;
 import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference;
@@ -54,6 +56,13 @@ public class WmmEncoder implements Encoder {
             secure = true)
     private boolean enableActiveSets = true;
 
+    @Option(name = MEMORY_IS_ZEROED,
+            description = "Assumes the whole memory is zeroed before the program runs." +
+                    "In particular, if set to TRUE, reads from uninitialized memory will return zero." +
+                    "Otherwise, uninitialized memory has a nondeterministic value.",
+            secure = true)
+    private boolean memoryIsZeroed = true;
+
     // =====================================================================
 
     private WmmEncoder(EncodingContext c) {
@@ -65,6 +74,7 @@ public static WmmEncoder withContext(EncodingContext context) throws InvalidConf
         WmmEncoder encoder = new WmmEncoder(context);
         context.getTask().getConfig().inject(encoder);
         logger.info("{}: {}", ENABLE_ACTIVE_SETS, encoder.enableActiveSets);
+        logger.info("{}: {}", MEMORY_IS_ZEROED, encoder.memoryIsZeroed);
         long t0 = System.currentTimeMillis();
         if (encoder.enableActiveSets) {
             encoder.initializeEncodeSets();
@@ -508,7 +518,7 @@ public Void visitSameLocation(SameLocation locDef) {
         public Void visitReadFrom(ReadFrom rfDef) {
             final Relation rf = rfDef.getDefinedRelation();
             Map<MemoryEvent, List<BooleanFormula>> edgeMap = new HashMap<>();
-            EncodingContext.EdgeEncoder edge = context.edge(rf);
+            final EncodingContext.EdgeEncoder edge = context.edge(rf);
             ra.getKnowledge(rf).getMaySet().apply((e1, e2) -> {
                 MemoryCoreEvent w = (MemoryCoreEvent) e1;
                 MemoryCoreEvent r = (MemoryCoreEvent) e2;
@@ -518,26 +528,35 @@ public Void visitReadFrom(ReadFrom rfDef) {
                 edgeMap.computeIfAbsent(r, key -> new ArrayList<>()).add(e);
                 enc.add(bmgr.implication(e, bmgr.and(execution(w, r), sameAddress, sameValue)));
             });
-            for (MemoryEvent r : edgeMap.keySet()) {
-                List<BooleanFormula> edges = edgeMap.get(r);
+            for (Load r : program.getThreadEvents(Load.class)) {
+                final BooleanFormula uninit = getUninitReadVar(r);
+                if (memoryIsZeroed) {
+                    enc.add(bmgr.implication(uninit, context.equalZero(context.value(r))));
+                }
+
+                final List<BooleanFormula> rfEdges = edgeMap.getOrDefault(r, List.of());
                 if (GlobalSettings.ALLOW_MULTIREADS) {
-                    enc.add(bmgr.implication(context.execution(r), bmgr.or(edges)));
+                    enc.add(bmgr.implication(context.execution(r), bmgr.or(bmgr.or(rfEdges), uninit)));
                     continue;
                 }
-                int num = edges.size();
+
                 String rPrefix = "s(" + RF + ",E" + r.getGlobalId() + ",";
-                BooleanFormula lastSeqVar = edges.get(0);
-                for (int i = 1; i < num; i++) {
+                BooleanFormula lastSeqVar = uninit;
+                for (int i = 0; i < rfEdges.size(); i++) {
                     BooleanFormula newSeqVar = bmgr.makeVariable(rPrefix + i + ")");
-                    enc.add(bmgr.equivalence(newSeqVar, bmgr.or(lastSeqVar, edges.get(i))));
-                    enc.add(bmgr.not(bmgr.and(edges.get(i), lastSeqVar)));
+                    enc.add(bmgr.equivalence(newSeqVar, bmgr.or(lastSeqVar, rfEdges.get(i))));
+                    enc.add(bmgr.not(bmgr.and(rfEdges.get(i), lastSeqVar)));
                     lastSeqVar = newSeqVar;
                 }
                 enc.add(bmgr.implication(context.execution(r), lastSeqVar));
             }
             return null;
         }
 
+        private BooleanFormula getUninitReadVar(Load load) {
+            return bmgr.makeVariable("uninit_read " + load.getGlobalId());
+        }
+
         @Override
         public Void visitCoherence(Coherence coDef) {
             final Relation co = coDef.getDefinedRelation();

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java

@@ -514,7 +514,7 @@ public Expression visitAllocaInst(AllocaInstContext ctx) {
         }
         //final int alignment = parseAlignment(ctx.align());
         //final int addressSpace = parseAddressSpace(ctx.addrSpace());
-        block.events.add(EventFactory.newAlloc(register, elementType, sizeExpression, false));
+        block.events.add(EventFactory.newAlloc(register, elementType, sizeExpression, false, false));
         return register;
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

@@ -89,8 +89,9 @@ public static List<Event> eventSequence(Object... events) {
 
     // ------------------------------------------ Memory events ------------------------------------------
 
-    public static Alloc newAlloc(Register register, Type allocType, Expression arraySize, boolean isHeapAlloc) {
-        return new Alloc(register, allocType, arraySize, isHeapAlloc);
+    public static Alloc newAlloc(Register register, Type allocType, Expression arraySize,
+                                 boolean isHeapAlloc, boolean doesZeroOutMemory) {
+        return new Alloc(register, allocType, arraySize, isHeapAlloc, doesZeroOutMemory);
     }
 
     public static Load newLoad(Register register, Expression address) {

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java

@@ -1,6 +1,5 @@
 package com.dat3m.dartagnan.program.event.lang;
 
-import com.dat3m.dartagnan.encoding.EncodingContext;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.ExpressionVisitor;
@@ -13,7 +12,6 @@
 import com.dat3m.dartagnan.program.event.RegReader;
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.google.common.base.Preconditions;
-import org.sosy_lab.java_smt.api.BooleanFormula;
 
 import java.math.BigInteger;
 import java.util.HashSet;
@@ -31,14 +29,17 @@ public class Alloc extends AbstractEvent implements RegReader, RegWriter {
     private Type allocationType;
     private Expression arraySize;
     private boolean isHeapAllocation;
+    private boolean doesZeroOutMemory;
 
-    public Alloc(Register resultRegister, Type allocType, Expression arraySize, boolean isHeapAllocation) {
+    public Alloc(Register resultRegister, Type allocType, Expression arraySize, boolean isHeapAllocation,
+                 boolean doesZeroOutMemory) {
         Preconditions.checkArgument(resultRegister.getType() == TypeFactory.getInstance().getArchType());
         Preconditions.checkArgument(arraySize.getType() instanceof IntegerType);
         this.resultRegister = resultRegister;
         this.arraySize = arraySize;
         this.allocationType = allocType;
         this.isHeapAllocation = isHeapAllocation;
+        this.doesZeroOutMemory = doesZeroOutMemory;
     }
 
     protected Alloc(Alloc other) {
@@ -47,6 +48,7 @@ protected Alloc(Alloc other) {
         this.allocationType = other.allocationType;
         this.arraySize = other.arraySize;
         this.isHeapAllocation = other.isHeapAllocation;
+        this.doesZeroOutMemory = other.doesZeroOutMemory;
     }
 
     @Override
@@ -57,10 +59,12 @@ protected Alloc(Alloc other) {
     public Type getAllocationType() { return allocationType; }
     public Expression getArraySize() { return arraySize; }
     public boolean isHeapAllocation() { return isHeapAllocation; }
+    public boolean doesZeroOutMemory() { return doesZeroOutMemory; }
 
     public boolean isSimpleAllocation() { return (arraySize instanceof IntLiteral size && size.isOne()); }
     public boolean isArrayAllocation() { return !isSimpleAllocation(); }
 
+
     public Expression getAllocationSize() {
         final ExpressionFactory expressions = ExpressionFactory.getInstance();
         final TypeFactory types = TypeFactory.getInstance();
@@ -99,9 +103,4 @@ protected String defaultString() {
 
     @Override
     public Alloc getCopy() { return new Alloc(this); }
-
-    @Override
-    public BooleanFormula encodeExec(EncodingContext context) {
-        throw new UnsupportedOperationException("Cannot encode alloc events.");
-    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java

@@ -13,7 +13,6 @@
 import java.util.Set;
 
 import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkState;
 
 /**
  * Associated with an array of memory locations.
@@ -55,9 +54,7 @@ public class MemoryObject extends LeafExpressionBase<IntegerType> {
     public boolean isStaticallyAllocated() { return isStatic; }
     public boolean isDynamicallyAllocated() { return !isStatic; }
 
-    // Should only be called for statically allocated objects.
-    public Set<Integer> getStaticallyInitializedFields() {
-        checkState(this.isStaticallyAllocated(), "Unexpected dynamic object %s", this);
+    public Set<Integer> getInitializedFields() {
         return initialValues.keySet();
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java

@@ -36,7 +36,7 @@ public void run(Program program) {
         }
 
         for (MemoryObject memoryObject : program.getMemory().getObjects()) {
-            for (int field : memoryObject.getStaticallyInitializedFields()) {
+            for (int field : memoryObject.getInitializedFields()) {
                 memoryObject.setInitialValue(field, memoryObject.getInitialValue(field).accept(transformer));
             }
         }