SyGuS, find SMT array write of a fixed size

examples/aes/aes.saw

@@ -5,20 +5,22 @@ print "Proving encrypt_lemma...";
 encrypt_lemma <-
   time (prove_print (unint_z3 ["AESRound"])
   (rewrite (cryptol_ss())
-  {{ \(state0 : State) (ks : [9]RoundKey) ->
+  {{ \(state0 : State) (ks : [13]RoundKey) ->
       (rounds where rounds = [state0] # [ AESRound (rk, s) | rk <- ks | s <- rounds ]) ! 0 ==
-        AESRound(ks@8,AESRound(ks@7,AESRound(ks@6,AESRound(ks@5,AESRound(ks@4,
-          AESRound(ks@3,AESRound(ks@2,AESRound(ks@1,AESRound(ks@0,state0)))))))))
+        AESRound(ks@12,AESRound(ks@11,AESRound(ks@10,AESRound(ks@9,
+          AESRound(ks@8,AESRound(ks@7,AESRound(ks@6,AESRound(ks@5,AESRound(ks@4,
+            AESRound(ks@3,AESRound(ks@2,AESRound(ks@1,AESRound(ks@0,state0)))))))))))))
   }}));
 
 print "Proving decrypt_lemma...";
 decrypt_lemma <-
   time (prove_print (unint_z3 ["AESInvRound"])
   (rewrite (cryptol_ss())
-  {{ \(state0 : State) (ks : [9]RoundKey) ->
+  {{ \(state0 : State) (ks : [13]RoundKey) ->
       (rounds where rounds = [state0] # [ AESInvRound (rk, s) | rk <- reverse ks | s <- rounds ]) ! 0 ==
         AESInvRound(ks@0,AESInvRound(ks@1,AESInvRound(ks@2,AESInvRound(ks@3,AESInvRound(ks@4,
-          AESInvRound(ks@5,AESInvRound(ks@6,AESInvRound(ks@7,AESInvRound(ks@8,state0)))))))))
+          AESInvRound(ks@5,AESInvRound(ks@6,AESInvRound(ks@7,AESInvRound(ks@8,
+            AESInvRound(ks@9,AESInvRound(ks@10,AESInvRound(ks@11,AESInvRound(ks@12,state0)))))))))))))
   }}));
 
 print "Proving msgToState_stateToMsg(rme)...";
@@ -65,7 +67,7 @@ InvMixColumns_MixColumns <-
 print "Proving aesDecrypt_aesEncrypt(rewriting)...";
 dec_enc <-
   time (prove_print do {
-    unfolding ["aesEncrypt", "aesDecrypt"];
+    unfolding ["aesEncrypt", "aesEncryptWithKeySchedule", "aesDecrypt"];
     simplify (addsimps [encrypt_lemma,
                         decrypt_lemma]
               (cryptol_ss()));
@@ -112,7 +114,7 @@ MixColumns_InvMixColumns <-
 print "Proving aesEncrypt_aesDecrypt(rewriting)...";
 enc_dec <-
   time (prove_print do {
-    unfolding ["aesEncrypt", "aesDecrypt"];
+    unfolding ["aesEncrypt", "aesEncryptWithKeySchedule", "aesDecrypt"];
     simplify (addsimps [encrypt_lemma,
                         decrypt_lemma]
               (cryptol_ss()));

intTests/test_smt_array_load_concrete_size/Makefile

@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -emit-llvm -frecord-command-line -O1
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test_smt_array_load_concrete_size/Mix.cry

@@ -0,0 +1,8 @@
+module Mix where
+
+import Array
+
+type ByteArray = Array[64][8]
+
+mix : {l} (width l <= 64) => ByteArray -> [64] -> [l][8] -> ByteArray
+mix block n data = arrayCopy block n (arrayRangeUpdate (arrayConstant 0) 0 data) 0 `(l)

intTests/test_smt_array_load_concrete_size/test.c

@@ -0,0 +1,13 @@
+#include <stdint.h>
+#include <string.h>
+
+int mix(uint8_t block[128], uint32_t n, uint8_t *data, size_t len) {
+  size_t left = 128 - n;
+
+  if (len < left) {
+    memcpy(block + n, data, len);
+  } else {
+    memcpy(block + n, data, left);
+  }
+  return 1;
+}

intTests/test_smt_array_load_concrete_size/test.saw

@@ -0,0 +1,66 @@
+enable_experimental;
+
+import "Mix.cry";
+let arrayRangeEq = parse_core "arrayRangeEq 64 (Vec 8 Bool)";
+
+m <- llvm_load_module "test.bc";
+
+let i8 = llvm_int 8;
+let i32 = llvm_int 32;
+
+let alloc_init_readonly ty v = do {
+  p <- llvm_alloc_readonly ty;
+  llvm_points_to p v;
+  return p;
+};
+
+let ptr_to_fresh_readonly n ty = do {
+  x <- llvm_fresh_var n ty;
+  p <- alloc_init_readonly ty (llvm_term x);
+  return (x, p);
+};
+
+let mix_spec len res_block_len range_eq_len = do {
+  block <- llvm_fresh_cryptol_var "block" {| ByteArray |};
+  block_ptr <- llvm_symbolic_alloc false 1 {{ 128:[64] }};
+  llvm_points_to_array_prefix block_ptr block {{ 128:[64] }};
+
+  (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len i8);
+
+  n <- llvm_fresh_var "n" i32;
+  llvm_precond({{ n < 128 }});
+
+  llvm_execute_func [block_ptr, (llvm_term n), data_ptr, (llvm_term {{ `len : [64] }})];
+
+  let res = {{ mix block (0 # n) data }};
+  res_block <- llvm_fresh_cryptol_var "res_block" {| ByteArray |};
+  llvm_points_to_array_prefix block_ptr res_block {{ `res_block_len:[64] }};
+  llvm_postcond {{ arrayRangeEq res_block 0 res 0 `range_eq_len }};
+
+  llvm_return (llvm_term {{ 1 : [32]}});
+};
+
+llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 128 128)
+  (do {
+    w4_unint_z3 [];
+  });
+
+llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 0 0)
+  (do {
+    w4_unint_z3 [];
+  });
+
+fails (llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 129 0)
+  (do {
+    w4_unint_z3 [];
+  }));
+

