Quick fix for saw

aws · Aug 26, 2022 · e53ffe4 · e53ffe4
1 parent f624826
commit e53ffe4
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/tests/saw/spec/handshake/handshake_io_lowlevel.saw b/tests/saw/spec/handshake/handshake_io_lowlevel.saw
@@ -48,9 +48,10 @@ print "Loaded bitcode via Crucible";
 //conn->mode
 let conn_mode pconn = crucible_field pconn "mode";
 
+let secure_crypto_params pconn = crucible_field pconn "secure";
+
 //conn->secure->cipher_suite->key_exchange_alg->flags
-let conn_secure_cipher_suite pconn =
-    (crucible_field (crucible_field pconn "secure") "cipher_suite");
+let conn_secure_cipher_suite crypto_params = crucible_field crypto_params "cipher_suite";
 
 //let key_exchange_algorithm csuite = crucible_elem csuite 3;
 let key_exchange_algorithm csuite = crucible_field csuite "key_exchange_alg";
@@ -151,8 +152,11 @@ let setup_connection_common chosen_psk_null = do {
    cca <- crucible_fresh_var "cca" (llvm_int 32);
    crucible_points_to (cca_type pconn) (crucible_term cca);
 
+   secure <- crucible_alloc (llvm_struct "struct.s2n_crypto_parameters");
+   crucible_points_to (secure_crypto_params pconn) secure;
+
    cipher_suite <- crucible_alloc (llvm_struct "struct.s2n_cipher_suite");
-   crucible_points_to (conn_secure_cipher_suite pconn)  cipher_suite;
+   crucible_points_to (conn_secure_cipher_suite secure) cipher_suite;
 
    kea <- crucible_alloc (llvm_struct "struct.s2n_kex");
    crucible_points_to (key_exchange_algorithm cipher_suite) kea;

diff --git a/tls/s2n_handshake_io.c b/tls/s2n_handshake_io.c
@@ -811,9 +811,6 @@ static S2N_RESULT s2n_validate_ems_status(struct s2n_connection *conn)
 
 int s2n_conn_set_handshake_type(struct s2n_connection *conn)
 {
-    POSIX_ENSURE_REF(conn);
-    POSIX_ENSURE_REF(conn->secure);
-
     if (IS_TLS13_HANDSHAKE(conn)) {
         POSIX_GUARD_RESULT(s2n_conn_set_tls13_handshake_type(conn));
         return S2N_SUCCESS;