diff --git a/benchmarks/mixed/lockref-par1.c b/benchmarks/mixed/lockref-par1.c new file mode 100644 index 0000000000..5dba302154 --- /dev/null +++ b/benchmarks/mixed/lockref-par1.c @@ -0,0 +1,48 @@ +#include +#include +#include +#include "lockref.h" + +#ifndef NTHREADS +#define NTHREADS 2 +#endif + +struct lockref my_lockref; + +void *get(void *unused) { + + lockref_get(&my_lockref); + + return NULL; +} + +void *ret(void *unused) { + + lockref_put_return(&my_lockref); + + return NULL; +} + +int main() { + + pthread_t g[NTHREADS]; + pthread_t r[NTHREADS]; + + atomic_store(&my_lockref.lock_count, 0); + + for (int i = 0; i < NTHREADS; i++) + pthread_create(&g[i], 0, get, (void *)(size_t)i); + for (int i = 0; i < NTHREADS; i++) + pthread_create(&r[i], 0, ret, (void *)(size_t)i); + + for (int i = 0; i < NTHREADS; i++) + pthread_join(g[i], 0); + assert(my_lockref.count >= 0); + assert(my_lockref.count <= NTHREADS); + + for (int i = 0; i < NTHREADS; i++) + pthread_join(r[i], 0); + assert(my_lockref.count == 0); // Wrong since some decrement might have no effect if there is no matching increment + + return 0; +} \ No newline at end of file diff --git a/benchmarks/mixed/lockref-par2.c b/benchmarks/mixed/lockref-par2.c new file mode 100644 index 0000000000..ee92b5504a --- /dev/null +++ b/benchmarks/mixed/lockref-par2.c @@ -0,0 +1,47 @@ +#include +#include +#include +#include "lockref.h" + +#ifndef NTHREADS +#define NTHREADS 2 +#endif + +struct lockref my_lockref; + +void *get(void *unused) { + + lockref_get(&my_lockref); + + return NULL; +} + +void *ret(void *unused) { + + lockref_put_return(&my_lockref); + + return NULL; +} + +int main() { + + pthread_t g[NTHREADS]; + pthread_t r[NTHREADS]; + + atomic_store(&my_lockref.lock_count, 0); + + for (int i = 0; i < NTHREADS; i++) + pthread_create(&g[i], 0, get, (void *)(size_t)i); + for (int i = 0; i < NTHREADS; i++) + pthread_create(&r[i], 0, ret, (void *)(size_t)i); + + for (int i = 0; i < NTHREADS; i++) + pthread_join(g[i], 0); + assert(my_lockref.count >= 0); // Correct since decrements fail if counter is zero + assert(my_lockref.count <= NTHREADS); // Correct because if all increments come first we get == NTHREADS + + for (int i = 0; i < NTHREADS; i++) + pthread_join(r[i], 0); + + return 0; +} \ No newline at end of file diff --git a/benchmarks/mixed/lockref-par3.c b/benchmarks/mixed/lockref-par3.c new file mode 100644 index 0000000000..4ffd018c21 --- /dev/null +++ b/benchmarks/mixed/lockref-par3.c @@ -0,0 +1,46 @@ +#include +#include +#include +#include "lockref.h" + +#ifndef NTHREADS +#define NTHREADS 2 +#endif + +struct lockref my_lockref; + +void *get(void *unused) { + + lockref_get(&my_lockref); + + return NULL; +} + +void *ret(void *unused) { + + lockref_put_return(&my_lockref); + + return NULL; +} + +int main() { + + pthread_t g[NTHREADS]; + pthread_t r[NTHREADS]; + + atomic_store(&my_lockref.lock_count, 0); + + for (int i = 0; i < NTHREADS; i++) + pthread_create(&g[i], 0, get, (void *)(size_t)i); + for (int i = 0; i < NTHREADS; i++) + pthread_create(&r[i], 0, ret, (void *)(size_t)i); + + for (int i = 0; i < NTHREADS; i++) + pthread_join(g[i], 0); + assert(my_lockref.count == NTHREADS); // Wrong, increment and decrement can be interleaved + + for (int i = 0; i < NTHREADS; i++) + pthread_join(r[i], 0); + + return 0; +} \ No newline at end of file diff --git a/benchmarks/mixed/lockref-seq.c b/benchmarks/mixed/lockref-seq.c new file mode 100644 index 0000000000..71ef565005 --- /dev/null +++ b/benchmarks/mixed/lockref-seq.c @@ -0,0 +1,46 @@ +#include +#include +#include +#include "lockref.h" + +#ifndef NTHREADS +#define NTHREADS 2 +#endif + +struct lockref my_lockref; + +void *get(void *unused) { + + lockref_get(&my_lockref); + + return NULL; +} + +void *ret(void *unused) { + + lockref_put_return(&my_lockref); + + return NULL; +} + +int main() { + + pthread_t g[NTHREADS]; + pthread_t r[NTHREADS]; + + atomic_store(&my_lockref.lock_count, 0); + + for (int i = 0; i < NTHREADS; i++) + pthread_create(&g[i], 0, get, (void *)(size_t)i); + for (int i = 0; i < NTHREADS; i++) + pthread_join(g[i], 0); + assert(my_lockref.count == NTHREADS); // Correct since all get first + + for (int i = 0; i < NTHREADS; i++) + pthread_create(&r[i], 0, ret, (void *)(size_t)i); + for (int i = 0; i < NTHREADS; i++) + pthread_join(r[i], 0); + assert(my_lockref.count == 0); // Correct since every decrement has a matching increment + + return 0; +} \ No newline at end of file diff --git a/benchmarks/mixed/lockref.h b/benchmarks/mixed/lockref.h new file mode 100644 index 0000000000..705b0b1564 --- /dev/null +++ b/benchmarks/mixed/lockref.h @@ -0,0 +1,67 @@ +#include +#include +#include +#include "spinlock.c" + +#define CMPXCHG_LOOP(CODE, SUCCESS) do { \ + struct lockref old; \ + old.lock_count = atomic_load(&lockref->lock_count); \ + while (old.lock.lock == 0) { \ + struct lockref new = old; \ + CODE \ + if (atomic_compare_exchange_strong(&lockref->lock_count, \ + (int64_t *) &old.lock_count, \ + new.lock_count)) { \ + SUCCESS; \ + } \ + } \ +} while (0) + +struct lockref { + union { + _Atomic(int64_t) lock_count; + struct { + spinlock_t lock; + _Atomic(int32_t) count; + }; + }; +}; + +/** + * lockref_get - Increments reference count unconditionally + * @lockref: pointer to lockref structure + * + * This operation is only valid if you already hold a reference + * to the object, so you know the count cannot be zero. + */ +void lockref_get(struct lockref *lockref) +{ + CMPXCHG_LOOP( + new.count++; + , + return; + ); + + spin_lock(&lockref->lock); + lockref->count++; + spin_unlock(&lockref->lock); +} + +/** + * lockref_put_return - Decrement reference count if possible + * @lockref: pointer to lockref structure + * + * Decrement the reference count and return the new value. + * If the lockref was dead or locked, return an error. + */ +int lockref_put_return(struct lockref *lockref) +{ + CMPXCHG_LOOP( + new.count--; + if (old.count <= 0) + return -1; + , + return new.count; + ); + return -1; +} \ No newline at end of file diff --git a/benchmarks/mixed/lockref1.c b/benchmarks/mixed/lockref1.c new file mode 100644 index 0000000000..191f4ab471 --- /dev/null +++ b/benchmarks/mixed/lockref1.c @@ -0,0 +1,103 @@ +#include +#include +#include + + +#ifndef NTHREADS +#define NTHREADS 3 +#endif + +// ========================================== +// Spinlock +// ========================================== + +struct spinlock_s { + _Atomic(int32_t) lock; +}; +typedef struct spinlock_s spinlock_t; + +void await_for_lock(struct spinlock_s *l) +{ + while (atomic_load_explicit(&l->lock, memory_order_relaxed) != 0); + return; +} + +int try_get_lock(struct spinlock_s *l) +{ + int val = 0; + return atomic_compare_exchange_strong_explicit(&l->lock, &val, 1, memory_order_acquire, memory_order_acquire); +} + +void spin_lock(struct spinlock_s *l) +{ + do { + await_for_lock(l); + } while(!try_get_lock(l)); + return; +} + +void spin_unlock(struct spinlock_s *l) +{ + atomic_store_explicit(&l->lock, 0, memory_order_release); +} + +// ========================================== +// Lockref +// ========================================== + +typedef struct { + union { + struct { + atomic_int lock; + int count; + }; + atomic_long lock_count; + }; +} lockref_t; + +void lockref_get(lockref_t *lockref) { + long old_val = atomic_load_explicit(&lockref->lock_count, memory_order_relaxed); + + while (((lockref_t *)&old_val)->lock == 0) { + long new_val = old_val; + ((lockref_t *)&new_val)->count++; + if (atomic_compare_exchange_strong_explicit( + &lockref->lock_count, &old_val, new_val, + memory_order_relaxed, memory_order_relaxed)) { + return; + } + } + + spin_lock(&lockref->lock); + lockref->count++; + spin_unlock(&lockref->lock); +} + +// ========================================== +// Main +// ========================================== + +lockref_t my_lockref; + +void *thread_n(void *unsued) { + + lockref_get(&my_lockref); + + return NULL; +} + +int main() { + + pthread_t t[NTHREADS]; + + atomic_store(&my_lockref.lock_count, 0); + + for (int i = 0; i < NTHREADS; i++) + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); + + for (int i = 0; i < NTHREADS; i++) + pthread_join(t[i], 0); + + assert(my_lockref.count == NTHREADS); + return 0; +} \ No newline at end of file diff --git a/benchmarks/mixed/lockref2.c b/benchmarks/mixed/lockref2.c new file mode 100644 index 0000000000..f535a73638 --- /dev/null +++ b/benchmarks/mixed/lockref2.c @@ -0,0 +1,101 @@ +#include +#include +#include + +#ifndef NTHREADS +#define NTHREADS 3 +#endif + +// ========================================== +// Spinlock +// ========================================== + +struct spinlock_s { + _Atomic(int32_t) lock; +}; +typedef struct spinlock_s spinlock_t; + +void await_for_lock(struct spinlock_s *l) +{ + while (atomic_load_explicit(&l->lock, memory_order_relaxed) != 0); + return; +} + +int try_get_lock(struct spinlock_s *l) +{ + int val = 0; + return atomic_compare_exchange_strong_explicit(&l->lock, &val, 1, memory_order_acquire, memory_order_acquire); +} + +void spin_lock(struct spinlock_s *l) +{ + do { + await_for_lock(l); + } while(!try_get_lock(l)); + return; +} + +void spin_unlock(struct spinlock_s *l) +{ + atomic_store_explicit(&l->lock, 0, memory_order_release); +} + +// ========================================== +// Lockref +// ========================================== + +struct lockref { + union { + _Atomic(int64_t) lock_count; + struct { + spinlock_t lock; + _Atomic(int32_t) count; + }; + }; +}; + +void lockref_get(struct lockref *lockref) { + struct lockref old; + + old.lock_count = atomic_load_explicit(&lockref->lock_count, memory_order_relaxed); + while (old.lock.lock == 0) { + struct lockref new = old; + new.count++; + if (atomic_compare_exchange_strong_explicit(&lockref->lock_count, (int64_t *) &old.lock_count, new.lock_count, memory_order_relaxed, memory_order_relaxed)) { + return; + } + } + + spin_lock(&lockref->lock); + lockref->count++; + spin_unlock(&lockref->lock); +} + +// ========================================== +// Main +// ========================================== + +struct lockref my_lockref; + +void *thread_n(void *unsued) { + + lockref_get(&my_lockref); + + return NULL; +} + +int main() { + + pthread_t t[NTHREADS]; + + atomic_store(&my_lockref.lock_count, 0); + + for (int i = 0; i < NTHREADS; i++) + pthread_create(&t[i], 0, thread_n, (void *)(size_t)i); + + for (int i = 0; i < NTHREADS; i++) + pthread_join(t[i], 0); + + assert(my_lockref.count == NTHREADS); + return 0; +} \ No newline at end of file diff --git a/benchmarks/mixed/mixed-local.c b/benchmarks/mixed/mixed-local.c new file mode 100644 index 0000000000..676dd3e0db --- /dev/null +++ b/benchmarks/mixed/mixed-local.c @@ -0,0 +1,20 @@ +#include +// Issue: Mixed-size access on a thread-local variable. ProgramProcessor Mem2Reg should promote x, if performed after Tearing. +// Expected: PASS if mixedSize enabled, else undefined + +int main() +{ + union { int as_int; short as_short; } x; + x.as_int = 0x1e240; + x.as_short = 0; +#ifdef __LITTLE_ENDIAN__ + __VERIFIER_assert(x.as_int == 0x10000); +#else +#ifdef __BIG_ENDIAN__ + __VERIFIER_assert(x.as_int == 0xe240); +#else +#error Undefined byte order +#endif +#endif + return 0; +} diff --git a/benchmarks/mixed/spinlock.c b/benchmarks/mixed/spinlock.c new file mode 100644 index 0000000000..599e07ca77 --- /dev/null +++ b/benchmarks/mixed/spinlock.c @@ -0,0 +1,31 @@ +#include + +struct spinlock_s { + _Atomic(int32_t) lock; +}; +typedef struct spinlock_s spinlock_t; + +void await_for_lock(struct spinlock_s *l) +{ + while (atomic_load_explicit(&l->lock, memory_order_relaxed) != 0); + return; +} + +int try_get_lock(struct spinlock_s *l) +{ + int val = 0; + return atomic_compare_exchange_strong_explicit(&l->lock, &val, 1, memory_order_acquire, memory_order_acquire); +} + +void spin_lock(struct spinlock_s *l) +{ + do { + await_for_lock(l); + } while(!try_get_lock(l)); + return; +} + +void spin_unlock(struct spinlock_s *l) +{ + atomic_store_explicit(&l->lock, 0, memory_order_release); +} \ No newline at end of file diff --git a/cat/aarch64.cat b/cat/aarch64.cat index 4b76cc212a..b05b1e7ce4 100644 --- a/cat/aarch64.cat +++ b/cat/aarch64.cat @@ -1,12 +1,18 @@ (* - * The ARMv8 Application Level Memory Model. + * The Armv8 Application Level Memory Model. * - * See section B2.3 of the ARMv8 ARM: + * This is a machine-readable, executable and formal artefact, which aims to be + * the latest stable version of the Armv8 memory model. + * If you have comments on the content of this file, please send an email to + * jade.alglave@arm.com, referring to version number: + * 814a6fc1610ec1a24f2cbd178e171966375626ac + * For a textual version of the model, see section B2.3 of the Armv8 ARM: * https://developer.arm.com/docs/ddi0487/latest/arm-architecture-reference-manual-armv8-for-armv8-a-architecture-profile * * Author: Will Deacon + * Author: Jade Alglave * - * Copyright (C) 2016, ARM Ltd. + * Copyright (C) 2016-2020, Arm Ltd. * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -44,10 +50,10 @@ * location and then consequently defines the fr relation using co and * rf. *) -include "cos.cat" +include "coscat.cat" (* - * Include aarch64fences.cat so that barriers show up in generated diagrams. + * Include aarch64fences.cat to define barriers. *) include "aarch64fences.cat" @@ -79,32 +85,40 @@ flag ~empty (dmb.full | dmb.ld | dmb.st) \ (* Coherence-after *) let ca = fr | co +(* Local read successor *) +let lrs = [W]; (po-loc \ (po-loc;[W];po-loc)) ; [R] + +(* Local write successor *) +let lws = po-loc; [W] + (* Observed-by *) let obs = rfe | fre | coe (* Dependency-ordered-before *) -let dob = addr | data +let dob = (addr | data) | ctrl; [W] | (ctrl | (addr; po)); [ISB]; po; [R] | addr; po; [W] - | (ctrl | data); coi - | (addr | data); rfi + | (addr | data); lrs (* Atomic-ordered-before *) let aob = rmw - | [range(rmw)]; rfi; [A | Q] + | [range(rmw)]; lrs; [A | Q] (* Barrier-ordered-before *) let bob = po; [dmb.full]; po + | po; ([A];amo;[L]); po | [L]; po; [A] | [R]; po; [dmb.ld]; po | [A | Q]; po | [W]; po; [dmb.st]; po; [W] | po; [L] - | po; [L]; coi + +(* Locally-ordered-before *) +let lob = lws; si | dob | aob | bob (* Ordered-before *) -let ob = obs | dob | aob | bob +let ob = obs; si | lob (* Internal visibility requirement *) acyclic po-loc | ca | rf as internal diff --git a/cat/stdlib.cat b/cat/stdlib.cat index a9c1120d8d..c0179c20a3 100644 --- a/cat/stdlib.cat +++ b/cat/stdlib.cat @@ -1,6 +1,7 @@ let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W] let po-loc = po & loc +let rmw = amo | lxsx let rfe = rf & ext let coe = co & ext diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4 index bae408b323..1c8f2d4710 100644 --- a/dartagnan/src/main/antlr4/LitmusAArch64.g4 +++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4 @@ -4,7 +4,6 @@ import LitmusAssertions; @header{ import com.dat3m.dartagnan.expression.integers.*; -import static com.dat3m.dartagnan.program.event.Tag.ARMv8.*; } main @@ -16,26 +15,17 @@ variableDeclaratorList ; variableDeclarator - : variableDeclaratorLocation - | variableDeclaratorRegister - | variableDeclaratorRegisterLocation - | variableDeclaratorLocationLocation + : type location (Equals constant)? #typedVariableDeclarator + | type location LBracket constant RBracket #typedArrayDeclarator + | location Equals constant #variableDeclaratorLocation + | location Equals Amp? location #variableDeclaratorLocationLocation + | type threadId Colon register64 (Equals constant)? #typedRegisterDeclarator + | threadId Colon register64 Equals constant #variableDeclaratorRegister + | threadId Colon register64 Equals Amp? location #variableDeclaratorRegisterLocation ; -variableDeclaratorLocation - : location Equals constant - ; - -variableDeclaratorRegister - : threadId Colon register64 Equals constant - ; - -variableDeclaratorRegisterLocation - : threadId Colon register64 Equals Amp? location - ; - -variableDeclaratorLocationLocation - : location Equals Amp? location +type + : Identifier ; variableList @@ -68,9 +58,12 @@ instruction | mov | arithmetic | load + | loadPair | loadExclusive | store + | storePair | storeExclusive + | swap | cmp | branch | branchRegister @@ -80,39 +73,54 @@ instruction | nop ; -mov locals [String rD, int size] - : MovInstruction r32 = register32 Comma expr32 {$rD = $r32.id; $size = 32;} - | MovInstruction r64 = register64 Comma expr64 {$rD = $r64.id; $size = 64;} +mov + : MovInstruction r32 = register32 Comma expr32 + | MovInstruction r64 = register64 Comma expr64 + ; + +cmp + : CmpInstruction r32 = register32 Comma expr32 + | CmpInstruction r64 = register64 Comma expr64 + ; + +arithmetic + : arithmeticInstruction rD32 = register32 Comma rV32 = register32 Comma expr32 + | arithmeticInstruction rD64 = register64 Comma rV64 = register64 Comma expr64 + ; + +load + : loadInstruction rD32 = register32 Comma LBracket address RBracket + | loadInstruction rD64 = register64 Comma LBracket address RBracket ; -cmp locals [String rD, int size] - : CmpInstruction r32 = register32 Comma expr32 {$rD = $r32.id; $size = 32;} - | CmpInstruction r64 = register64 Comma expr64 {$rD = $r64.id; $size = 64;} +loadPair + : LDP rD032 = register32 Comma rD132 = register32 Comma LBracket address RBracket + | LDP rD064 = register64 Comma rD164 = register64 Comma LBracket address RBracket ; -arithmetic locals [String rD, String rV, int size] - : arithmeticInstruction rD32 = register32 Comma rV32 = register32 Comma expr32 {$rD = $rD32.id; $rV = $rV32.id; $size = 32;} - | arithmeticInstruction rD64 = register64 Comma rV64 = register64 Comma expr64 {$rD = $rD64.id; $rV = $rV64.id; $size = 64;} +loadExclusive + : loadExclusiveInstruction rD32 = register32 Comma LBracket address RBracket + | loadExclusiveInstruction rD64 = register64 Comma LBracket address RBracket ; -load locals [String rD, int size] - : loadInstruction rD32 = register32 Comma LBracket address (Comma offset)? RBracket {$rD = $rD32.id; $size = 32;} - | loadInstruction rD64 = register64 Comma LBracket address (Comma offset)? RBracket {$rD = $rD64.id; $size = 64;} +store + : storeInstruction rV32 = register32 Comma LBracket address RBracket + | storeInstruction rV64 = register64 Comma LBracket address RBracket ; -loadExclusive locals [String rD, int size] - : loadExclusiveInstruction rD32 = register32 Comma LBracket address (Comma offset)? RBracket {$rD = $rD32.id; $size = 32;} - | loadExclusiveInstruction rD64 = register64 Comma LBracket address (Comma offset)? RBracket {$rD = $rD64.id; $size = 64;} +storePair + : STP r032 = register32 Comma r132 = register32 Comma LBracket address RBracket + | STP r064 = register64 Comma r164 = register64 Comma LBracket address RBracket ; -store locals [String rV, int size] - : storeInstruction rV32 = register32 Comma LBracket address (Comma offset)? RBracket {$rV = $rV32.id; $size = 32;} - | storeInstruction rV64 = register64 Comma LBracket address (Comma offset)? RBracket {$rV = $rV64.id; $size = 64;} +storeExclusive + : storeExclusiveInstruction rS32 = register32 Comma rV32 = register32 Comma LBracket address RBracket + | storeExclusiveInstruction rS32 = register32 Comma rV64 = register64 Comma LBracket address RBracket ; -storeExclusive locals [String rS, String rV, int size] - : storeExclusiveInstruction rS32 = register32 Comma rV32 = register32 Comma LBracket address (Comma offset)? RBracket {$rS = $rS32.id; $rV = $rV32.id; $size = 32;} - | storeExclusiveInstruction rS32 = register32 Comma rV64 = register64 Comma LBracket address (Comma offset)? RBracket {$rS = $rS32.id; $rV = $rV64.id; $size = 64;} +swap + : swapInstruction rS32 = register32 Comma rD32 = register32 Comma LBracket address RBracket + | swapInstruction rS64 = register64 Comma rD64 = register64 Comma LBracket address RBracket ; fence locals [String opt] @@ -141,24 +149,55 @@ nop : Nop ; -loadInstruction locals [String mo] - : LDR {$mo = MO_RX;} - | LDAR {$mo = MO_ACQ;} - ; - -loadExclusiveInstruction locals [String mo] - : LDXR {$mo = MO_RX;} - | LDAXR {$mo = MO_ACQ;} - ; - -storeInstruction locals [String mo] - : STR {$mo = MO_RX;} - | STLR {$mo = MO_REL;} - ; - -storeExclusiveInstruction locals [String mo] - : STXR {$mo = MO_RX;} - | STLXR {$mo = MO_REL;} +loadInstruction locals [boolean acquire, boolean byteSize, boolean halfWordSize] + : LDR + | LDRB {$byteSize = true;} + | LDRH {$halfWordSize = true;} + | LDAR {$acquire = true;} + | LDARB {$acquire = true; $byteSize = true;} + | LDARH {$acquire = true; $halfWordSize = true;} + ; + +loadExclusiveInstruction locals [boolean acquire, boolean byteSize, boolean halfWordSize] + : LDXR + | LDXRB {$byteSize = true;} + | LDXRH {$halfWordSize = true;} + | LDAXR {$acquire = true;} + | LDAXRB {$acquire = true; $byteSize = true;} + | LDAXRH {$acquire = true; $halfWordSize = true;} + ; + +storeInstruction locals [boolean release, boolean byteSize, boolean halfWordSize] + : STR + | STRB {$byteSize = true;} + | STRH {$halfWordSize = true;} + | STLR {$release = true;} + | STLRB {$release = true; $byteSize = true;} + | STLRH {$release = true; $halfWordSize = true;} + ; + +storeExclusiveInstruction locals [boolean release, boolean byteSize, boolean halfWordSize] + : STXR + | STXRB {$byteSize = true;} + | STXRH {$halfWordSize = true;} + | STLXR {$release = true;} + | STLXRB {$release = true; $byteSize = true;} + | STLXRH {$release = true; $halfWordSize = true;} + ; + +swapInstruction locals [boolean acquire, boolean release, boolean byteSize, boolean halfWordSize] + : SWP + | SWPB {$byteSize = true;} + | SWPH {$halfWordSize = true;} + | SWPA {$acquire = true;} + | SWPAB {$acquire = true; $byteSize = true;} + | SWPAH {$acquire = true; $halfWordSize = true;} + | SWPL {$release = true;} + | SWPLB {$release = true; $byteSize = true;} + | SWPLH {$release = true; $halfWordSize = true;} + | SWPAL {$acquire = true; $release = true;} + | SWPALB {$acquire = true; $release = true; $byteSize = true;} + | SWPALH {$acquire = true; $release = true; $halfWordSize = true;} ; arithmeticInstruction locals [IntBinaryOp op] @@ -220,8 +259,13 @@ expr32 | expressionImmediate ; +address + : register64 (Comma offset)? + ; + offset : immediate + | register64 | expressionConversion ; @@ -241,12 +285,9 @@ expressionImmediate : immediate shift? ; -expressionConversion - : register32 Comma BitfieldOperator - ; - -address returns[String id] - : r = register64 {$id = $r.id;} +expressionConversion returns[boolean signed] + : register32 Comma UXTW {$signed = false;} + | register32 Comma SXTW {$signed = true;} ; register64 returns[String id] @@ -311,16 +352,49 @@ EON : 'EON' ; // Invert and XOR // Load instructions LDR : 'LDR' ; +LDRB : 'LDRB' ; +LDRH : 'LDRH' ; LDAR : 'LDAR' ; +LDARB : 'LDARB' ; +LDARH : 'LDARH' ; +LDP : 'LDP' ; LDXR : 'LDXR' ; +LDXRB : 'LDXRB' ; +LDXRH : 'LDXRH' ; LDAXR : 'LDAXR' ; +LDAXRB : 'LDAXRB' ; +LDAXRH : 'LDAXRH' ; // Store instructions STR : 'STR' ; +STRB : 'STRB' ; +STRH : 'STRH' ; STLR : 'STLR' ; +STLRB : 'STLRB' ; +STLRH : 'STLRH' ; +STP : 'STP' ; STXR : 'STXR' ; -STLXR : 'STLXR' ; +STXRB : 'STXRB' ; +STXRH : 'STXRH' ; +STLXR : 'STLXR' ; +STLXRB : 'STLXRB' ; +STLXRH : 'STLXRH' ; + +// Swap word instructions (~ Exchange) + +SWP : 'SWP' ; +SWPB : 'SWPB' ; +SWPH : 'SWPH' ; +SWPA : 'SWPA' ; +SWPAB : 'SWPAB' ; +SWPAH : 'SWPAH' ; +SWPL : 'SWPL' ; +SWPLB : 'SWPLB' ; +SWPLH : 'SWPLH' ; +SWPAL : 'SWPAL' ; +SWPALB : 'SWPALB' ; +SWPALH : 'SWPALH' ; MovInstruction : 'MOV' @@ -386,10 +460,8 @@ LSL : 'LSL'; // Logical shift left LSR : 'LSR'; // Logical shift right ASR : 'ASR'; // Arithmetic shift right (preserves sign bit) -BitfieldOperator - : 'UXTW' // Zero extends a 32-bit word (unsigned) - | 'SXTW' // Zero extends a 32-bit word (signed) - ; +UXTW : 'UXTW' ; // Zero extends a 32-bit word (unsigned) +SXTW : 'SXTW' ; // Zero extends a 32-bit word (signed) Register64 : 'X' DigitSequence diff --git a/dartagnan/src/main/antlr4/LitmusAssertions.g4 b/dartagnan/src/main/antlr4/LitmusAssertions.g4 index 8086c2d3b5..bcd1fdfc39 100644 --- a/dartagnan/src/main/antlr4/LitmusAssertions.g4 +++ b/dartagnan/src/main/antlr4/LitmusAssertions.g4 @@ -39,6 +39,7 @@ varName constant : Minus? DigitSequence + | hex=HexDigitSequence ; assertionListExpectationList @@ -136,6 +137,10 @@ Digit : [0-9] ; +HexDigitSequence + : '0x' [0-9a-fA-F]+ + ; + fragment Letter : [A-Za-z] diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index 81cdfe206d..9d6a1a53dd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -50,6 +50,7 @@ public class OptionNames { public static final String PROPAGATE_COPY_ASSIGNMENTS = "program.processing.propagateCopyAssignments"; public static final String REMOVE_ASSERTION_OF_TYPE = "program.processing.skipAssertionsOfType"; public static final String NONTERMINATION_INSTRUMENTATION = "program.processing.nonTermination"; + public static final String MIXED_SIZE = "program.processing.mixedSize"; // Program Property Options public static final String REACHING_DEFINITIONS_METHOD = "program.analysis.reachingDefinitions"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java index e58480cbbd..c9b0e3fe98 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -443,6 +443,37 @@ public TypedFormula visitIntCmpExpression(IntCmpExp } } + @Override + public TypedFormula visitIntConcat(IntConcat expr) { + Preconditions.checkArgument(!expr.getOperands().isEmpty()); + + if (context.useIntegers) { + throw new UnsupportedOperationException("Cannot encode bitwise concatenation on mathematical integers."); + } else { + final BitvectorFormulaManager bvmgr = bitvectorFormulaManager(); + final List operands = expr.getOperands(); + + BitvectorFormula enc = (BitvectorFormula) encodeIntegerExpr(operands.get(0)).formula(); + for (Expression op : operands.subList(1, operands.size())) { + enc = bvmgr.concat((BitvectorFormula) encodeIntegerExpr(op).formula(), enc); + } + return new TypedFormula<>(expr.getType(), enc); + } + } + + @Override + public TypedFormula visitIntExtract(IntExtract expr) { + if (context.useIntegers) { + // TODO: We could support this with modulo operations + throw new UnsupportedOperationException("Cannot extract bits from mathematical integers."); + } else { + final BitvectorFormulaManager bvmgr = bitvectorFormulaManager(); + final BitvectorFormula operandEnc = (BitvectorFormula) encodeIntegerExpr(expr.getOperand()).formula(); + final BitvectorFormula extract = bvmgr.extract(operandEnc, expr.getHighBit(), expr.getLowBit()); + return new TypedFormula(expr.getType(), extract); + } + } + // ==================================================================================== // Aggregates diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java index 454b1947b7..b051493c02 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java @@ -71,6 +71,11 @@ public Boolean visitProgramOrder(ProgramOrder definition) { return doUpdateSelf(definition); } + @Override + public Boolean visitSameInstruction(SameInstruction definition) { + return doUpdateSelf(definition); + } + @Override public Boolean visitControlDependency(DirectControlDependency definition) { return doUpdateSelf(definition); @@ -97,7 +102,12 @@ public Boolean visitLinuxCriticalSections(LinuxCriticalSections definition) { } @Override - public Boolean visitReadModifyWrites(ReadModifyWrites definition) { + public Boolean visitAMOPairs(AMOPairs definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitLXSXPairs(LXSXPairs definition) { return doUpdateSelf(definition); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index 1b245e250d..fbd4a324cf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -10,6 +10,7 @@ import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.core.NamedBarrier; import com.dat3m.dartagnan.program.event.core.RMWStoreExclusive; +import com.dat3m.dartagnan.program.event.core.InstructionBoundary; import com.dat3m.dartagnan.smt.ModelExt; import com.dat3m.dartagnan.utils.Utils; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; @@ -486,17 +487,32 @@ public Void visitLinuxCriticalSections(LinuxCriticalSections rscsDef) { } @Override - public Void visitReadModifyWrites(ReadModifyWrites rmwDef) { - final Relation rmw = rmwDef.getDefinedRelation(); + public Void visitLXSXPairs(LXSXPairs lxsxDef) { + final Relation rmw = lxsxDef.getDefinedRelation(); BooleanFormula unpredictable = bmgr.makeFalse(); final RelationAnalysis.Knowledge k = ra.getKnowledge(rmw); final Map> mayIn = k.getMaySet().getInMap(); final Map> mayOut = k.getMaySet().getOutMap(); + final Map siMap = new HashMap<>(); + for (InstructionBoundary end : program.getThreadEvents(InstructionBoundary.class)) { + final List events = end.getInstructionEvents().stream().filter(e -> e.hasTag(EXCL)).toList(); + for (Event event : events) { + siMap.put(event, events.get(0)); + } + } // ---------- Encode matching for LL/SC-type RMWs ---------- for (RMWStoreExclusive store : program.getThreadEvents(RMWStoreExclusive.class)) { - BooleanFormula storeExec = bmgr.makeFalse(); + final Event firstStore = siMap.getOrDefault(store, store); + if (!store.equals(firstStore)) { + enc.add(bmgr.equivalence(context.execution(store), context.execution(firstStore))); + continue; + } + final List storeExec = new ArrayList<>(); for (Event e : mayIn.getOrDefault(store, Set.of())) { + if (!e.equals(siMap.getOrDefault(e, e))) { + continue; + } MemoryCoreEvent load = (MemoryCoreEvent) e; BooleanFormula sameAddress = context.sameAddress(load, store); // Encode if load and store form an exclusive pair @@ -505,12 +521,14 @@ public Void visitReadModifyWrites(ReadModifyWrites rmwDef) { pairingCond.add(context.execution(load)); pairingCond.add(context.controlFlow(store)); for (Event otherLoad : mayIn.getOrDefault(store, Set.of())) { - if (otherLoad.getGlobalId() > load.getGlobalId()) { + if (otherLoad.getGlobalId() > load.getGlobalId() && + otherLoad.equals(siMap.getOrDefault(otherLoad, otherLoad))) { pairingCond.add(bmgr.not(context.execution(otherLoad))); } } for (Event otherStore : mayOut.getOrDefault(load, Set.of())) { - if (otherStore.getGlobalId() < store.getGlobalId()) { + if (otherStore.getGlobalId() < store.getGlobalId() && + otherStore.equals(siMap.getOrDefault(otherStore, otherStore))) { pairingCond.add(bmgr.not(context.controlFlow(otherStore))); } } @@ -524,9 +542,9 @@ public Void visitReadModifyWrites(ReadModifyWrites rmwDef) { unpredictable = bmgr.or(unpredictable, bmgr.and(context.execution(store), isPair, bmgr.not(sameAddress))); } enc.add(bmgr.equivalence(isPair, bmgr.and(pairingCond))); - storeExec = bmgr.or(storeExec, isPair); + storeExec.add(isPair); } - enc.add(bmgr.implication(context.execution(store), storeExec)); + enc.add(bmgr.implication(context.execution(store), bmgr.or(storeExec))); } // ---------- Encode actual RMW relation ---------- @@ -546,7 +564,7 @@ public Void visitReadModifyWrites(ReadModifyWrites rmwDef) { edge.encode(load, store), k.getMustSet().contains(load, store) ? execution(load, store) : // Relation between exclusive load and store - bmgr.and(context.execution(store), exclPair(load, store), sameAddress))); + bmgr.and(context.execution(store), exclPair(siMap.getOrDefault(load, load), siMap.getOrDefault(store, store)), sameAddress))); } }); enc.add(bmgr.equivalence(Flag.ARM_UNPREDICTABLE_BEHAVIOUR.repr(context.getFormulaManager()), unpredictable)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java index 02fb0741d7..5c77a6330d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java @@ -171,6 +171,14 @@ public Expression makeRshift(Expression leftOperand, Expression rightOperand, bo return makeIntBinary(leftOperand, signed ? IntBinaryOp.ARSHIFT : IntBinaryOp.RSHIFT, rightOperand); } + public Expression makeIntConcat(List operands) { + return new IntConcat(operands); + } + + public Expression makeIntExtract(Expression operand, int lowBit, int highBit) { + return new IntExtract(operand, lowBit, highBit); + } + public Expression makeIntUnary(IntUnaryOp operator, Expression operand) { return new IntUnaryExpr(operator, operand); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java index 2181e52d8e..308cad9c73 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionKind.java @@ -23,6 +23,8 @@ enum Other implements ExpressionKind { ITE, EXTRACT, INSERT, + BV_EXTRACT, + BV_CONCAT, FORMULA; @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java index 398193682b..ad586d43ee 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java @@ -7,13 +7,11 @@ import com.dat3m.dartagnan.expression.booleans.BoolUnaryOp; import com.dat3m.dartagnan.expression.floats.FloatSizeCast; import com.dat3m.dartagnan.expression.floats.IntToFloatCast; -import com.dat3m.dartagnan.expression.integers.FloatToIntCast; -import com.dat3m.dartagnan.expression.integers.IntBinaryOp; -import com.dat3m.dartagnan.expression.integers.IntSizeCast; -import com.dat3m.dartagnan.expression.integers.IntUnaryOp; +import com.dat3m.dartagnan.expression.integers.*; import com.dat3m.dartagnan.expression.misc.GEPExpr; import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Register; +import com.google.common.collect.Lists; import java.util.Objects; import java.util.Set; @@ -69,6 +67,16 @@ public String visitUnaryExpression(UnaryExpression expr) { return expr.getKind() + visit(expr.getOperand()); } + @Override + public String visitIntConcat(IntConcat expr) { + return Lists.reverse(expr.getOperands()).stream().map(this::visit).collect(Collectors.joining("::")); + } + + @Override + public String visitIntExtract(IntExtract expr) { + return String.format("%s[%d..%d]", expr.getOperand().accept(this), expr.getLowBit(), expr.getHighBit()); + } + @Override public String visitIntSizeCastExpression(IntSizeCast expr) { final String opName = expr.isTruncation() ? "trunc" : (expr.preservesSign() ? "sext" : "zext"); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java index 4c96f91430..3396f90063 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java @@ -30,6 +30,8 @@ public interface ExpressionVisitor { default TRet visitIntBinaryExpression(IntBinaryExpr expr) { return visitBinaryExpression(expr); } default TRet visitIntCmpExpression(IntCmpExpr expr) { return visitBinaryExpression(expr); } default TRet visitIntUnaryExpression(IntUnaryExpr expr) { return visitUnaryExpression(expr); } + default TRet visitIntConcat(IntConcat expr) { return visitExpression(expr); } + default TRet visitIntExtract(IntExtract expr) { return visitUnaryExpression(expr); } default TRet visitIntSizeCastExpression(IntSizeCast expr) { return visitCastExpression(expr); } default TRet visitFloatToIntCastExpression(FloatToIntCast expr) { return visitCastExpression(expr); } default TRet visitIntLiteral(IntLiteral lit) { return visitLeafExpression(lit); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntConcat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntConcat.java new file mode 100644 index 0000000000..d8e74d7c5f --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntConcat.java @@ -0,0 +1,33 @@ +package com.dat3m.dartagnan.expression.integers; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionKind; +import com.dat3m.dartagnan.expression.ExpressionVisitor; +import com.dat3m.dartagnan.expression.base.NaryExpressionBase; +import com.dat3m.dartagnan.expression.type.IntegerType; +import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.expression.utils.ExpressionHelper; +import com.google.common.collect.ImmutableList; + +import java.util.List; + +public class IntConcat extends NaryExpressionBase { + + public IntConcat(List operands) { + super(getConcatType(operands), ExpressionKind.Other.BV_CONCAT, ImmutableList.copyOf(operands)); + } + + private static IntegerType getConcatType(List operands) { + int size = 0; + for (Expression op : operands) { + ExpressionHelper.checkExpectedType(op, IntegerType.class); + size += ((IntegerType)op.getType()).getBitWidth(); + } + return TypeFactory.getInstance().getIntegerType(size); + } + + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visitIntConcat(this); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntExtract.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntExtract.java new file mode 100644 index 0000000000..3b2b373523 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntExtract.java @@ -0,0 +1,35 @@ +package com.dat3m.dartagnan.expression.integers; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionKind; +import com.dat3m.dartagnan.expression.ExpressionVisitor; +import com.dat3m.dartagnan.expression.base.UnaryExpressionBase; +import com.dat3m.dartagnan.expression.type.IntegerType; +import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.expression.utils.ExpressionHelper; +import com.google.common.base.Preconditions; + +public class IntExtract extends UnaryExpressionBase { + + private final int lowBit; + private final int highBit; + + public IntExtract(Expression operand, int lowBit, int highBit) { + super(TypeFactory.getInstance().getIntegerType(highBit - lowBit + 1), + ExpressionKind.Other.BV_EXTRACT, + operand); + ExpressionHelper.checkExpectedType(operand, IntegerType.class); + int originalWidth = ((IntegerType)operand.getType()).getBitWidth(); + Preconditions.checkArgument(0 <= lowBit && lowBit <= highBit && highBit < originalWidth); + this.lowBit = lowBit; + this.highBit = highBit; + } + + public int getLowBit() { return lowBit; } + public int getHighBit() { return highBit; } + + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visitIntExtract(this); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java index 44aa9e0723..0de47c05ba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java @@ -264,6 +264,8 @@ public Expression visitIntBinaryExpression(IntBinaryExpr expr) { return expressions.makeIntBinary(left, op, right); } + // TODO: Add simplifications for IntExtract and IntConcat expressions + @Override public Expression visitITEExpression(ITEExpr expr) { final Expression cond = expr.getCondition().accept(this); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java index f196c77802..f2213b26c1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java @@ -13,10 +13,7 @@ import com.dat3m.dartagnan.expression.floats.FloatBinaryExpr; import com.dat3m.dartagnan.expression.floats.FloatCmpExpr; import com.dat3m.dartagnan.expression.floats.FloatUnaryExpr; -import com.dat3m.dartagnan.expression.integers.IntBinaryExpr; -import com.dat3m.dartagnan.expression.integers.IntCmpExpr; -import com.dat3m.dartagnan.expression.integers.IntSizeCast; -import com.dat3m.dartagnan.expression.integers.IntUnaryExpr; +import com.dat3m.dartagnan.expression.integers.*; import com.dat3m.dartagnan.expression.misc.GEPExpr; import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.expression.type.TypeFactory; @@ -53,6 +50,16 @@ public Expression visitIntUnaryExpression(IntUnaryExpr expr) { return expressions.makeIntUnary(expr.getKind(), expr.getOperand().accept(this)); } + @Override + public Expression visitIntConcat(IntConcat expr) { + return expressions.makeIntConcat(expr.getOperands().stream().map(e -> e.accept(this)).toList()); + } + + @Override + public Expression visitIntExtract(IntExtract expr) { + return expressions.makeIntExtract(expr.getOperand().accept(this), expr.getLowBit(), expr.getHighBit()); + } + @Override public Expression visitIntSizeCastExpression(IntSizeCast expr) { return expressions.makeIntegerCast(expr.getOperand().accept(this), expr.getTargetType(), expr.preservesSign()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLlvm.java index 2c1702c08a..167ad1836e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/ParserLlvm.java @@ -3,8 +3,10 @@ import com.dat3m.dartagnan.exception.AbortErrorListener; import com.dat3m.dartagnan.parsers.LLVMIRLexer; import com.dat3m.dartagnan.parsers.LLVMIRParser; +import com.dat3m.dartagnan.parsers.LLVMIRParser.*; import com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.memory.Memory; import org.antlr.v4.runtime.*; class ParserLlvm implements ParserInterface { @@ -18,12 +20,42 @@ public Program parse(CharStream charStream) { LLVMIRParser parser = new LLVMIRParser(tokenStream); parser.addErrorListener(new AbortErrorListener()); - ParserRuleContext parserEntryPoint = parser.compilationUnit(); - VisitorLlvm visitor = new VisitorLlvm(); + CompilationUnitContext parserEntryPoint = parser.compilationUnit(); + DataLayout dataLayout = parseDataLayout(parserEntryPoint); + Program program = new Program(new Memory(dataLayout.bigEndian), Program.SourceLanguage.LLVM); + VisitorLlvm visitor = new VisitorLlvm(program); - parserEntryPoint.accept(visitor); + visitor.visitCompilationUnit(parserEntryPoint); // LLVM programs can be compiled to different targets, // thus we don't set the architectures. return visitor.buildProgram(); } + + private static final class DataLayout { + boolean bigEndian; + } + + private static DataLayout parseDataLayout(CompilationUnitContext ctx) { + var layout = new DataLayout(); + for (TopLevelEntityContext topLevelEntity : ctx.topLevelEntity()) { + TargetDefContext targetDef = topLevelEntity.targetDef(); + TargetDataLayoutContext targetDataLayout = targetDef == null ? null : targetDef.targetDataLayout(); + if (targetDataLayout == null) { + continue; + } + for (String spec : targetDataLayout.StringLit().getText().split("-")) { + parseDataLayout(layout, spec); + } + break; + } + return layout; + } + + //Target Data Layout specifications are read left-to-right as they occur + //see https://llvm.org/docs/LangRef.html#data-layout + private static void parseDataLayout(DataLayout layout, String spec) { + if (spec.equalsIgnoreCase("e")) { + layout.bigEndian = spec.equals("E"); + } + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java index bc364025eb..1aa5aff4e7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java @@ -202,10 +202,7 @@ public MemoryObject getOrNewMemoryObject(String name, int size) { mem.setName(name); if (program.getFormat() == LITMUS) { // Litmus code always initializes memory - final Expression zero = expressions.makeZero(types.getArchType()); - for (int offset = 0; offset < size; offset++) { - mem.setInitialValue(offset, zero); - } + mem.setInitialValue(0, expressions.makeZero(types.getIntegerType(8 * size))); } locations.put(name, mem); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorAsmArm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorAsmArm.java index 68ed5527e5..f628fa6f45 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorAsmArm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorAsmArm.java @@ -249,7 +249,7 @@ public Object visitStoreExclusive(AsmArmParser.StoreExclusiveContext ctx) { Register freshResultRegister = (Register) ctx.register(0).accept(this); Register value = (Register) ctx.register(1).accept(this); Register address = (Register) ctx.register(2).accept(this); - asmInstructions.add(EventFactory.Common.newExclusiveStore(freshResultRegister, address, value, Tag.ARMv8.MO_RX)); + asmInstructions.add(EventFactory.Common.newExclusiveStore(freshResultRegister, address, value, "")); return null; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java index 078a99a57c..3f743fee51 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java @@ -1,10 +1,5 @@ package com.dat3m.dartagnan.parsers.program.visitors; -import java.math.BigInteger; -import java.util.Arrays; -import java.util.HashMap; -import java.util.Map; - import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; @@ -13,22 +8,34 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusAArch64BaseVisitor; -import com.dat3m.dartagnan.parsers.LitmusAArch64Parser; +import com.dat3m.dartagnan.parsers.LitmusAArch64Parser.*; import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; -import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; -import com.dat3m.dartagnan.program.event.arch.StoreExclusive; +import com.dat3m.dartagnan.program.event.arch.Xchg; import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.metadata.CustomPrinting; +import org.antlr.v4.runtime.tree.TerminalNode; + +import java.math.BigInteger; +import java.util.*; + +import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters; +import static com.dat3m.dartagnan.program.event.Tag.ARMv8.*; +import static com.google.common.base.Preconditions.checkArgument; public class VisitorLitmusAArch64 extends LitmusAArch64BaseVisitor { - private record CmpInstruction(Expression left, Expression right) {}; + private record CmpInstruction(Expression left, Expression right) {} + private final ProgramBuilder programBuilder = ProgramBuilder.forArch(Program.SourceLanguage.LITMUS, Arch.ARM8); private final TypeFactory types = programBuilder.getTypeFactory(); - private final IntegerType archType = types.getArchType(); + private final IntegerType i8 = types.getIntegerType(8); + private final IntegerType i16 = types.getIntegerType(16); + private final IntegerType i32 = types.getIntegerType(32); + private final IntegerType i64 = types.getIntegerType(64); private final ExpressionFactory expressions = programBuilder.getExpressionFactory(); private int mainThread; private int threadCount = 0; @@ -42,13 +49,13 @@ public VisitorLitmusAArch64() { // Entry point @Override - public Object visitMain(LitmusAArch64Parser.MainContext ctx) { + public Object visitMain(MainContext ctx) { visitThreadDeclaratorList(ctx.program().threadDeclaratorList()); visitVariableDeclaratorList(ctx.variableDeclaratorList()); visitInstructionList(ctx.program().instructionList()); VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter()); Program prog = programBuilder.build(); - replaceZeroRegisters(prog, Arrays.asList("XZR, WZR")); + replaceZeroRegisters(prog, Arrays.asList("XZR", "WZR")); return prog; } @@ -56,36 +63,67 @@ public Object visitMain(LitmusAArch64Parser.MainContext ctx) { // Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; } @Override - public Object visitVariableDeclaratorLocation(LitmusAArch64Parser.VariableDeclaratorLocationContext ctx) { - programBuilder.initLocEqConst(ctx.location().getText(), expressions.parseValue(ctx.constant().getText(), archType)); + public Object visitTypedVariableDeclarator(TypedVariableDeclaratorContext ctx) { + final int typeBytes = typeBytes(ctx.type()); + if (ctx.constant() != null) { + final IntegerType type = types.getIntegerType(8 * typeBytes); + programBuilder.initLocEqConst(ctx.location().getText(), parseValue(ctx.constant(), type)); + } else { + programBuilder.newMemoryObject(ctx.location().getText(), typeBytes); + } return null; } @Override - public Object visitVariableDeclaratorRegister(LitmusAArch64Parser.VariableDeclaratorRegisterContext ctx) { - programBuilder.initRegEqConst(ctx.threadId().id, ctx.register64().id, expressions.parseValue(ctx.constant().getText(), archType)); + public Object visitTypedArrayDeclarator(TypedArrayDeclaratorContext ctx) { + final int typeBytes = typeBytes(ctx.type()); + final int arraySize = toInt(ctx.constant()); + programBuilder.newMemoryObject(ctx.location().getText(), typeBytes * arraySize); return null; } @Override - public Object visitVariableDeclaratorRegisterLocation(LitmusAArch64Parser.VariableDeclaratorRegisterLocationContext ctx) { - programBuilder.initRegEqLocPtr(ctx.threadId().id, ctx.register64().id, ctx.location().getText(), archType); + public Object visitVariableDeclaratorLocation(VariableDeclaratorLocationContext ctx) { + programBuilder.initLocEqConst(ctx.location().getText(), parseValue(ctx.constant(), i64)); return null; } @Override - public Object visitVariableDeclaratorLocationLocation(LitmusAArch64Parser.VariableDeclaratorLocationLocationContext ctx) { - programBuilder.initLocEqLocPtr(ctx.location(0).getText(), ctx.location(1).getText()); + public Object visitVariableDeclaratorRegister(VariableDeclaratorRegisterContext ctx) { + programBuilder.initRegEqConst(ctx.threadId().id, ctx.register64().id, parseValue(ctx.constant(), i64)); return null; } + @Override + public Object visitTypedRegisterDeclarator(TypedRegisterDeclaratorContext ctx) { + final int typeSize = typeBytes(ctx.type()); + final IntegerType type = types.getIntegerType(8 * typeSize); + if (ctx.constant() == null) { + programBuilder.getOrNewRegister(ctx.threadId().id, ctx.register64().id, type); + } else { + programBuilder.initRegEqConst(ctx.threadId().id, ctx.register64().id, parseValue(ctx.constant(), type)); + } + return null; + } + + @Override + public Object visitVariableDeclaratorRegisterLocation(VariableDeclaratorRegisterLocationContext ctx) { + programBuilder.initRegEqLocPtr(ctx.threadId().id, ctx.register64().id, ctx.location().getText(), i64); + return null; + } + + @Override + public Object visitVariableDeclaratorLocationLocation(VariableDeclaratorLocationLocationContext ctx) { + programBuilder.initLocEqLocPtr(ctx.location(0).getText(), ctx.location(1).getText()); + return null; + } // ---------------------------------------------------------------------------------------------------------------- // Thread declarator list (on top of instructions), e.g. " P0 | P1 | P2 ;" @Override - public Object visitThreadDeclaratorList(LitmusAArch64Parser.ThreadDeclaratorListContext ctx) { - for(LitmusAArch64Parser.ThreadIdContext threadCtx : ctx.threadId()){ + public Object visitThreadDeclaratorList(ThreadDeclaratorListContext ctx) { + for(ThreadIdContext threadCtx : ctx.threadId()){ programBuilder.newThread(threadCtx.id); threadCount++; } @@ -96,7 +134,7 @@ public Object visitThreadDeclaratorList(LitmusAArch64Parser.ThreadDeclaratorList // Instruction list (the program itself) @Override - public Object visitInstructionRow(LitmusAArch64Parser.InstructionRowContext ctx) { + public Object visitInstructionRow(InstructionRowContext ctx) { for(int i = 0; i < threadCount; i++){ mainThread = i; visitInstruction(ctx.instruction(i)); @@ -105,87 +143,173 @@ public Object visitInstructionRow(LitmusAArch64Parser.InstructionRowContext ctx) } @Override - public Object visitMov(LitmusAArch64Parser.MovContext ctx) { - Register register = programBuilder.getOrNewRegister(mainThread, ctx.rD, archType); - Expression expr = ctx.expr32() != null ? (Expression)ctx.expr32().accept(this) : (Expression)ctx.expr64().accept(this); - return programBuilder.addChild(mainThread, EventFactory.newLocal(register, expr)); + public Object visitMov(MovContext ctx) { + final Register r64 = parseRegister64(ctx.r32, ctx.r64); + final Expression expr = parseExpression(ctx.expr32(), ctx.expr64()); + return add(EventFactory.newLocal(r64, expressions.makeIntegerCast(expr, i64, false))); } @Override - public Object visitCmp(LitmusAArch64Parser.CmpContext ctx) { - Register register = programBuilder.getOrNewRegister(mainThread, ctx.rD, archType); - Expression expr = ctx.expr32() != null ? (Expression)ctx.expr32().accept(this) : (Expression)ctx.expr64().accept(this); - lastCmpInstructionPerThread.put(mainThread, new CmpInstruction(register, expr)); + public Object visitCmp(CmpContext ctx) { + final Register r64 = parseRegister64(ctx.r32, ctx.r64); + final Expression comparator = parseExpression(ctx.expr32(), ctx.expr64()); + final IntegerType type = ctx.r64 != null ? i64 : i32; + final Expression left = expressions.makeIntegerCast(r64, type, false); + final Expression right = expressions.makeIntegerCast(comparator, type, true); + lastCmpInstructionPerThread.put(mainThread, new CmpInstruction(left, right)); return null; } @Override - public Object visitArithmetic(LitmusAArch64Parser.ArithmeticContext ctx) { - Register rD = programBuilder.getOrNewRegister(mainThread, ctx.rD, archType); - Register r1 = programBuilder.getOrErrorRegister(mainThread, ctx.rV); - Expression expr = ctx.expr32() != null ? (Expression)ctx.expr32().accept(this) : (Expression)ctx.expr64().accept(this); - return programBuilder.addChild(mainThread, EventFactory.newLocal(rD, expressions.makeIntBinary(r1, ctx.arithmeticInstruction().op, expr))); + public Object visitArithmetic(ArithmeticContext ctx) { + final Register r64 = parseRegister64(ctx.rD32, ctx.rD64); + final Register operand = parseRegister64(ctx.rV32, ctx.rV64); + final Expression expr = parseExpression(ctx.expr32(), ctx.expr64()); + final IntegerType type = ctx.rD64 != null ? i64 : i32; + final Expression left = expressions.makeIntegerCast(operand, type, false); + final Expression right = expressions.makeIntegerCast(expr, type, false); + final Expression result = expressions.makeIntBinary(left, ctx.arithmeticInstruction().op, right); + add(EventFactory.newLocal(r64, expressions.makeIntegerCast(result, i64, false))); + return null; } @Override - public Object visitLoad(LitmusAArch64Parser.LoadContext ctx) { - Register register = programBuilder.getOrNewRegister(mainThread, ctx.rD, archType); - Register address = programBuilder.getOrErrorRegister(mainThread, ctx.address().id); - if(ctx.offset() != null){ - address = visitOffset(ctx.offset(), address); - } - return programBuilder.addChild(mainThread, EventFactory.newLoadWithMo(register, address, ctx.loadInstruction().mo)); + public Object visitLoad(LoadContext ctx) { + final Register r64 = parseRegister64(ctx.rD32, ctx.rD64); + final LoadInstructionContext inst = ctx.loadInstruction(); + final Register register = shrinkRegister(r64, ctx.rD32, inst.halfWordSize, inst.byteSize); + final Expression address = parseAddress(ctx.address()); + final String mo = inst.acquire ? MO_ACQ : ""; + add(EventFactory.newLoadWithMo(register, address, mo)); + addRegister64Update(r64, register); + return null; } @Override - public Object visitLoadExclusive(LitmusAArch64Parser.LoadExclusiveContext ctx) { - Register register = programBuilder.getOrNewRegister(mainThread, ctx.rD, archType); - Register address = programBuilder.getOrErrorRegister(mainThread, ctx.address().id); - if(ctx.offset() != null){ - address = visitOffset(ctx.offset(), address); - } - Load load = EventFactory.newRMWLoadExclusiveWithMo(register, address, ctx.loadExclusiveInstruction().mo); - return programBuilder.addChild(mainThread, load); + public Object visitLoadPair(LoadPairContext ctx) { + final boolean extended = ctx.rD064 != null; + final Register r064 = parseRegister64(ctx.rD032, ctx.rD064); + final Register r164 = parseRegister64(ctx.rD132, ctx.rD164); + final Register value0 = extended ? r064 : shrinkRegister(r064, ctx.rD032, false, false); + final Register value1 = extended ? r164 : shrinkRegister(r164, ctx.rD132, false, false); + final Expression address0 = parseAddress(ctx.address()); + final Expression address1 = expressions.makeAdd(address0, expressions.makeValue(extended ? 8 : 4, i64)); + add(EventFactory.newLoad(value0, address0)); + add(EventFactory.newLoad(value1, address1)); + addRegister64Update(r064, value0); + addRegister64Update(r164, value1); + return null; } @Override - public Object visitStore(LitmusAArch64Parser.StoreContext ctx) { - Register register = programBuilder.getOrNewRegister(mainThread, ctx.rV, archType); - Register address = programBuilder.getOrErrorRegister(mainThread, ctx.address().id); - if(ctx.offset() != null){ - address = visitOffset(ctx.offset(), address); - } - return programBuilder.addChild(mainThread, EventFactory.newStoreWithMo(address, register, ctx.storeInstruction().mo)); + public Object visitLoadExclusive(LoadExclusiveContext ctx) { + final Register r64 = parseRegister64(ctx.rD32, ctx.rD64); + final LoadExclusiveInstructionContext inst = ctx.loadExclusiveInstruction(); + final Register register = shrinkRegister(r64, ctx.rD32, inst.halfWordSize, inst.byteSize); + final Expression address = parseAddress(ctx.address()); + final String mo = inst.acquire ? MO_ACQ : ""; + add(EventFactory.newRMWLoadExclusiveWithMo(register, address, mo)); + addRegister64Update(r64, register); + return null; } @Override - public Object visitStoreExclusive(LitmusAArch64Parser.StoreExclusiveContext ctx) { - Register register = programBuilder.getOrNewRegister(mainThread, ctx.rV, archType); - Register statusReg = programBuilder.getOrNewRegister(mainThread, ctx.rS, archType); - Register address = programBuilder.getOrErrorRegister(mainThread, ctx.address().id); - if(ctx.offset() != null){ - address = visitOffset(ctx.offset(), address); + public Object visitStore(StoreContext ctx) { + final Register r64 = parseRegister64(ctx.rV32, ctx.rV64); + final StoreInstructionContext inst = ctx.storeInstruction(); + final IntegerType type = inst.byteSize ? i8 : inst.halfWordSize ? i16 : ctx.rV64 == null ? i32 : i64; + final Expression value = expressions.makeIntegerCast(r64, type, false); + final Expression address = parseAddress(ctx.address()); + final String mo = ctx.storeInstruction().release ? MO_REL : ""; + return add(EventFactory.newStoreWithMo(address, value, mo)); + } + + @Override + public Object visitStorePair(StorePairContext ctx) { + final boolean extended = ctx.r064 != null; + final Register r64 = parseRegister64(ctx.r032, ctx.r064); + final Register s64 = parseRegister64(ctx.r132, ctx.r164); + final IntegerType type = extended ? i64 : i32; + final Expression value0 = expressions.makeIntegerCast(r64, type, false); + final Expression value1 = expressions.makeIntegerCast(s64, type, false); + final Expression address0 = parseAddress(ctx.address()); + final Expression address1 = expressions.makeAdd(address0, expressions.makeValue(extended ? 8 : 4, i64)); + add(EventFactory.newStore(address0, value0)); + return add(EventFactory.newStore(address1, value1)); + } + + @Override + public Object visitStoreExclusive(StoreExclusiveContext ctx) { + final Register r64 = parseRegister64(ctx.rV32, ctx.rV64); + final StoreExclusiveInstructionContext inst = ctx.storeExclusiveInstruction(); + final IntegerType type = inst.byteSize ? i8 : inst.halfWordSize ? i16 : ctx.rV64 == null ? i32 : i64; + final Expression value = expressions.makeIntegerCast(r64, type, false); + final Register status = parseRegister64(ctx.rS32); + final Expression address = parseAddress(ctx.address()); + final String mo = ctx.storeExclusiveInstruction().release ? MO_REL : ""; + return add(EventFactory.Common.newExclusiveStore(status, address, value, mo)); + } + + private static final CustomPrinting SWP_PRINTER = e -> { + if (!(e instanceof Xchg xchg)) { + return Optional.empty(); } - StoreExclusive event = EventFactory.Common.newExclusiveStore(statusReg, address, register, ctx.storeExclusiveInstruction().mo); - return programBuilder.addChild(mainThread, event); + final String acq = e.hasTag(MO_ACQ) ? "A" : ""; + final String rel = e.hasTag(MO_REL) ? "L" : ""; + final Expression value = xchg.getValue(); + final Register loadReg = xchg.getResultRegister(); + final Expression address = xchg.getAddress(); + + return Optional.of(String.format("SWP%s%s %s, %s, [%s]", acq, rel, value, loadReg, address)); + }; + + // FIXME: SWP into a zero register (WZR or XZR) acts like a store, in particular SWPA(L) does not give + // acquire semantics then. + @Override + public Object visitSwap(SwapContext ctx) { + final SwapInstructionContext inst = ctx.swapInstruction(); + final boolean extended = ctx.rD64 != null; + final Register r64 = parseRegister64(ctx.rD32, ctx.rD64); + final Register lReg = shrinkRegister(r64, ctx.rD32, inst.halfWordSize, inst.byteSize); + final Register sReg = parseRegister64(ctx.rS32, ctx.rS64); + final Expression value = extended ? sReg : expressions.makeCast(sReg, lReg.getType(), false); + final Expression address = parseAddress(ctx.address()); + + final List mo = new ArrayList<>(); + if (inst.acquire) { + mo.add(MO_ACQ); + } + if (inst.release) { + mo.add(MO_REL); + } + + // TODO: Can lReg and sReg match? If so, we get a problem here. + final Xchg xchg = EventFactory.Common.newXchg(lReg, address, value); + xchg.addTags(mo); + xchg.setMetadata(SWP_PRINTER); + + add(xchg); + addRegister64Update(r64, lReg); + return null; } + @Override - public Object visitBranch(LitmusAArch64Parser.BranchContext ctx) { + public Object visitBranch(BranchContext ctx) { Label label = programBuilder.getOrCreateLabel(mainThread, ctx.label().getText()); if(ctx.branchCondition() == null){ - return programBuilder.addChild(mainThread, EventFactory.newGoto(label)); + return add(EventFactory.newGoto(label)); } CmpInstruction cmp = lastCmpInstructionPerThread.put(mainThread, null); if(cmp == null){ throw new ParsingException("Invalid syntax near " + ctx.getText()); } Expression expr = expressions.makeIntCmp(cmp.left, ctx.branchCondition().op, cmp.right); - return programBuilder.addChild(mainThread, EventFactory.newJump(expr, label)); + return add(EventFactory.newJump(expr, label)); } @Override - public Object visitBranchRegister(LitmusAArch64Parser.BranchRegisterContext ctx) { + public Object visitBranchRegister(BranchRegisterContext ctx) { Register register = programBuilder.getOrErrorRegister(mainThread, ctx.rV); if (!(register.getType() instanceof IntegerType integerType)) { throw new ParsingException("Comparing non-integer register."); @@ -193,75 +317,138 @@ public Object visitBranchRegister(LitmusAArch64Parser.BranchRegisterContext ctx) IntLiteral zero = expressions.makeZero(integerType); Expression expr = expressions.makeIntCmp(register, ctx.branchRegInstruction().op, zero); Label label = programBuilder.getOrCreateLabel(mainThread, ctx.label().getText()); - return programBuilder.addChild(mainThread, EventFactory.newJump(expr, label)); + return add(EventFactory.newJump(expr, label)); } @Override - public Object visitBranchLabel(LitmusAArch64Parser.BranchLabelContext ctx) { - return programBuilder.addChild(mainThread, programBuilder.getOrCreateLabel(mainThread, ctx.label().getText())); + public Object visitBranchLabel(BranchLabelContext ctx) { + return add(programBuilder.getOrCreateLabel(mainThread, ctx.label().getText())); } @Override - public Object visitFence(LitmusAArch64Parser.FenceContext ctx) { - return programBuilder.addChild(mainThread, EventFactory.newFenceOpt(ctx.Fence().getText(), ctx.opt)); + public Object visitFence(FenceContext ctx) { + return add(EventFactory.newFenceOpt(ctx.Fence().getText(), ctx.opt)); } @Override - public Object visitReturn(LitmusAArch64Parser.ReturnContext ctx) { + public Object visitReturn(ReturnContext ctx) { Label end = programBuilder.getEndOfThreadLabel(mainThread); - return programBuilder.addChild(mainThread, EventFactory.newGoto(end)); + return add(EventFactory.newGoto(end)); } @Override - public Expression visitExpressionRegister64(LitmusAArch64Parser.ExpressionRegister64Context ctx) { - Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register64().id, archType); + public Expression visitExpressionRegister64(ExpressionRegister64Context ctx) { + Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register64().id, i64); if(ctx.shift() != null){ - IntLiteral val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); + IntLiteral val = parseValue(ctx.shift().immediate().constant(), i64); expr = expressions.makeIntBinary(expr, ctx.shift().shiftOperator().op, val); } return expr; } @Override - public Expression visitExpressionRegister32(LitmusAArch64Parser.ExpressionRegister32Context ctx) { - Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register32().id, archType); - if(ctx.shift() != null){ - IntLiteral val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); - expr = expressions.makeIntBinary(expr, ctx.shift().shiftOperator().op, val); + public Expression visitExpressionRegister32(ExpressionRegister32Context ctx) { + final Register r64 = programBuilder.getOrNewRegister(mainThread, ctx.register32().id, i64); + final Expression expr = expressions.makeIntExtract(r64, 0, 31); + if (ctx.shift() == null) { + return expr; } - return expr; + final IntLiteral val = parseValue(ctx.shift().immediate().constant(), i64); + return expressions.makeIntBinary(expr, ctx.shift().shiftOperator().op, val); } @Override - public Expression visitExpressionImmediate(LitmusAArch64Parser.ExpressionImmediateContext ctx) { - Expression expr = expressions.parseValue(ctx.immediate().constant().getText(), archType); + public Expression visitExpressionImmediate(ExpressionImmediateContext ctx) { + Expression expr = parseValue(ctx.immediate().constant(), i64); if(ctx.shift() != null){ - IntLiteral val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); + IntLiteral val = parseValue(ctx.shift().immediate().constant(), i64); expr = expressions.makeIntBinary(expr, ctx.shift().shiftOperator().op, val); } return expr; } @Override - public Expression visitExpressionConversion(LitmusAArch64Parser.ExpressionConversionContext ctx) { - // TODO: Implement when adding support for mixed-size accesses - return programBuilder.getOrNewRegister(mainThread, ctx.register32().id, archType); - } - - private Register visitOffset(LitmusAArch64Parser.OffsetContext ctx, Register register){ - Register result = programBuilder.getOrNewRegister(mainThread, null, archType); - Expression expr = ctx.immediate() == null - ? programBuilder.getOrErrorRegister(mainThread, ctx.expressionConversion().register32().id) - : expressions.parseValue(ctx.immediate().constant().getText(), archType); - programBuilder.addChild(mainThread, EventFactory.newLocal(result, expressions.makeAdd(register, expr))); - return result; + public Expression visitExpressionConversion(ExpressionConversionContext ctx) { + final Register r64 = programBuilder.getOrNewRegister(mainThread, ctx.register32().id, i64); + return expressions.makeIntegerCast(expressions.makeIntExtract(r64, 0, 31), i64, ctx.signed); } @Override - public Expression visitImmediate(LitmusAArch64Parser.ImmediateContext ctx) { + public Expression visitImmediate(ImmediateContext ctx) { final int radix = ctx.Hexa() != null ? 16 : 10; BigInteger value = new BigInteger(ctx.constant().getText(), radix); - return expressions.makeValue(value, archType); + return expressions.makeValue(value, i64); + } + + private Expression parseExpression(Expr32Context x32, Expr64Context x64) { + return (Expression) (x32 != null ? x32 : x64).accept(this); + } + + private Expression parseAddress(AddressContext ctx) { + final Register base = programBuilder.getOrErrorRegister(mainThread, ctx.register64().id); + if (ctx.offset() == null) { + return base; + } + final ExpressionConversionContext conversion = ctx.offset().expressionConversion(); + final Register32Context register32 = conversion == null ? null : conversion.register32(); + final Register64Context register64 = ctx.offset().register64(); + final ImmediateContext imm = ctx.offset().immediate(); + final Expression offset = imm == null ? parseRegister64(register32, register64) : parseValue(imm.constant(), i64); + return expressions.makeAdd(base, offset); } + private Register parseRegister64(Register32Context w) { + return programBuilder.getOrNewRegister(mainThread, w.id, i64); + } + + private Register parseRegister64(Register64Context x) { + return programBuilder.getOrNewRegister(mainThread, x.id, i64); + } + + private Register parseRegister64(Register32Context w, Register64Context x) { + checkArgument((w == null) != (x == null), "Expected exactly one register, got [%s, %s]", w, x); + return w == null ? parseRegister64(x) : parseRegister64(w); + } + + private int toInt(ConstantContext ctx) { + final int radix = ctx.hex == null ? 10 : 16; + final TerminalNode node = ctx.hex == null ? ctx.DigitSequence() : ctx.HexDigitSequence(); + return Integer.parseInt(node.getText(), radix); + } + + private int typeBytes(TypeContext ignore) { + //defaults to 64 bits + return 8; + } + + private IntLiteral parseValue(ConstantContext ctx, IntegerType type) { + if (ctx.hex != null) { + return expressions.makeValue(new BigInteger(ctx.hex.getText().substring(2), 16), type); + } + return expressions.parseValue(ctx.getText(), type); + } + + private Register shrinkRegister(Register other, Register32Context ctx, boolean halfWordSize, boolean byteSize) { + checkArgument(other.getType().equals(i64), "Non-64-bit %s", other); + checkArgument(!byteSize | !halfWordSize, "Inconclusive access size"); + if (byteSize) { + return programBuilder.getOrNewRegister(mainThread, "B" + other.getName().substring(1), i8); + } + if (halfWordSize) { + return programBuilder.getOrNewRegister(mainThread, "H" + other.getName().substring(1), i16); + } + return ctx == null ? other : programBuilder.getOrNewRegister(mainThread, ctx.getText(), i32); + } + + private void addRegister64Update(Register r64, Register value) { + checkArgument(r64.getType().equals(i64), "Unexpectedly-typed register %s", r64); + if (r64 != value) { + add(EventFactory.newLocal(r64, expressions.makeIntegerCast(value, i64, false))); + } + } + + private Void add(Event event) { + programBuilder.addChild(mainThread, event); + return null; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java index 5f720d48b9..6edb76b566 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java @@ -4,6 +4,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.type.IntegerType; +import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusAssertionsBaseVisitor; import com.dat3m.dartagnan.parsers.LitmusAssertionsLexer; import com.dat3m.dartagnan.parsers.LitmusAssertionsParser; @@ -17,17 +18,21 @@ import org.antlr.v4.runtime.misc.Interval; import org.antlr.v4.runtime.tree.TerminalNode; +import java.math.BigInteger; + import static com.dat3m.dartagnan.program.Program.SpecificationType.*; import static com.google.common.base.Preconditions.checkState; class VisitorLitmusAssertions extends LitmusAssertionsBaseVisitor { private final ProgramBuilder programBuilder; + private final TypeFactory types; private final ExpressionFactory expressions; private final IntegerType archType; private VisitorLitmusAssertions(ProgramBuilder programBuilder) { this.programBuilder = programBuilder; + this.types = programBuilder.getTypeFactory(); this.expressions = programBuilder.getExpressionFactory(); this.archType = programBuilder.getTypeFactory().getArchType(); } @@ -98,14 +103,20 @@ public Expression visitAssertionOr(LitmusAssertionsParser.AssertionOrContext ctx @Override public Expression visitAssertionBasic(LitmusAssertionsParser.AssertionBasicContext ctx) { - Expression expr1 = acceptAssertionValue(ctx.assertionValue(0), false); - Expression expr2 = acceptAssertionValue(ctx.assertionValue(1), true); + final Expression lhs = acceptAssertionValue(ctx.assertionValue(0), false); + final Expression rhs = acceptAssertionValue(ctx.assertionValue(1), true); + final Expression expr1 = expressions.makeIntegerCast(lhs, archType, false); + final Expression expr2 = expressions.makeIntegerCast(rhs, archType, false); return expressions.makeIntCmp(expr1, ctx.assertionCompare().op, expr2); } private Expression acceptAssertionValue(LitmusAssertionsParser.AssertionValueContext ctx, boolean right) { - if (ctx.constant() != null) { - return expressions.parseValue(ctx.constant().getText(), archType); + LitmusAssertionsParser.ConstantContext constant = ctx.constant(); + if (constant != null) { + if (constant.hex != null) { + return expressions.makeValue(new BigInteger(constant.hex.getText().substring(2), 16), archType); + } + return expressions.parseValue(constant.getText(), archType); } String name = ctx.varName().getText(); if (ctx.threadId() != null) { @@ -115,6 +126,7 @@ private Expression acceptAssertionValue(LitmusAssertionsParser.AssertionValueCon checkState(base != null, "uninitialized location %s", name); TerminalNode offset = ctx.DigitSequence(); int o = offset == null ? 0 : Integer.parseInt(offset.getText()); - return right && offset == null ? base : new FinalMemoryValue(name, archType, base, o); + final IntegerType type = types.getIntegerType(Math.min(64, 8 * base.getKnownSize())); + return right && offset == null ? base : new FinalMemoryValue(name, type, base, o); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java index 948a3e130a..a0cfa32c51 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java @@ -19,7 +19,6 @@ import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.metadata.Metadata; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; -import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; @@ -48,7 +47,7 @@ public class VisitorLlvm extends LLVMIRBaseVisitor { private static final String DEFAULT_ENTRY_FUNCTION = "main"; // Global context - private final Program program = new Program(new Memory(), Program.SourceLanguage.LLVM); + private final Program program; private final TypeFactory types = TypeFactory.getInstance(); private final ExpressionFactory expressions = ExpressionFactory.getInstance(); private final Type pointerType = types.getPointerType(); @@ -71,7 +70,9 @@ public class VisitorLlvm extends LLVMIRBaseVisitor { // Nonnull, if a type has been parsed. private Type parsedType; - public VisitorLlvm() {} + public VisitorLlvm(Program p) { + program = p; + } public Program buildProgram() { ProgramBuilder.processAfterParsing(program); @@ -1511,7 +1512,7 @@ public Optional getField(String fieldName) { return Optional.empty(); } } - + // ---------------------------------------------------------------------------------------------------------------- // Helper to parse inline asm code private Optional> tryParse(ParserAsm parser, CharStream asmCode) throws ProgramProcessingException{ diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsLogical.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsLogical.java index b2e29ebb5d..9763c22439 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsLogical.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsLogical.java @@ -60,7 +60,7 @@ public Event visitOpSelect(SpirvParser.OpSelectContext ctx) { id, type, op1.getType(), op2.getType()); } if (op1.getType() instanceof IntegerType || op1.getType() instanceof BooleanType) { - return builder.addEvent(new Local(register, expressions.makeITE(cond, op1, op2))); + return builder.addEvent(EventFactory.newLocal(register, expressions.makeITE(cond, op1, op2))); } throw new ParsingException("Illegal definition for '%s', " + "operands must be integers or arrays of booleans", id); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java index f0de7102db..1eb8ebe29e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java @@ -6,10 +6,15 @@ import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.type.AggregateType; import com.dat3m.dartagnan.expression.type.ArrayType; +import com.dat3m.dartagnan.expression.type.FunctionType; +import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.expression.type.TypeOffset; import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.memory.Memory; +import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; import com.google.common.base.Preconditions; @@ -18,6 +23,9 @@ public class Program { + private static final TypeFactory types = TypeFactory.getInstance(); + private static final FunctionType initThreadType = types.getFunctionType(types.getVoidType(), List.of()); + public enum SourceLanguage { LITMUS, LLVM, SPV } public enum SpecificationType { EXISTS, FORALL, NOT_EXISTS, ASSERT } @@ -36,6 +44,7 @@ public enum SpecificationType { EXISTS, FORALL, NOT_EXISTS, ASSERT } private boolean isCompiled; private final SourceLanguage format; + private int nextThreadId = 0; private int nextConstantId = 0; // ------------------------ @@ -127,6 +136,7 @@ public void setFilterSpecification(Expression spec) { public void addThread(Thread t) { threads.add(t); t.setProgram(this); + nextThreadId = Math.max(nextThreadId, t.getId()) + 1; } public void addFunction(Function func) { @@ -194,6 +204,22 @@ public List getThreadEventsWithAllTags(String... tags) { return getThreadEvents().stream().filter(e -> e.getTags().containsAll(tagList)).collect(Collectors.toList()); } + public void addInit(MemoryObject object, int offset) { + final boolean isC11 = arch == Arch.C11 || arch == Arch.OPENCL; + final List paramNames = List.of(); + // NOTE: We use different names to avoid symmetry detection treating all inits as symmetric. + final String threadName = "Init_" + nextThreadId; + final Thread thread = new Thread(threadName, initThreadType, paramNames, nextThreadId, + EventFactory.newThreadStart(null)); + final Event init = EventFactory.newInit(object, offset); + thread.append(init); + if (isC11) { + init.addTags(Tag.C11.NONATOMIC); + } + thread.append(EventFactory.newLabel("END_OF_T" + thread.getId())); + addThread(thread); + } + // Unrolling // ----------------------------------------------------------------------------------------------------------------- diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java index 2330b85306..18b0f68e6c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java @@ -2,6 +2,7 @@ import com.dat3m.dartagnan.configuration.Alias; import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.core.Init; @@ -34,18 +35,40 @@ public interface AliasAnalysis { boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b); - static AliasAnalysis fromConfig(Program program, Context analysisContext, Configuration config) throws InvalidConfigurationException { - Config c = new Config(config); + /** + * Checks if two accessed byte ranges may overlap, without matching perfectly. + *

