Merge pull request #960 from GaloisInc/issue958

Fix the bit-order convention for `extractWord` in the What4 backend
GaloisInc · Nov 12, 2020 · d00ff6b · d00ff6b
2 parents a7d352b + f730750
commit d00ff6b
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs
@@ -325,7 +325,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
        return (l, r)
 
   extractWord (What4 sym _) bits idx bv =
-    liftIO $ SW.bvSliceBE sym idx bits bv
+    liftIO $ SW.bvSliceLE sym idx bits bv
 
   wordEq                (What4 sym _) x y = liftIO (SW.bvEq sym x y)
   wordLessThan          (What4 sym _) x y = liftIO (SW.bvult sym x y)

diff --git a/tests/issues/issue958.icry b/tests/issues/issue958.icry
@@ -0,0 +1,5 @@
+:set prover=sbv-z3
+:prove (\x y -> split (x#y) == [x :[64] ,y])
+
+:set prover=w4-z3
+:prove (\x y -> split (x#y) == [x :[64] ,y])
diff --git a/tests/issues/issue958.icry.stdout b/tests/issues/issue958.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+Q.E.D.
+Q.E.D.