intTests/test_smt_array_load_concrete_size/test.sh

@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+
+set -e
+
+$SAW test.saw
+

saw-remote-api/src/SAWServer.hs

@@ -270,6 +270,8 @@ initialState readFileFn =
                 , rwProofs = []
                 , rwPreservedRegs = []
                 , rwAllocSymInitCheck = True
+                , rwWhat4PushMuxOps = False
+                , rwNoSatisfyingWriteFreshConstant = True
                 , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout
                 , rwPathSatSolver = CC.PathSat_Z3
                 , rwSkipSafetyProofs = False

src/SAWScript/Builtins.hs

@@ -717,7 +717,8 @@ goal_eval unints =
   execTactic $ tacticChange $ \goal ->
   do sc <- getSharedContext
      unintSet <- resolveNames unints
-     sqt' <- traverseSequentWithFocus (io . evalProp sc unintSet) (goalSequent goal)
+     what4PushMuxOps <- gets rwWhat4PushMuxOps
+     sqt' <- traverseSequentWithFocus (io . evalProp sc what4PushMuxOps unintSet) (goalSequent goal)
      return (sqt', EvalEvidence unintSet)
 
 extract_uninterp ::
@@ -2097,7 +2098,8 @@ specialize_theorem thm ts =
   do sc <- getSharedContext
      db <- SV.getTheoremDB
      pos <- SV.getPosition
-     (thm', db') <- io (specializeTheorem sc db pos "specialize_theorem" thm (map ttTerm ts))
+     what4PushMuxOps <- gets rwWhat4PushMuxOps
+     (thm', db') <- io (specializeTheorem sc what4PushMuxOps db pos "specialize_theorem" thm (map ttTerm ts))
      SV.putTheoremDB db'
      SV.returnProof thm'
 

src/SAWScript/Crucible/Common.hs

@@ -38,12 +38,14 @@ import           Lang.Crucible.Backend
 import           Lang.Crucible.Backend.Online (OnlineBackend, newOnlineBackend)
 import qualified Data.Parameterized.Nonce as Nonce
 import           What4.Protocol.Online (OnlineSolver(..))
+import qualified What4.Solver.CVC5 as CVC5
 import qualified What4.Solver.Z3 as Z3
 import qualified What4.Solver.Yices as Yices
 import qualified What4.Protocol.SMTLib2 as SMT2
 
 import qualified What4.Config as W4
 import qualified What4.Expr as W4
+import qualified What4.Expr.Builder as W4
 import qualified What4.Interface as W4
 import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
@@ -67,18 +69,21 @@ type Sym = W4.ExprBuilder Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.F
 type Backend solver = OnlineBackend solver Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.FloatReal)
 
 data SomeOnlineBackend =
