From 5ba13e1d42cc06a97a319238344aebb38b8dc1cd Mon Sep 17 00:00:00 2001
From: Ryan <mccleeary@galois.com>
Date: Thu, 28 Sep 2023 08:13:43 -0600
Subject: [PATCH 1/3] Fix bound check in SetupValue for LLVM

---
 src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index c021372a03..11b102b4ac 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -502,7 +502,7 @@ typeOfSetupValue cc env nameEnv val =
                Right memTy' ->
                  case memTy' of
                    Crucible.ArrayType n memTy''
-                     | fromIntegral i <= n -> return (Crucible.PtrType (Crucible.MemType memTy''))
+                     | fromIntegral i < n -> return (Crucible.PtrType (Crucible.MemType memTy''))
                      | otherwise -> throwError $ unwords $
                          [ "typeOfSetupValue: array type index out of bounds"
                          , "(index: " ++ show i ++ ")"
@@ -574,7 +574,7 @@ resolveSetupElemOffset cc env nameEnv v i = do
            Right memTy' ->
              case memTy' of
                Crucible.ArrayType n memTy''
-                 | fromIntegral i <= n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
+                 | fromIntegral i < n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
                Crucible.StructType si ->
                  case Crucible.siFieldOffset si i of
                    Just d -> return d

From 56f13b4b2bebcc39eb249764e41a5636d514bd26 Mon Sep 17 00:00:00 2001
From: Ryan <mccleeary@galois.com>
Date: Thu, 28 Sep 2023 08:35:35 -0600
Subject: [PATCH 2/3] Add int test for bound check

---
 intTests/test_llvm_bound_check/Makefile  |   2 ++
 intTests/test_llvm_bound_check/bound.bc  | Bin 0 -> 2224 bytes
 intTests/test_llvm_bound_check/bound.c   |   5 +++++
 intTests/test_llvm_bound_check/bound.saw |  15 +++++++++++++++
 intTests/test_llvm_bound_check/test.sh   |  10 ++++++++++
 5 files changed, 32 insertions(+)
 create mode 100644 intTests/test_llvm_bound_check/Makefile
 create mode 100644 intTests/test_llvm_bound_check/bound.bc
 create mode 100644 intTests/test_llvm_bound_check/bound.c
 create mode 100644 intTests/test_llvm_bound_check/bound.saw
 create mode 100644 intTests/test_llvm_bound_check/test.sh

diff --git a/intTests/test_llvm_bound_check/Makefile b/intTests/test_llvm_bound_check/Makefile
new file mode 100644
index 0000000000..f10757bb1b
--- /dev/null
+++ b/intTests/test_llvm_bound_check/Makefile
@@ -0,0 +1,2 @@
+bound.bc : bound.c
+	clang -c -emit-llvm -o bound.bc bound.c
diff --git a/intTests/test_llvm_bound_check/bound.bc b/intTests/test_llvm_bound_check/bound.bc
new file mode 100644
index 0000000000000000000000000000000000000000..d50645634eafe99fdf1e39cf8972451a8b56a0b7
GIT binary patch
literal 2224
zcmYjSeQXow8Gp|ga)vl(Lp?~w-El`kYqf=590+!7OaACu!}5pO_D3c$#ZF?+S@UtR
zgFiw$opV8#YN0bIe^?rmY!y{Z`!Z_&U=pfgJELCaq7-!%>Y~VQ3<Q+2Xk`=9Ds9he
z!nRj;@B6&Z`|*7Jp66X(I?#fk8R1WB5&AbYw`Xbn1Tc01Z%`+8p8nxSq2K;%@%Jrf
z<URs;f)1faK(uHCq=ET<_^DLKC0DuWRI|Zsy-dvNj_lI5b4@=Rly%?HxG%T3hYe<<
zMcek>J!bQqS6UW2Uf-wA8(fz)!)5JtBky@*j{g&3HqW-bY<fA}^>+U3CB9UKd*9^|
z0&&QExUA&|-$24Eof(~Q1iJQ@bQi9s{pR7beCN>2(lx6_6y2gh)QE4QJ?KmuLSZ;}
zaJ=&=wuz9?ZWHNjDe`>9#T9exO0Kn9WA7B$%^XuFBsDInJ$^N!rJ_h1PpCavDygLs
zvN|QH(XbNJQqxXK=IS|ah2Za}xMG0$9By!N>nUy}z--podaiXj$5jf<ii`Wg&)sny
zS|OH5Ijc%(HEN=!!^)(rPNO2hRa02{7XpoDxT1@@ontn0t(6>8OmUA~a2qF|(5jIP
z)zhy`rqxNma-xk&mZ?NmjRVcA@hp`{t8pGSkWpFf(Nf7Ub$*F_Hnrr*Xqbw@PEnoq
zQ!$ZB%#k*j`qiWfABmg5SWG0fY7+P$LT*S&Q;{$hnskEBa9e}OG>9<O3p?|aT~aJs
zd=|u=Oe@lJruDzf?Ejd(JIn@WRh`6_lkc=q@1P!o8>KOH&?$%$#?%Y5PV_<^Toucc
zy<tU?sRTp=J6@eksL3VOk|9sZ@F}eUA3e58PjAy>X*%Ylz{aW7=7$C<B2&|ieymDI
z`5pd;4bHa(U9yS(i|!-wszyT~8B1<79(DF;jpy_Tl{G{&u*@7FYj0nAe)o%S-fHrk
z-feWdj4ms>4to9p*1NSbvs`0BM#3@YvCNj{-7=L-P|?h!?mp6gWuTwPbhpmU6$>oH
zH6-q8Y*P+aNJrV@m?s^T#Qc;*orjotRY{_zB{G&!C0=c>?4`HTbWPNci~5aidfP{L
z8<yF1fw?QN#Q+x)-?iOTY^xsYB5A*=*k?&wW!o6@Q|H6f$uPKzIw@nQNf2@q6??i1
zu8qs;0Qj#Bz@#QKsaGFw(~qn4KbGh%ksK@o?sE*l4*InKvm!9dfXhJh=V_0%?6GDV
z{f&}k!D9jZER<dYq2J8dJ|k`UlJ4UXRq9tGk}?&>ftqSlr?P7M?eFU!BmLifbUjUP
zIQ2E2-U2Il6T4QxK))j}YbkE6%G7J@BZ3RHow4LSy;l@l#n-uGh+mB-s6^&W-;=Z+
zdw}~%BfA84y}<sIfb?T30=pe({=o&sQYqQ;9tSw&o1(q$vCYA>H2=pvV5u4heIR2^
zR3wu+yJ4WWmgsvv`fIVHaL2{fYX|Pu*mY3A+iuG%jz#6*Y{@e3u~tg<8wG2*1UA|$
z-o;5RWDzw94(wOk|9Xqw^6S5<HgEI#d!qgxum7iy9yib%A`R28tIZFqblpck6+6D%
z3P2{acWVc>1opnbE(<I~a8o!G;(uwo>2cg3tqY2^(ti`855`V|o?b{uwf)Zz=)Z~j
zT9tn2)IZFEloCNkuTfyjKn9?KJv_Avp-j!Xtkn{@&H<6CIG3|fO;}us3QVYTNTh2x
zzIwRip6C&jb8S@As}5w<w`DkceSxsgm+T8A%c`dr;8X#R>Ab?X+yM?$y<K3xmolOx
zkI-v?^$6$XJ#)JD-4U~w??}yGy7cMmS%YcV-eq>bmloddH(W!fBgfhJP&g17h>lDL
zeWyHpUoaLNJr|z}42}jvk-%8+s5CJ$J{633C&q$<kzkx38V!v9n2!Y`(UFO9zN_b$
zc&w*G>k?-S+74|21_R8xO8%ygb>!jBZrzH%BARBqJifBmKVu#o`tYsj$oY<654{rY
z8fvlq;@}0}{tr%FxcJHMJ~?vnH<gRy3rht073AwnU_;BE2$Vah4E<6De2?8`T`kSr
zXKv+MH{l^D;1F##@U{Q=hM#`m1K8^87`*xiKKe;sPEkoyBdZcBAOd5mU%FDVEE2Y>
ziesUqc?%MhS*tN?JW~(gezWm9tmc^VGav*Cg#HPyule*)8(QWX0ii%O^r-<MTyv<3
z{i<TS0!c<XvWguNE?vSkF~B2u$)Gkixn6~>jXL?+KBz%^orZKVPwdq-ISKF24LalS
zC@iB%9w8D&Gi^9Li@wBUqXppsJp|M~a$y@Y@B+Rc%kJBu`(eZlk9bYO6KGgbaAo5>
zrtunX&(|^iocAKojiSE8!|yKY#5)lB5$MngBj|viWfXcA_CRE;=lIcpB#j1-js=D$
YqKU3<fP*+Vac+G0*w8=-@BRPwA3$l`!vFvP

literal 0
HcmV?d00001

diff --git a/intTests/test_llvm_bound_check/bound.c b/intTests/test_llvm_bound_check/bound.c
new file mode 100644
index 0000000000..bdfed48120
--- /dev/null
+++ b/intTests/test_llvm_bound_check/bound.c
@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t f(uint32_t x[2]) {
+  return x[1];
+}
\ No newline at end of file
diff --git a/intTests/test_llvm_bound_check/bound.saw b/intTests/test_llvm_bound_check/bound.saw
new file mode 100644
index 0000000000..0eada15c21
--- /dev/null
+++ b/intTests/test_llvm_bound_check/bound.saw
@@ -0,0 +1,15 @@
+let f_spec = do {
+    x <- llvm_alloc (llvm_array 2 (llvm_int 32));
+    a <- llvm_fresh_var "a" (llvm_int 32);
+    llvm_points_to (llvm_elem x 1) (llvm_term a);
+
+    // BAD: Out-of-bounds write
+    llvm_points_to (llvm_elem x 2) (llvm_term a);
+
+    llvm_execute_func [x];
+
+    llvm_return (llvm_term a);
+};
+
+m <- llvm_load_module "bound.bc";
+llvm_verify m "f" [] false f_spec z3;
\ No newline at end of file
diff --git a/intTests/test_llvm_bound_check/test.sh b/intTests/test_llvm_bound_check/test.sh
new file mode 100644
index 0000000000..ad62bae603
--- /dev/null
+++ b/intTests/test_llvm_bound_check/test.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+set -e
+
+# We want to ensure there isn't a memory store failure and this is caught during type checking of Setup Value
+if $SAW bound.saw | grep -q "Memory store failed"; then
+    exit 1
+else
+    exit 0
+fi

From 29f9c9e5849cd48c210fdeb050aa297f6055e434 Mon Sep 17 00:00:00 2001
From: Ryan <mccleeary@galois.com>
Date: Thu, 28 Sep 2023 10:46:01 -0600
Subject: [PATCH 3/3] Change check in unit test for type check error.

---
 intTests/test_llvm_bound_check/Makefile | 2 +-
 intTests/test_llvm_bound_check/test.sh  | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/intTests/test_llvm_bound_check/Makefile b/intTests/test_llvm_bound_check/Makefile
index f10757bb1b..f48deac7d9 100644
--- a/intTests/test_llvm_bound_check/Makefile
+++ b/intTests/test_llvm_bound_check/Makefile
@@ -1,2 +1,2 @@
 bound.bc : bound.c
-	clang -c -emit-llvm -o bound.bc bound.c
+	clang -c -emit-llvm -frecord-command-line -o $@ $<
diff --git a/intTests/test_llvm_bound_check/test.sh b/intTests/test_llvm_bound_check/test.sh
index ad62bae603..bc198584b3 100644
--- a/intTests/test_llvm_bound_check/test.sh
+++ b/intTests/test_llvm_bound_check/test.sh
@@ -3,8 +3,8 @@
 set -e
 
 # We want to ensure there isn't a memory store failure and this is caught during type checking of Setup Value
-if $SAW bound.saw | grep -q "Memory store failed"; then
-    exit 1
-else
+if $SAW bound.saw | grep -q "array type index out of bounds"; then
     exit 0
+else
+    exit 1
 fi