From c081ca34ff3c41f656b526c7d9a95f65016029c5 Mon Sep 17 00:00:00 2001
From: Junghee Lim <junghee@grammatech.com>
Date: Tue, 4 Jun 2024 11:42:39 -0400
Subject: [PATCH 1/2] Pick the max alignment when there are multiple alignments
 for an EA

---
 .../ex_aligned_data_in_code/ex_original.s     |  4 +++-
 src/datalog/main.dl                           | 22 ++++++++++++++-----
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/examples/asm_examples/ex_aligned_data_in_code/ex_original.s b/examples/asm_examples/ex_aligned_data_in_code/ex_original.s
index 65a2ddfa..dd242e55 100644
--- a/examples/asm_examples/ex_aligned_data_in_code/ex_original.s
+++ b/examples/asm_examples/ex_aligned_data_in_code/ex_original.s
@@ -19,7 +19,9 @@ main:
     lea data128.2(%rip), %rax
     movdqa 0(%rax), %xmm1
 
-    # Load data into YMM register using movdqa: `data256` needs to be aligned.
+    # Load data into XMM and YMM using vmovapd: `data256` needs to be 32-bit
+    # aligned (YMM) instead of being 16-bit aligned (XMM).
+    vmovapd data256(%rip), %xmm0
     vmovapd data256(%rip), %ymm0
 
     # Load data into YMM register using vmovups: `data256u` does not need to be aligned.
diff --git a/src/datalog/main.dl b/src/datalog/main.dl
index f2446937..be81cd8a 100644
--- a/src/datalog/main.dl
+++ b/src/datalog/main.dl
@@ -689,16 +689,14 @@ halt(EA):-
     instruction_get_operation(EA,Operation).
 
 /**
-Information about alignment in bits for a given address
+Auxiliary predicate that builds initial alignments from `alignment_required`:
+the max alignment is picked for an EA later.
 */
-.decl alignment(EA:address,AlignInBits:unsigned)
-.output alignment
-
-alignment(0,0):- false.
+.decl alignment_candidate(EA:address,AlignInBits:unsigned)
 
 // Data in code needs to be aligned when referenced by instruction that
 // requires aligned memory: e.g., some SIMD instructions
-alignment(DataEA, AlignInBits):-
+alignment_candidate(DataEA, AlignInBits):-
     arch.alignment_required(EA,AlignInBits),
     (
         pc_relative_operand(EA,_,DataEA);
@@ -708,6 +706,18 @@ alignment(DataEA, AlignInBits):-
     DataEA >= Begin,
     DataEA < End.
 
+/**
+Information about alignment in bits for a given address
+*/
+.decl alignment(EA:address,AlignInBits:unsigned)
+.output alignment
+
+alignment(0,0):- false.
+
+alignment(DataEA, AlignInBits):-
+    alignment_candidate(DataEA, AlignInBits),
+    AlignInBits = max X: {alignment_candidate(DataEA, X)}.
+
 //////////////////////////////////////////////////////////////////////////////////
 // Operations to abstract features of instructions
 

From 797b42975320ce3f9c6a307601cfe5e24d1be6f4 Mon Sep 17 00:00:00 2001
From: Junghee Lim <junghee@grammatech.com>
Date: Tue, 11 Jun 2024 14:30:22 -0400
Subject: [PATCH 2/2] Remove an unnecessary line

---
 src/datalog/main.dl | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/datalog/main.dl b/src/datalog/main.dl
index be81cd8a..503a16e6 100644
--- a/src/datalog/main.dl
+++ b/src/datalog/main.dl
@@ -712,8 +712,6 @@ Information about alignment in bits for a given address
 .decl alignment(EA:address,AlignInBits:unsigned)
 .output alignment
 
-alignment(0,0):- false.
-
 alignment(DataEA, AlignInBits):-
     alignment_candidate(DataEA, AlignInBits),
     AlignInBits = max X: {alignment_candidate(DataEA, X)}.