-  forall solver. OnlineSolver solver => 
+  forall solver. OnlineSolver solver =>
     SomeOnlineBackend (Backend solver)
 
 data SAWCruciblePersonality sym = SAWCruciblePersonality
 
 sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator)
 sawCoreState sym = pure (sym ^. W4.userState)
 
-newSAWCoreExprBuilder :: SC.SharedContext -> IO Sym
-newSAWCoreExprBuilder sc =
+newSAWCoreExprBuilder :: SC.SharedContext -> Bool -> IO Sym
+newSAWCoreExprBuilder sc what4PushMuxOps =
   do st <- newSAWCoreState sc
-     W4.newExprBuilder W4.FloatRealRepr st Nonce.globalNonceGenerator
+     sym <- W4.newExprBuilder W4.FloatRealRepr st Nonce.globalNonceGenerator
+     pushMuxOpsSetting <- W4.getOptionSetting W4.pushMuxOpsOption $ W4.getConfiguration sym
+     _ <- W4.setOpt pushMuxOpsSetting what4PushMuxOps
+     pure sym
 
 defaultSAWCoreBackendTimeout :: Integer
 defaultSAWCoreBackendTimeout = 10000
@@ -89,14 +94,18 @@ newSAWCoreBackend pss sym = newSAWCoreBackendWithTimeout pss sym 0
 newSAWCoreBackendWithTimeout :: PathSatSolver -> Sym -> Integer -> IO SomeOnlineBackend
 newSAWCoreBackendWithTimeout PathSat_Yices sym timeout =
   do bak <- newOnlineBackend sym Yices.yicesDefaultFeatures
+     W4.extendConfig Z3.z3Options (W4.getConfiguration sym)
      W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
+     W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym)
      yicesTimeoutSetting <- W4.getOptionSetting Yices.yicesGoalTimeout (W4.getConfiguration sym)
      _ <- W4.setOpt yicesTimeoutSetting timeout
      return (SomeOnlineBackend (bak :: Backend Yices.Connection))
 
 newSAWCoreBackendWithTimeout PathSat_Z3 sym timeout =
   do bak <- newOnlineBackend sym (SMT2.defaultFeatures Z3.Z3)
      W4.extendConfig Z3.z3Options (W4.getConfiguration sym)
+     W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
+     W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym)
      z3TimeoutSetting <- W4.getOptionSetting Z3.z3Timeout (W4.getConfiguration sym)
      _ <- W4.setOpt z3TimeoutSetting timeout
      return (SomeOnlineBackend (bak :: Backend (SMT2.Writer Z3.Z3)))

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -841,7 +841,7 @@ setupCrucibleContext jclass =
      cb <- getJavaCodebase
      sc <- getSharedContext
      pathSatSolver <- gets rwPathSatSolver
-     sym <- io $ newSAWCoreExprBuilder sc
+     sym <- io $ newSAWCoreExprBuilder sc False
      bak <- io $ newSAWCoreBackend pathSatSolver sym
      opts <- getOptions
      io $ CJ.setSimulatorVerbosity (simVerbose opts) sym

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -159,7 +159,7 @@ jvm_extract c mname = do
   ctx <- getJVMTrans
 
   io $ do -- only the IO monad, nothing else
-          sym <- newSAWCoreExprBuilder sc
+          sym <- newSAWCoreExprBuilder sc False
           SomeOnlineBackend bak <- newSAWCoreBackend pathSatSolver sym
           st  <- sawCoreState sym
           CJ.setSimulatorVerbosity verbosity sym