+ * Accesses to memory actually target a range of bytes, + * starting with the byte the address points to, inclusively, + * and ending with the byte offset from the start by the associated type's size in bytes, exclusively. + * This analysis calls a pair of accesses on memory mixing, + * if the accessed byte range overlaps, without also being equal. + * There are three cases how this can be achieved: + *

    + *
  • The types match, but the address are offset by a too small margin. + *
  • The addresses match exactly, as in {@link #mayAlias}, but the type sizes differ. + *
  • A combination of the above. + *
+ * False positives may occur, but false negatives shall not occur, + * so long as the program features no undefined behavior, such as use-after-free or buffer overflows. + * @param event Memory access in the analyzed program. + * @return Sorted list of offsets, where another access' byte range may start or end. + */ + List mayMixedSizeAccesses(MemoryCoreEvent event); + + static AliasAnalysis fromConfig(Program program, Context analysisContext, Configuration config, + boolean detectMixedSizeAccesses) throws InvalidConfigurationException { + Config c = new Config(config, detectMixedSizeAccesses); logger.info("Selected alias analysis: {}", c.method); long t0 = System.currentTimeMillis(); AliasAnalysis a = switch (c.method) { - case FIELD_SENSITIVE -> FieldSensitiveAndersen.fromConfig(program, config); - case FIELD_INSENSITIVE -> AndersenAliasAnalysis.fromConfig(program, config); + case FIELD_SENSITIVE -> FieldSensitiveAndersen.fromConfig(program, c); + case FIELD_INSENSITIVE -> AndersenAliasAnalysis.fromConfig(program, c); case FULL -> InclusionBasedPointerAnalysis.fromConfig(program, analysisContext, c); }; - a = new CombinedAliasAnalysis(a, EqualityAliasAnalysis.fromConfig(program, config)); + a = new CombinedAliasAnalysis(a, EqualityAliasAnalysis.fromConfig(program, c)); if (Arch.supportsVirtualAddressing(program.getArch())) { - a = VirtualAliasAnalysis.wrap(a); + a = VirtualAliasAnalysis.wrap(a, c); } if (c.graphviz) { a.generateGraph(program, c); @@ -87,9 +110,23 @@ final class Config { " Defaults to 'false'.", secure = true) boolean graphvizInternal; - private Config(Configuration config) throws InvalidConfigurationException { + final boolean detectMixedSizeAccesses; + + private Config(Configuration config, boolean msa) throws InvalidConfigurationException { + detectMixedSizeAccesses = msa; config.inject(this); } + + List defaultMayMixedSizeAccesses(MemoryCoreEvent event) { + final var set = new ArrayList(); + if (detectMixedSizeAccesses) { + final int bytes = TypeFactory.getInstance().getMemorySizeInBytes(event.getAccessType()); + for (int i = 1; i < bytes; i++) { + set.add(i); + } + } + return set; + } } final class CombinedAliasAnalysis implements AliasAnalysis { @@ -112,6 +149,18 @@ public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) { return a1.mayAlias(a, b) && a2.mayAlias(a, b); } + @Override + public List mayMixedSizeAccesses(MemoryCoreEvent a) { + final List set1 = a1.mayMixedSizeAccesses(a); + final List set2 = a2.mayMixedSizeAccesses(a); + // compute the intersection + if (set1.isEmpty() | set2.isEmpty()) { + return set1.isEmpty() ? set1 : set2; + } + final boolean smaller = set1.size() < set2.size(); + return (smaller ? set1 : set2).stream().filter((smaller ? set2 : set1)::contains).toList(); + } + @Override public Graphviz getGraphVisualization() { return a1.getGraphVisualization(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java index 3aa76b80fe..0cca76eba5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java @@ -15,8 +15,6 @@ import com.google.common.base.Verify; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Sets; -import org.sosy_lab.common.configuration.Configuration; -import org.sosy_lab.common.configuration.InvalidConfigurationException; import java.util.*; import java.util.stream.Collectors; @@ -37,6 +35,7 @@ */ public class AndersenAliasAnalysis implements AliasAnalysis { + private final AliasAnalysis.Config config; ///When a pointer set gains new content, it is added to this queue private final Queue variables = new ArrayDeque<>(); ///Super set of all pointer sets in this analysis @@ -49,8 +48,9 @@ public class AndersenAliasAnalysis implements AliasAnalysis { // ================================ Construction ================================ - private AndersenAliasAnalysis(Program program) { + private AndersenAliasAnalysis(Program program, Config c) { Preconditions.checkArgument(program.isCompiled(), "The program must be compiled first."); + config = c; ImmutableSet.Builder builder = new ImmutableSet.Builder<>(); for (MemoryObject a : program.getMemory().getObjects()) { for (int i = 0; i < a.getKnownSize(); i++) { @@ -61,8 +61,8 @@ private AndersenAliasAnalysis(Program program) { run(program); } - public static AndersenAliasAnalysis fromConfig(Program program, Configuration config) throws InvalidConfigurationException { - return new AndersenAliasAnalysis(program); + public static AndersenAliasAnalysis fromConfig(Program program, Config config) { + return new AndersenAliasAnalysis(program, config); } // ================================ API ================================ @@ -77,6 +77,11 @@ public boolean mustAlias(MemoryCoreEvent x, MemoryCoreEvent y) { return getMaxAddressSet(x).size() == 1 && getMaxAddressSet(x).containsAll(getMaxAddressSet(y)); } + @Override + public List mayMixedSizeAccesses(MemoryCoreEvent event) { + return config.defaultMayMixedSizeAccesses(event); + } + private ImmutableSet getMaxAddressSet(MemoryEvent e) { return eventAddressSpaceMap.get(e); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java index 9d5a923e78..5f95fc360a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java @@ -7,11 +7,12 @@ import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; -import org.sosy_lab.common.configuration.Configuration; -import org.sosy_lab.common.configuration.InvalidConfigurationException; +import java.util.List; import java.util.Set; +import static com.google.common.base.Preconditions.checkNotNull; + /** * A simple alias analysis that establishes must-aliases of * two events, if they use the same address-expression and @@ -21,11 +22,17 @@ */ public class EqualityAliasAnalysis implements AliasAnalysis { + private final Config config; + private final MutableEventGraph trueSet = new MapEventGraph(); private final MutableEventGraph falseSet = new MapEventGraph(); - public static EqualityAliasAnalysis fromConfig(Program program, Configuration config) throws InvalidConfigurationException { - return new EqualityAliasAnalysis(); + public static EqualityAliasAnalysis fromConfig(Program program, Config config) { + return new EqualityAliasAnalysis(config); + } + + private EqualityAliasAnalysis(Config c) { + config = checkNotNull(c); } @Override @@ -70,4 +77,9 @@ public boolean mustAlias(MemoryCoreEvent a, MemoryCoreEvent b) { public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) { return true; } + + @Override + public List mayMixedSizeAccesses(MemoryCoreEvent event) { + return config.defaultMayMixedSizeAccesses(event); + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java index 3127715cf8..233cb7e345 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java @@ -10,15 +10,12 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Sets; -import org.sosy_lab.common.configuration.Configuration; -import org.sosy_lab.common.configuration.InvalidConfigurationException; import java.math.BigInteger; import java.util.*; @@ -26,6 +23,7 @@ import static com.dat3m.dartagnan.expression.integers.IntBinaryOp.*; import static com.dat3m.dartagnan.expression.integers.IntUnaryOp.MINUS; import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Verify.verify; import static java.util.stream.Collectors.toList; import static java.util.stream.IntStream.range; @@ -44,6 +42,8 @@ */ public class FieldSensitiveAndersen implements AliasAnalysis { + private final Config config; + ///When a pointer set gains new content, it is added to this queue private final LinkedHashSet variables = new LinkedHashSet<>(); @@ -59,13 +59,15 @@ public class FieldSensitiveAndersen implements AliasAnalysis { // ================================ Construction ================================ - public static FieldSensitiveAndersen fromConfig(Program program, Configuration config) throws InvalidConfigurationException { - var analysis = new FieldSensitiveAndersen(); + public static FieldSensitiveAndersen fromConfig(Program program, Config config) { + var analysis = new FieldSensitiveAndersen(config); analysis.run(program); return analysis; } - private FieldSensitiveAndersen() { } + private FieldSensitiveAndersen(Config c) { + config = checkNotNull(c); + } // ================================ API ================================ @@ -80,7 +82,12 @@ public boolean mustAlias(MemoryCoreEvent x, MemoryCoreEvent y) { return a.size() == 1 && a.containsAll(getMaxAddressSet(y)); } - private ImmutableSet getMaxAddressSet(MemoryEvent e) { + @Override + public List mayMixedSizeAccesses(MemoryCoreEvent event) { + return config.defaultMayMixedSizeAccesses(event); + } + + private ImmutableSet getMaxAddressSet(MemoryCoreEvent e) { return eventAddressSpaceMap.get(e); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java index 8a13f70d7c..eab26d8e50 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java @@ -2,8 +2,12 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionVisitor; +import com.dat3m.dartagnan.expression.aggregates.ConstructExpr; +import com.dat3m.dartagnan.expression.aggregates.ExtractExpr; import com.dat3m.dartagnan.expression.integers.*; import com.dat3m.dartagnan.expression.misc.ITEExpr; +import com.dat3m.dartagnan.expression.processing.ExpressionInspector; +import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; @@ -23,6 +27,7 @@ import java.math.BigInteger; import java.util.*; +import java.util.stream.IntStream; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Verify.verify; @@ -70,6 +75,8 @@ public class InclusionBasedPointerAnalysis implements AliasAnalysis { private static final Logger logger = LogManager.getLogger(InclusionBasedPointerAnalysis.class); + private static final TypeFactory types = TypeFactory.getInstance(); + // This analysis depends on another, that maps used registers to a list of possible direct writers. private final ReachingDefinitionsAnalysis dependency; @@ -91,6 +98,9 @@ public class InclusionBasedPointerAnalysis implements AliasAnalysis { // Non-trivial modifiers may only appear for singleton Locals. private final Map, DerivedVariable> registerVariables = new HashMap<>(); + // Maps memory events to additional offsets inside their byte range, which may match other accesses' bounds. + private final Map> mixedAccesses = new HashMap<>(); + // If enabled, the algorithm describes its internal graph to be written into a file. private Graphviz graphviz; @@ -119,6 +129,9 @@ public static InclusionBasedPointerAnalysis fromConfig(Program program, Context final ReachingDefinitionsAnalysis def = analysisContext.requires(ReachingDefinitionsAnalysis.class); final var analysis = new InclusionBasedPointerAnalysis(program, def); analysis.run(program, config); + if (config.detectMixedSizeAccesses) { + analysis.detectMixedSizeAccesses(); + } logger.debug("variable count: {}", analysis.totalVariables); logger.debug("replacement count: {}", @@ -155,14 +168,16 @@ public boolean mayAlias(MemoryCoreEvent x, MemoryCoreEvent y) { if (vx.base == vy.base && isConstant(vx.modifier) && isConstant(vy.modifier)) { return vx.modifier.offset == vy.modifier.offset; } - final List ox = new ArrayList<>(vx.base.includes); - ox.add(new IncludeEdge(vx.base, TRIVIAL_MODIFIER)); - final List oy = new ArrayList<>(vy.base.includes); - oy.add(new IncludeEdge(vy.base, TRIVIAL_MODIFIER)); + final List ox = toIncludeSet(vx.base); + final List oy = toIncludeSet(vy.base); for (final IncludeEdge ax : ox) { for (final IncludeEdge ay : oy) { - if (ax.source == ay.source && overlaps(compose(ax.modifier, vx.modifier), compose(ay.modifier, vy.modifier))) { - return true; + if (ax.source == ay.source) { + final Modifier l = compose(ax.modifier, vx.modifier); + final Modifier r = compose(ay.modifier, vy.modifier); + if (overlaps(l, r)) { + return true; + } } } } @@ -177,6 +192,79 @@ public boolean mustAlias(MemoryCoreEvent x, MemoryCoreEvent y) { isConstant(vx.modifier) && isConstant(vy.modifier); } + @Override + public List mayMixedSizeAccesses(MemoryCoreEvent event) { + final List result = mixedAccesses.get(event); + if (result != null) { + return Collections.unmodifiableList(result); + } + final int bytes = types.getMemorySizeInBytes(event.getAccessType()); + return IntStream.range(1, bytes).boxed().toList(); + } + + // ================================ Mixed Size Access Detection ================================ + + private void detectMixedSizeAccesses() { + final List events = List.copyOf(addressVariables.keySet()); + final List> offsets = new ArrayList<>(); + for (int i = 0; i < events.size(); i++) { + final MemoryCoreEvent event0 = events.get(i); + final var set0 = new HashSet(); + for (int j = 0; j < i; j++) { + detectMixedSizeAccessPair(event0, set0, events.get(j), offsets.get(j)); + } + offsets.add(set0); + } + for (int i = 0; i < events.size(); i++) { + mixedAccesses.put(events.get(i), offsets.get(i).stream().sorted().toList()); + } + } + + private void detectMixedSizeAccessPair(MemoryCoreEvent x, Set xSet, MemoryCoreEvent y, Set ySet) { + final DerivedVariable vx = addressVariables.get(x); + final DerivedVariable vy = addressVariables.get(y); + assert vx != null & vy != null; + final int bytesX = types.getMemorySizeInBytes(x.getAccessType()); + final int bytesY = types.getMemorySizeInBytes(y.getAccessType()); + if (vx.base == vy.base) { + fetchAllMixedOffsets(xSet, vx.modifier, bytesX, ySet, vy.modifier, bytesY); + return; + } + final List oy = toIncludeSet(vy.base); + for (final IncludeEdge ax : toIncludeSet(vx.base)) { + for (final IncludeEdge ay : oy) { + if (ax.source == ay.source) { + final Modifier modifierX = compose(ax.modifier, vx.modifier); + final Modifier modifierY = compose(ay.modifier, vy.modifier); + fetchAllMixedOffsets(xSet, modifierX, bytesX, ySet, modifierY, bytesY); + } + } + } + } + + + private List toIncludeSet(Variable address) { + final List set = new ArrayList<>(address.includes); + set.add(new IncludeEdge(address, TRIVIAL_MODIFIER)); + return set; + } + + private void fetchAllMixedOffsets(Set xSet, Modifier xModifier, int xBytes, + Set ySet, Modifier yModifier, int yBytes) { + fetchMixedOffsets(xSet, xModifier, xBytes, yModifier, yBytes); + fetchMixedOffsets(ySet, yModifier, yBytes, xModifier, xBytes); + } + + private void fetchMixedOffsets(Set out, Modifier modifier0, int bytes0, Modifier modifier1, int bytes1) { + final Modifier next = compose(modifier1, modifier(bytes1, List.of())); + for (int i = 1; i < bytes0; i++) { + final Modifier offset = compose(modifier0, modifier(i, List.of())); + if (overlaps(offset, modifier1) || overlaps(offset, next)) { + out.add(i); + } + } + } + @Override public Graphviz getGraphVisualization() { return graphviz; @@ -190,7 +278,7 @@ private void run(Program program, AliasAnalysis.Config configuration) { // Each memory object gets a variable representing its base address value. for (final MemoryObject object : program.getMemory().getObjects()) { totalVariables++; - objectVariables.put(object, new Variable(object, object.toString())); + objectVariables.put(object, new Variable(object, null, object.toString())); } // Each expression gets a "res" variable representing its result value set. // Each register writer gets an "out" variable ("ld" for loads) representing its return value set. @@ -396,12 +484,14 @@ private void postProcess(Map.Entry entry) { final Modifier modifier = compose(includeEdge.modifier, address.modifier); assert includeEdge.source.object != null; // If the only included address refers to the last element, treat it as a direct static offset instead. - if (!includeEdge.source.object.hasKnownSize()) { + // This only works on concrete objects, where size is reliable. + if (!includeEdge.source.object.getClass().equals(MemoryObject.class) || !includeEdge.source.object.hasKnownSize()) { return; } - final int remainingSize = includeEdge.source.object.getKnownSize() - modifier.offset; + final int accessSize = types.getMemorySizeInBytes(entry.getKey().getAccessType()); + final int remainingSize = includeEdge.source.object.getKnownSize() - modifier.offset - (accessSize - 1); for (final Integer a : modifier.alignment) { - if (a < remainingSize) { + if (Math.abs(a) < remainingSize || a < 0 && modifier.offset + a >= 0) { return; } } @@ -424,10 +514,13 @@ private static final class Variable { private final Set seeAlso = new LinkedHashSet<>(); // If nonnull, this variable represents that object's base address. private final MemoryObject object; + // If nonnull, this variable represents an aggregate of field variables. + private final DerivedVariable[] aggregate; // For visualization. private final String name; - private Variable(MemoryObject o, String n) { + private Variable(MemoryObject o, DerivedVariable[] a, String n) { object = o; + aggregate = a; name = n; } @Override public String toString() { return name; } @@ -476,7 +569,7 @@ private static IncludeEdge includeEdge(DerivedVariable variable) { private Variable newVariable(String name) { totalVariables++; - return new Variable(null, name); + return new Variable(null, null, name); } // Inserts a single inclusion relationship into the graph. @@ -825,12 +918,6 @@ private static List compose(List left, int right) { return right == 0 ? left : compose(left, List.of(right)); } - // Adds an optional register to a set of dynamic offsets. - // If the register is present, it may contain any value. - private static List compose(List left, Register right) { - return right == null ? left : TOP; - } - // Applies another offset to an existing labeled edge. private static DerivedVariable compose(DerivedVariable other, Modifier modifier) { return isTrivial(modifier) ? other : new DerivedVariable(other.base, compose(other.modifier, modifier)); @@ -848,62 +935,14 @@ private static StoreEdge compose(StoreEdge other, Modifier modifier) { return isTrivial(modifier) ? other : new StoreEdge(other.value, compose(other.addressModifier, modifier)); } - // Multiplies all dynamic offsets with another factor. - private static List mul(List a, int factor) { - return factor == 0 ? List.of() : a.stream().map(i -> i * factor).toList(); - } - - // Describes (constant address or register or zero) + offset + alignment * (variable) - private record Result(MemoryObject address, Register register, BigInteger offset, List alignment) { - private boolean isConstant() { - return address == null && register == null && alignment.isEmpty(); - } - @Override - public String toString() { - return String.format("%s+%s+%sx", address != null ? address : register, offset, alignment); - } - } - // Interprets an expression. // The result refers to an existing variable, // if the expression has a static base, or if the expression has a dynamic base with exactly one writer. // Otherwise, it refers to a new variable with proper incoming edges. private DerivedVariable getResultVariable(Expression expression, RegReader reader) { - final var collector = new Collector(); - final Result result = expression.accept(collector); - final DerivedVariable main; - if (result != null && (result.address != null || result.register != null)) { - final DerivedVariable base = result.address != null ? derive(objectVariables.get(result.address)) : - getPhiNodeVariable(result.register, reader); - sort(result.alignment); - main = compose(base, modifier(result.offset.intValue(), result.alignment)); - } else { - main = null; - } - if (main != null && - collector.address.stream().allMatch(a -> a == result.address) && - collector.register.stream().allMatch(r -> r == result.register)) { - return main; - } - if (main == null && collector.address.isEmpty() && collector.register.isEmpty()) { - return null; - } - final Variable variable = newVariable("res" + reader.getGlobalId() + "(" + expression + ")"); - if (main != null) { - addInclude(variable, includeEdge(main)); - } - for (final MemoryObject object : collector.address) { - if (result == null || object != result.address) { - addInclude(variable, new IncludeEdge(objectVariables.get(object), RELAXED_MODIFIER)); - } - } - for (final Register register : collector.register) { - if (result == null || register != result.register) { - final DerivedVariable registerVariable = getPhiNodeVariable(register, reader); - addInclude(variable, new IncludeEdge(registerVariable.base, RELAXED_MODIFIER)); - } - } - return derive(variable); + final var collector = new Collector(reader); + final List result = expression.accept(collector); + return getOrNewVariable(result, String.format("res%d(%s)", reader.getGlobalId(), expression)); } // Fetches the node for address values that can be read from a register at a specific program point. @@ -926,114 +965,171 @@ private DerivedVariable getPhiNodeVariable(Register register, RegReader reader) return registerVariables.compute(writers, (k, v) -> derive(result)); } - private static final class Collector implements ExpressionVisitor { + private DerivedVariable getOrNewVariable(List edges, String name) { + if (edges.isEmpty()) { + return null; + } + if (edges.size() == 1) { + return new DerivedVariable(edges.get(0).source, edges.get(0).modifier); + } + final Variable base = newVariable(name); + for (IncludeEdge edge : edges) { + addInclude(base, edge); + } + return derive(base); + } - final Set address = new LinkedHashSet<>(); - final Set register = new LinkedHashSet<>(); + private final class Collector implements ExpressionVisitor> { - @Override - public Result visitExpression(Expression expr) { - register.addAll(expr.getRegs()); - return null; + private final RegReader reader; + + private Collector(RegReader reader) { + this.reader = reader; } @Override - public Result visitIntBinaryExpression(IntBinaryExpr x) { - final Result left = x.getLeft().accept(this); - final Result right = x.getRight().accept(this); - final IntBinaryOp kind = x.getKind(); - if (left != null && left.isConstant() && right != null && right.isConstant()) { - // TODO: Make sure that the type of normalization does not break this code. - // Maybe always do signed normalization? - final BigInteger result = kind.apply(left.offset, right.offset, x.getType().getBitWidth()); - return new Result(null, null, result, List.of()); - } - return switch (kind) { - case MUL -> { - if (left == null && right == null || - left != null && left.address != null || - right != null && right.address != null) { - yield null; - } - if (left == null || right == null) { - final Result factor = left == null ? right : left; - if (factor.register != null) { - yield null; - } - final List alignment = compose(factor.alignment, factor.offset.intValue()); - yield new Result(null, null, BigInteger.ZERO, alignment); - } - final List leftAlignment = mul(compose(left.alignment, left.register), right.offset.intValue()); - final List rightAlignment = mul(compose(right.alignment, right.register), left.offset.intValue()); - yield new Result(null, null, left.offset.multiply(right.offset), compose(leftAlignment, rightAlignment)); + public List visitExpression(Expression expr) { + final List edges = new ArrayList<>(); + expr.accept(new ExpressionInspector() { + @Override + public Expression visitRegister(Register register) { + edges.add(new IncludeEdge(getPhiNodeVariable(register, reader).base, RELAXED_MODIFIER)); + return register; } - case ADD, SUB -> { - if (left == null || right == null || left.address != null && right.address != null) { - yield null; - } - final MemoryObject base = left.address != null ? left.address : right.address; - final BigInteger offset = kind.apply(left.offset, right.offset, x.getType().getBitWidth()); - if (base != null) { - final List leftAlignment = compose(left.alignment, left.register); - final List rightAlignment = compose(right.alignment, right.register); - yield new Result(base, null, offset, compose(leftAlignment, rightAlignment)); - } - if (left.register != null && right.register != null) { - yield null; - } - final Register register = left.register != null ? left.register : right.register; - final List alignment = compose(left.alignment, right.alignment); - yield new Result(null, register, offset, alignment); + @Override + public Expression visitMemoryObject(MemoryObject object) { + edges.add(new IncludeEdge(objectVariables.get(object), RELAXED_MODIFIER)); + return object; } - default -> null; - }; + }); + return edges; } + record ExprFlip(Expression x, int factor) {} + @Override - public Result visitIntUnaryExpression(IntUnaryExpr x) { - if (x.getKind() != IntUnaryOp.MINUS) { - return null; + public List visitIntBinaryExpression(IntBinaryExpr x) { + BigInteger offset = BigInteger.ZERO; + final List operands = new ArrayList<>(); + final Stack stack = new Stack<>(); + if (!matchLinearExpression(new ExprFlip(x, 1), stack)) { + return visitExpression(x); } - final Result result = x.getOperand().accept(this); - if (result.address != null || result.register != null) { - return null; + while (!stack.isEmpty()) { + final ExprFlip operand = stack.pop(); + if (matchLinearExpression(operand, stack)) { + continue; + } + if (operand.x instanceof IntLiteral literal) { + offset = offset.add(literal.getValue().multiply(BigInteger.valueOf(operand.factor))); + } else { + operands.add(operand); + } + } + final List result = new ArrayList<>(); + final int o = offset.intValue(); + for (int i = 0; i < operands.size(); i++) { + final ExprFlip operand = operands.get(i); + if (operand.factor != 1) { + result.addAll(visitExpression(operand.x)); + continue; + } + List alignment = List.of(); + for (int j = 0; j < operands.size(); j++) { + alignment = j == i ? alignment : compose(alignment, operands.get(j).factor); + } + for (IncludeEdge subResult : operand.x.accept(this)) { + addInto(result, compose(subResult, modifier(o, alignment)), false); + } } - final var alignment = new ArrayList(); - for (final Integer a : result.alignment) { - alignment.add(-Math.abs(a)); + return result; + } + + private boolean matchLinearExpression(ExprFlip operand, Stack stack) { + final Expression left = operand.x instanceof IntBinaryExpr x ? x.getLeft() : null; + final Expression right = operand.x instanceof IntBinaryExpr x ? x.getRight() : null; + final boolean add = operand.x.getKind().equals(IntBinaryOp.ADD); + final boolean sub = operand.x.getKind().equals(IntBinaryOp.SUB); + final boolean mul = operand.x.getKind().equals(IntBinaryOp.MUL); + if (add || sub) { + stack.push(new ExprFlip(right, operand.factor * (add ? 1 : -1))); + stack.push(new ExprFlip(left, operand.factor)); + return true; + } else if (mul) { + final IntLiteral leftLiteral = left instanceof IntLiteral l ? l : null; + final IntLiteral rightLiteral = right instanceof IntLiteral l ? l : null; + if (leftLiteral != null || rightLiteral != null) { + final int factor = (leftLiteral != null ? leftLiteral : rightLiteral).getValueAsInt(); + stack.push(new ExprFlip(leftLiteral != null ? right : left, operand.factor * factor)); + return true; + } } - return new Result(null, null, result.offset.negate(), alignment); + return false; } @Override - public Result visitIntSizeCastExpression(IntSizeCast expr) { + public List visitIntSizeCastExpression(IntSizeCast expr) { // We assume type casts do not affect the value of pointers. - final Result result = expr.getOperand().accept(this); - return expr.isExtension() && !expr.preservesSign() ? result : null; + return expr.isExtension() && !expr.preservesSign() ? expr.getOperand().accept(this) : visitExpression(expr); } @Override - public Result visitITEExpression(ITEExpr x) { - x.getTrueCase().accept(this); - x.getFalseCase().accept(this); - return null; + public List visitITEExpression(ITEExpr x) { + final List result = new ArrayList<>(x.getTrueCase().accept(this)); + for (IncludeEdge edge : x.getFalseCase().accept(this)) { + addInto(result, edge, false); + } + return result; } @Override - public Result visitMemoryObject(MemoryObject a) { - address.add(a); - return new Result(a, null, BigInteger.ZERO, List.of()); + public List visitMemoryObject(MemoryObject a) { + return List.of(new IncludeEdge(objectVariables.get(a), TRIVIAL_MODIFIER)); } @Override - public Result visitRegister(Register r) { - register.add(r); - return new Result(null, r, BigInteger.ZERO, List.of()); + public List visitRegister(Register r) { + DerivedVariable phiVariable = getPhiNodeVariable(r, reader); + return List.of(includeEdge(phiVariable)); } @Override - public Result visitIntLiteral(IntLiteral v) { - return new Result(null, null, v.getValue(), List.of()); + public List visitExtractExpression(ExtractExpr extract) { + final List result = new ArrayList<>(); + for (IncludeEdge operand : extract.getOperand().accept(this)) { + DerivedVariable field = new DerivedVariable(operand.source, operand.modifier); + for (int index : extract.getIndices()) { + final DerivedVariable[] aggregate = operand.source.aggregate; + final DerivedVariable f = aggregate == null || aggregate.length <= index ? null : aggregate[index]; + if (f == null) { + field = compose(field, RELAXED_MODIFIER); + break; + } + field = compose(f, field.modifier); + } + result.add(includeEdge(field)); + } + return result; + } + + @Override + public List visitConstructExpression(ConstructExpr construct) { + final List result = new ArrayList<>(); + final var operands = new DerivedVariable[construct.getOperands().size()]; + final String name = construct.toString(); + for (int i = 0; i < construct.getOperands().size(); i++) { + final String fieldName = String.format("%s[%d]", name, i); + operands[i] = getOrNewVariable(construct.getOperands().get(i).accept(this), fieldName); + } + final Variable proxy = new Variable(null, operands, name); + totalVariables++; + for (DerivedVariable operand : operands) { + if (operand != null) { + addInclude(proxy, includeEdge(operand)); + } + } + result.add(new IncludeEdge(proxy, TRIVIAL_MODIFIER)); + return result; } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/VirtualAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/VirtualAliasAnalysis.java index f9cc3aac21..ad8a31d8da 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/VirtualAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/VirtualAliasAnalysis.java @@ -3,15 +3,19 @@ import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.memory.VirtualMemoryObject; +import java.util.List; + public class VirtualAliasAnalysis implements AliasAnalysis { private final AliasAnalysis wrappedAnalysis; + private final Config config; - private VirtualAliasAnalysis(AliasAnalysis analysis) { + private VirtualAliasAnalysis(AliasAnalysis analysis, Config config) { this.wrappedAnalysis = analysis; + this.config = config; } - public static AliasAnalysis wrap(AliasAnalysis analysis) { - return new VirtualAliasAnalysis(analysis); + public static AliasAnalysis wrap(AliasAnalysis analysis, Config config) { + return new VirtualAliasAnalysis(analysis, config); } @Override @@ -23,6 +27,11 @@ public boolean mustAlias(MemoryCoreEvent e1, MemoryCoreEvent e2) { return samePhysicalAddress(e1, e2) || wrappedAnalysis.mustAlias(e1, e2); } + @Override + public List mayMixedSizeAccesses(MemoryCoreEvent event) { + return config.defaultMayMixedSizeAccesses(event); + } + // GPU memory models make use of virtual addresses. // This models same_location_r from the PTX Alloy model. // Checking address1 and address2 hold the same physical address diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index f7523f2a0d..2074e22864 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -13,6 +13,7 @@ import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.event.arch.StoreExclusive; +import com.dat3m.dartagnan.program.event.arch.Xchg; import com.dat3m.dartagnan.program.event.arch.opencl.OpenCLRMWExtremum; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; @@ -27,6 +28,7 @@ import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; import com.dat3m.dartagnan.program.event.core.annotations.StringAnnotation; +import com.dat3m.dartagnan.program.event.core.InstructionBoundary; import com.dat3m.dartagnan.program.event.core.special.StateSnapshot; import com.dat3m.dartagnan.program.event.core.threading.*; import com.dat3m.dartagnan.program.event.functions.AbortIf; @@ -214,6 +216,14 @@ public static StringAnnotation newStringAnnotation(String annotation) { return new StringAnnotation(annotation); } + public static InstructionBoundary newInstructionBegin() { + return new InstructionBoundary(null, null); + } + + public static InstructionBoundary newInstructionEnd(InstructionBoundary begin) { + return new InstructionBoundary(null, begin); + } + public static Local newLocal(Register register, Expression expr) { return new Local(register, expr); } @@ -367,6 +377,10 @@ private Common() { public static StoreExclusive newExclusiveStore(Register register, Expression address, Expression value, String mo) { return new StoreExclusive(register, address, value, mo); } + + public static Xchg newXchg(Register register, Expression address, Expression storeValue) { + return new Xchg(register, address, storeValue); + } } // ============================================================================================= diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java index 0a8ec356f1..165f9d17a7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.program.event; import com.dat3m.dartagnan.program.event.arch.StoreExclusive; +import com.dat3m.dartagnan.program.event.arch.Xchg; import com.dat3m.dartagnan.program.event.arch.opencl.OpenCLRMWExtremum; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; @@ -60,8 +61,9 @@ public interface EventVisitor { default T visitLock(Lock e) { return visitMemEvent(e); } default T visitUnlock(Unlock e) { return visitMemEvent(e); } - // ------------------ AARCH64 Events ------------------ + // ------------------ Common Events ------------------ default T visitStoreExclusive(StoreExclusive e) { return visitMemEvent(e); } + default T visitXchg(Xchg xchg) { return visitMemEvent(xchg); }; // ------------------ Linux Events ------------------ default T visitLKMMAddUnless(LKMMAddUnless e) { return visitMemEvent(e); } @@ -120,4 +122,5 @@ public interface EventVisitor { default T visitSpirvXchg(SpirvXchg e) { return visitMemEvent(e); } default T visitSpirvCmpXchg(SpirvCmpXchg e) { return visitMemEvent(e); } default T visitSpirvRmwExtremum(SpirvRmwExtremum e) { return visitMemEvent(e); } + } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index 2fcf9bfe2d..a4f5d3262d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -37,6 +37,7 @@ private Tag() { } // Some events should not be optimized (e.g. fake dependencies) or deleted (e.g. bounds) public static final String NOOPT = "__NOOPT"; public static final String STARTLOAD = "__STARTLOAD"; + public static final String NO_INSTRUCTION = "__NO_INSTRUCTION"; // ============================================================================================= // =========================================== ARMv8 =========================================== @@ -46,18 +47,17 @@ public static final class ARMv8 { private ARMv8() { } - public static final String MO_RX = "RX"; public static final String MO_REL = "L"; public static final String MO_ACQ = "A"; public static final String MO_ACQ_PC = "Q"; public static String extractStoreMoFromCMo(String cMo) { - return cMo.equals(C11.MO_SC) || cMo.equals(C11.MO_RELEASE) || cMo.equals(C11.MO_ACQUIRE_RELEASE) ? MO_REL : MO_RX; + return cMo.equals(C11.MO_SC) || cMo.equals(C11.MO_RELEASE) || cMo.equals(C11.MO_ACQUIRE_RELEASE) ? MO_REL : ""; } public static String extractLoadMoFromCMo(String cMo) { //TODO: What about MO_CONSUME loads? - return cMo.equals(C11.MO_SC) || cMo.equals(C11.MO_ACQUIRE) || cMo.equals(C11.MO_ACQUIRE_RELEASE) ? MO_ACQ : MO_RX; + return cMo.equals(C11.MO_SC) || cMo.equals(C11.MO_ACQUIRE) || cMo.equals(C11.MO_ACQUIRE_RELEASE) ? MO_ACQ : ""; } public static String extractStoreMoFromLKMo(String lkMo) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/Xchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/Xchg.java new file mode 100644 index 0000000000..59e020bc1c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/Xchg.java @@ -0,0 +1,32 @@ +package com.dat3m.dartagnan.program.event.arch; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.common.RMWXchgBase; + +public class Xchg extends RMWXchgBase { + + public Xchg(Register register, Expression address, Expression value) { + super(register, address, value, ""); + } + + private Xchg(Xchg other){ + super(other); + } + + @Override + public String defaultString() { + return String.format("%s <- xchg(*%s, %s)", resultRegister, address, storeValue); + } + + @Override + public Xchg getCopy(){ + return new Xchg(this); + } + + @Override + public T accept(EventVisitor visitor) { + return visitor.visitXchg(this); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/InstructionBoundary.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/InstructionBoundary.java new file mode 100644 index 0000000000..0346443b4f --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/InstructionBoundary.java @@ -0,0 +1,54 @@ +package com.dat3m.dartagnan.program.event.core; + +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.Event; + +import java.util.ArrayList; +import java.util.List; + +import static com.google.common.base.Preconditions.checkState; + +/** + * Instances of this class occur in pairs, where the link is owned by the later event. + * The "begin" boundary must be a dominator of the "end" boundary, but the opposite may not be true. + * + *

+ * Visible events enclosed by such a pair are said to originate from the same instruction. + * In execution graphs, they shall be {@code si}-related. + */ +public final class InstructionBoundary extends AbstractEvent { + + private final InstructionBoundary begin; + + public InstructionBoundary(Void ignore, InstructionBoundary b) { + begin = b; + } + + private InstructionBoundary(InstructionBoundary other) { + super(other); + begin = other.begin; + } + + public List getInstructionEvents() { + if (begin == null) { + return List.of(); + } + checkState(begin.getFunction() == getFunction() && begin.getGlobalId() < getGlobalId(), "Broken instruction"); + final var events = new ArrayList(); + for (Event event = begin.getSuccessor(); event != this; event = event.getSuccessor()) { + events.add(event); + } + return events; + } + + @Override + protected String defaultString() { + final String format = begin == null ? "=== begin instruction %d ===" : "=== end instruction %d ==="; + return String.format(format, (begin == null ? this : begin).getGlobalId()); + } + + @Override + public Event getCopy() { + return new InstructionBoundary(this); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java index f891b25eed..049ccb54a3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java @@ -17,9 +17,26 @@ public class Memory { private final Type ptrType = TypeFactory.getInstance().getPointerType(); private final IntegerType archType = TypeFactory.getInstance().getArchType(); private final Expression defaultAlignment = ExpressionFactory.getInstance().makeValue(8, archType); + private final boolean bigEndian; private int nextIndex = 1; + public Memory() { + this(false); + } + + public Memory(boolean bigEndian) { + this.bigEndian = bigEndian; + } + + public boolean isBigEndian() { + return bigEndian; + } + + public boolean isLittleEndian() { + return !bigEndian; + } + // Generates a new, statically allocated memory object. public MemoryObject allocate(int size) { Preconditions.checkArgument(size > 0, "Illegal allocation. Size must be positive"); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java index ebb7f6348f..5ce55e137b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java @@ -34,7 +34,7 @@ public static CoreCodeVerification fromConfig(Configuration config) { Load.class, Store.class, Init.class, GenericMemoryEvent.class, GenericVisibleEvent.class, CondJump.class, IfAsJump.class, ExecutionStatus.class, Label.class, Local.class, Skip.class, RMWStore.class, RMWStoreExclusive.class, Alloc.class, - Assume.class, Assert.class, + Assume.class, Assert.class, InstructionBoundary.class, ThreadCreate.class, ThreadJoin.class, ThreadArgument.class, ThreadStart.class, ThreadReturn.class, ControlBarrier.class, NamedBarrier.class, BeginAtomic.class, EndAtomic.class, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index 1b6d0769cf..3b5fda0f09 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -62,21 +62,25 @@ public class Intrinsics { private enum AssertionType { USER, OVERFLOW, INVALIDDEREF, UNKNOWN_FUNCTION } + private final boolean detectMixedSizeAccesses; + private static final TypeFactory types = TypeFactory.getInstance(); private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); //FIXME This might have concurrency issues if processing multiple programs at the same time. private BeginAtomic currentAtomicBegin; - private Intrinsics() { + private Intrinsics(boolean msa) { + detectMixedSizeAccesses = msa; } public static Intrinsics newInstance() { - return new Intrinsics(); + return new Intrinsics(false); } - public static Intrinsics fromConfig(Configuration config) throws InvalidConfigurationException { - Intrinsics instance = newInstance(); + public static Intrinsics fromConfig(Configuration config, boolean detectMixedSizeAccesses) + throws InvalidConfigurationException { + Intrinsics instance = new Intrinsics(detectMixedSizeAccesses); config.inject(instance); return instance; } @@ -1462,17 +1466,23 @@ private List inlineMemCpy(FunctionCall call) { final int count = countValue.getValueAsInt(); final List replacement = new ArrayList<>(2 * count + 1); - for (int i = 0; i < count; i++) { + //FIXME without MSA detection, each byte is treated as a 64-bit value. + final IntegerType type = detectMixedSizeAccesses ? types.getIntegerType(8 * count) : types.getArchType(); + final int typeSize = detectMixedSizeAccesses ? count : 1; + for (int i = 0; i < count; i += typeSize) { final Expression offset = expressions.makeValue(i, types.getArchType()); final Expression srcAddr = expressions.makeAdd(src, offset); final Expression destAddr = expressions.makeAdd(dest, offset); - // FIXME: We have no other choice but to load ptr-sized chunks for now - final Register reg = caller.getOrNewRegister("__memcpy_" + i, types.getArchType()); + final Register reg = caller.getOrNewRegister("__memcpy_" + i, type); - replacement.addAll(List.of( - EventFactory.newLoad(reg, srcAddr), - newStore(destAddr, reg) - )); + final Event load = EventFactory.newLoad(reg, srcAddr); + final Event store = EventFactory.newStore(destAddr, reg); + + // communicate to Tearing to not create same-instruction blocks + load.addTags(Tag.NO_INSTRUCTION); + store.addTags(Tag.NO_INSTRUCTION); + + replacement.addAll(List.of(load, store)); } if (call instanceof ValueFunctionCall valueCall) { // std.memcpy returns the destination address, llvm.memcpy has no return value diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java index 65423661b5..b69592dcd9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java @@ -38,6 +38,9 @@ public class MemToReg implements FunctionProcessor { private static final Logger logger = LogManager.getLogger(MemToReg.class); + private static final TypeFactory types = TypeFactory.getInstance(); + private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); + private MemToReg() { } @@ -56,11 +59,9 @@ private Matcher analyze(Function function) { final var matcher = new Matcher(); // Initially, all locally-allocated addresses are potentially promotable. for (final Alloc allocation : function.getEvents(Alloc.class)) { - final Map fields = getPrimitiveReplacementTypes(allocation); // Allocations will usually not have users. Otherwise, their object is not promotable. - if (fields == null || allocation.getUsers().isEmpty()) { + if (allocation.getUsers().isEmpty()) { matcher.reachabilityGraph.put(allocation, new HashSet<>()); - matcher.fields.put(allocation, fields); } } // This loop should terminate, since back jumps occur, only if changes were made. @@ -73,61 +74,140 @@ private Matcher analyze(Function function) { } private void promoteAll(Function function, Matcher matcher) { - final ExpressionFactory expressions = ExpressionFactory.getInstance(); // Replace every unmarked address. - final HashMap> replacingRegisters = new HashMap<>(); - for (final Alloc allocation : function.getEvents(Alloc.class)) { - if (matcher.reachabilityGraph.containsKey(allocation)) { - final Map registerTypes = getPrimitiveReplacementTypes(allocation); - if (registerTypes != null) { - replacingRegisters.put(allocation, new HashMap<>(Maps.transformValues(registerTypes, function::newRegister))); - boolean deleted = allocation.tryDelete(); - assert deleted : "Allocation cannot be removed, probably because it has remaining users."; - } + final Map promotableObjects = collectPromotableObjects(function, matcher); + final Map> updates = new HashMap<>(Maps.toMap(promotableObjects.keySet(), k -> List.of())); + // Mark all loads and stores to replaceable storage. + updates.putAll(Maps.transformEntries(matcher.accesses, (k, v) -> promoteAccess(k, v, promotableObjects))); + // Mark involved local GEP assignments. + for (final Map.Entry entry : matcher.assignments.entrySet()) { + if (promotableObjects.containsKey(entry.getValue().base)) { + updates.put(entry.getKey(), List.of()); } } + updates.values().removeIf(Objects::isNull); + // If some events cannot be removed, give up. + //TODO Build a dependency graph and replace the events that can be removed. + if (updates.keySet().stream().anyMatch(e -> !e.getUsers().isEmpty())) { + logger.warn("Could not remove events, because some are still used."); + return; + } + // Replace events. + for (Map.Entry> update : updates.entrySet()) { + update.getKey().replaceBy(update.getValue()); + } + // Evaluate the process. + if (!updates.isEmpty()) { + final long loadCount = updates.keySet().stream().filter(Load.class::isInstance).count(); + final long storeCount = updates.keySet().stream().filter(Store.class::isInstance).count(); + logger.debug("Removed {} loads and {} stores in function \"{}\".", loadCount, storeCount, function.getName()); + } + } - int loadCount = 0, storeCount = 0; - // Replace all loads and stores to replaceable storage. - for (final Map.Entry entry : matcher.accesses.entrySet()) { - final MemoryEvent event = entry.getKey(); - final AddressOffset access = entry.getValue(); - final Map registers = access == null ? null : replacingRegisters.get(access.base); - if (registers == null || !registers.containsKey((int)access.offset)) { + private Map collectPromotableObjects(Function function, Matcher matcher) { + final Map promotableObjects = new HashMap<>(); + for (final Alloc allocation : function.getEvents(Alloc.class)) { + if (!matcher.reachabilityGraph.containsKey(allocation)) { continue; } - - final Register memreg = registers.get((int)access.offset); - if (event instanceof Load load) { - final Register reg = load.getResultRegister(); - assert load.getUsers().isEmpty(); - load.replaceBy(EventFactory.newLocal(reg, expressions.makeCast(memreg, reg.getType()))); - loadCount++; - } else if (event instanceof Store store) { - assert store.getUsers().isEmpty(); - store.replaceBy(EventFactory.newLocal(memreg, expressions.makeCast(store.getMemValue(), memreg.getType()))); - storeCount++; + final Set registerTypes = new HashSet<>(); + for (Map.Entry entry : matcher.accesses.entrySet()) { + if (!entry.getValue().base.equals(allocation)) { + continue; + } + final Type accessType = entry.getKey().getAccessType(); + final int accessSize = types.getMemorySizeInBytes(accessType); + registerTypes.add(new Field((int) entry.getValue().offset, accessSize, accessType)); } + final Map registers = Maps.asMap(registerTypes, f -> newRegister(allocation, f)); + promotableObjects.put(allocation, new Promotable(registers)); } - // Remove involved local assignments. - for (final Map.Entry entry : matcher.assignments.entrySet()) { - if (replacingRegisters.containsKey(entry.getValue().base)) { - assert entry.getKey().getUsers().isEmpty(); - entry.getKey().tryDelete(); + return promotableObjects; + } + + private Register newRegister(Alloc allocation, Field field) { + return allocation.getFunction().newUniqueRegister("memToReg", field.type); + } + + private List promoteAccess(MemoryCoreEvent event, AddressOffset access, + Map promotableObjects) { + final Promotable object = access == null ? null : promotableObjects.get(access.base); + final Type accessType = event.getAccessType(); + final int accessSize = types.getMemorySizeInBytes(accessType); + final Field field = object == null ? null : new Field((int) access.offset, accessSize, accessType); + final Register memreg = field == null ? null : object.replacingRegisters.get(field); + if (memreg == null) { + return null; + } + final List replacement = new ArrayList<>(); + if (event instanceof Load load) { + final Register reg = load.getResultRegister(); + assert load.getUsers().isEmpty(); + replacement.add(EventFactory.newLocal(reg, expressions.makeCast(memreg, reg.getType()))); + } else if (event instanceof Store store) { + assert store.getUsers().isEmpty(); + replacement.add(EventFactory.newLocal(memreg, expressions.makeCast(store.getMemValue(), accessType))); + updateMixedRegisters(memreg, field, object, replacement); + } + return replacement; + } + + private void updateMixedRegisters(Register memreg, Field field, Promotable object, List replacement) { + // Update all registers representing overlapping byte ranges. + if (!object.hasMixedAccesses) { + return; + } + final boolean bigEndian = memreg.getFunction().getProgram().getMemory().isBigEndian(); + assert memreg.getType().equals(field.type); + final Type integerType = types.getIntegerType(types.getMemorySizeInBits(field.type)); + final Expression storedValue = expressions.makeCast(memreg, integerType); + final int end = field.offset + field.size; + for (Map.Entry otherEntry : object.replacingRegisters.entrySet()) { + final Field other = otherEntry.getKey(); + if (other.equals(field) || !other.overlaps(field)) { + continue; } + final Register otherRegister = otherEntry.getValue(); + final int overlapBegin = Integer.max(field.offset, other.offset); + final int overlapEnd = Integer.min(end, other.offset + other.size); + final int firstByte = bigEndian ? end - overlapEnd : overlapBegin - field.offset; + final Expression truncated = extractBytes(storedValue, firstByte, overlapEnd - overlapBegin); + final Type otherType = otherRegister.getType(); + final int otherBytes = types.getMemorySizeInBytes(otherType); + final Type otherIntegerType = types.getIntegerType(8 * otherBytes); + final Expression formerValue = expressions.makeCast(otherRegister, otherIntegerType); + final int frontBytes = overlapBegin - other.offset; + final int backBytes = other.offset + other.size - overlapEnd; + final int lowBytes = bigEndian ? backBytes : frontBytes; + final int highBytes = bigEndian ? frontBytes : backBytes; + final Expression lowBits = extractBytes(formerValue, 0, lowBytes); + final Expression highBits = extractBytes(formerValue, otherBytes - highBytes, highBytes); + final List operands = Arrays.asList(lowBits, truncated, highBits); + final List filteredOperands = operands.stream().filter(Objects::nonNull).toList(); + final Expression extended = expressions.makeIntConcat(filteredOperands); + replacement.add(EventFactory.newLocal(otherRegister, expressions.makeCast(extended, otherType))); } - if (loadCount + storeCount > 0) { - logger.debug("Removed {} loads and {} stores in function \"{}\".", loadCount, storeCount, function.getName()); + } + + private Expression extractBytes(Expression operand, int offset, int size) { + return size <= 0 ? null : expressions.makeIntExtract(operand, 8 * offset, 8 * (offset + size) - 1); + } + + private static final class Promotable { + private final Map replacingRegisters; + // Redundant flag for the likely case, that a promoted object + private final boolean hasMixedAccesses; + + private Promotable(Map fields) { + replacingRegisters = new HashMap<>(fields); + hasMixedAccesses = hasMixedAccesses(replacingRegisters.keySet()); } } - private Map getPrimitiveReplacementTypes(Alloc allocation) { - if (!(allocation.getArraySize() instanceof IntLiteral sizeExpression)) { - return null; + private record Field(int offset, int size, Type type) { + private boolean overlaps(Field other) { + return Long.max(offset, other.offset) < Long.min(offset + size, other.offset + other.size); } - final TypeFactory typeFactory = TypeFactory.getInstance(); - final int size = sizeExpression.getValueAsInt(); - return typeFactory.decomposeIntoPrimitives(typeFactory.getArrayType(allocation.getAllocationType(), size)); } // Invariant: base != null @@ -140,13 +220,23 @@ private AddressOffset increase(long o) { // Invariant: register != null private record RegisterOffset(Register register, long offset) {} + // Checks if mixed-size accesses to a promotable object were collected. + private static boolean hasMixedAccesses(Set registerTypes) { + final List registerTypeList = List.copyOf(registerTypes); + for (int i = 0; i < registerTypeList.size(); i++) { + for (int j = 0; j < i; j++) { + if (registerTypeList.get(i).overlaps(registerTypeList.get(j))) { + return true; + } + } + } + return false; + } + // Processes events in program order. // Returns a label, if it is program-ordered before the current event and its symbolic state was updated. private static final class Matcher implements EventVisitor