Add test case for joinBytes

test/test.hs

@@ -682,6 +682,11 @@ tests = testGroup "hevm"
     , testProperty "simplifyProp-equivalence-sym" $ \(p) -> prop $ do
         let simplified = Expr.simplifyProp p
         checkEquivPropAndLHS p simplified
+    , testProperty "simplify-joinbytes" $ \(SymbolicJoinBytes exprList) -> prop $ do
+        let x = joinBytesFromList exprList
+        let simplified = Expr.simplify x
+        y <- checkEquiv x simplified
+        assertBoolM "Must be equal" y
     , testProperty "simpProp-equivalence-sym-Prop" $ \(ps :: [Prop]) -> prop $ do
         let simplified = pand (Expr.simplifyProps ps)
         checkEquivPropAndLHS (pand ps) simplified
@@ -4012,6 +4017,23 @@ instance Arbitrary (Expr EWord) where
 instance Arbitrary (Expr Byte) where
   arbitrary = sized genByte
 
+newtype SymbolicJoinBytes = SymbolicJoinBytes [Expr Byte]
+  deriving (Eq, Show)
+
+instance Arbitrary SymbolicJoinBytes where
+  arbitrary = liftM SymbolicJoinBytes $ replicateM 32 arbitrary
+
+joinBytesFromList :: [Expr Byte] -> Expr EWord
+joinBytesFromList [a0, a1, a2, a3, a4, a5, a6, a7,
+                   a8, a9, a10, a11, a12, a13, a14, a15,
+                   a16, a17, a18, a19, a20, a21, a22, a23,
+                   a24, a25, a26, a27, a28, a29, a30, a31] =
+  JoinBytes a0 a1 a2 a3 a4 a5 a6 a7
+            a8 a9 a10 a11 a12 a13 a14 a15
+            a16 a17 a18 a19 a20 a21 a22 a23
+            a24 a25 a26 a27 a28 a29 a30 a31
+joinBytesFromList _ = internalError "List must contain exactly 32 elements"
+
 instance Arbitrary (Expr Buf) where
   arbitrary = sized defaultBuf