Fix saw

tests/saw/spec/handshake/handshake_io_lowlevel.saw

@@ -68,6 +68,9 @@ let conn_config pconn = crucible_field pconn "config";
 //conn->config -> client_cert_auth_type
 let config_cca_type config = (crucible_field config "client_cert_auth_type");
 
+//conn->config->client_cert_auth_type_overridden
+let config_cca_type_ov config = (crucible_field config "client_cert_auth_type_overridden");
+
 //conn->handshake_params.our_chain_and_key->ocsp_status.size
 let ocsp_status_size cert_and_key =
     crucible_field (crucible_field (cert_and_key) "ocsp_status") "size";
@@ -154,12 +157,6 @@ let setup_connection_common chosen_psk_null = do {
    cork_val <- crucible_fresh_var "corked" (llvm_int 2);
    crucible_ghost_value corked cork_val;
 
-   cca_ov <- crucible_fresh_var "cca_ov" (llvm_int 8);
-   crucible_points_to (cca_type_ov pconn) (crucible_term cca_ov);
-
-   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;
 
@@ -175,9 +172,6 @@ let setup_connection_common chosen_psk_null = do {
    config <- crucible_alloc (llvm_struct "struct.s2n_config");
    crucible_points_to (conn_config pconn) config;
 
-   config_cca <- crucible_fresh_var "config_cca" (llvm_int 32);
-   crucible_points_to (config_cca_type config) (crucible_term config_cca);
-
    cak <- crucible_alloc (llvm_struct "struct.s2n_cert_chain_and_key");
    crucible_points_to (conn_chain_and_key pconn) cak;
 
@@ -226,7 +220,7 @@ let setup_connection_common chosen_psk_null = do {
 
    no_client_cert <- crucible_fresh_var "no_client_cert" (llvm_int 8);
 
-   let client_cert_auth_type = {{ if cca_ov != 0 then cca else config_cca }};
+   let client_cert_auth_type = s2n_connection_get_client_auth_type pconn config;
 
    npn_negotiated <- llvm_fresh_var "npn_negotiated" (llvm_int 1);
    llvm_points_to_bitfield pconn "npn_negotiated" (llvm_term npn_negotiated);
@@ -293,29 +287,39 @@ let s2n_allowed_to_cache_connection_spec = do {
 };
 
 
-let s2n_connection_get_client_auth_type_spec = do{
+let s2n_connection_get_client_auth_type pconn config = do {
+    conn_cca_ov <- llvm_fresh_var "conn_cca_ov" (llvm_int 1);
+    llvm_points_to_bitfield pconn "client_cert_auth_type_overridden" (llvm_term conn_cca_ov);
 
-    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");
-    auth_type <- crucible_alloc (llvm_int 32);
+    conn_cca <- crucible_fresh_var "conn_cca" (llvm_int 32);
+    crucible_points_to (cca_type pconn) (crucible_term conn_cca);
 
-    cca_ov <- crucible_fresh_var "cca_ov" (llvm_int 8);
-    crucible_points_to (cca_type_ov pconn) (crucible_term cca_ov);
-
-    config <- crucible_alloc_readonly (llvm_struct "struct.s2n_config");
-    crucible_points_to (conn_config pconn) config;
+    config_cca_ov <- llvm_fresh_var "config_cca_ov" (llvm_int 1);
+    llvm_points_to_bitfield pconn "client_cert_auth_type_overridden" (llvm_term config_cca_ov);
 
     config_cca <- crucible_fresh_var "config_cca" (llvm_int 32);
     crucible_points_to (config_cca_type config) (crucible_term config_cca);
+
+    let default_cca = {{ if mode == S2N_CLIENT then S2N_CERT_AUTH_OPTIONAL else S2N_CERT_AUTH_NONE }};
+    let expected_cca = {{ if cca_ov != 0 then cca
+                          else if config_cca_ov != 0 then config_cca
+                          else default_cca }};
+    return expected_cca;
+}
+
+let s2n_connection_get_client_auth_type_spec = do {
+    pconn <- crucible_alloc_readonly (llvm_struct "struct.s2n_connection");
+    auth_type <- crucible_alloc (llvm_int 32);
 
-    cca <- crucible_fresh_var "cca" (llvm_int 32);
-    crucible_points_to (cca_type pconn) (crucible_term cca);
+    config <- crucible_alloc_readonly (llvm_struct "struct.s2n_config");
+    crucible_points_to (conn_config pconn) config;
 
     crucible_execute_func [pconn, auth_type];
 
-    crucible_points_to (auth_type) (crucible_term {{if cca_ov != zero then cca else config_cca}});
+    let expected_cca = s2n_connection_get_client_auth_type pconn config;
+    crucible_points_to (auth_type) (crucible_term expected_cca);
 
     crucible_return (crucible_term {{ 0 : [32] }});
-
 };
 
 // Specification for s2n_conn_set_handshake_type that sets up simulation of it

tls/s2n_config.c

@@ -403,8 +403,8 @@ int s2n_config_get_client_auth_type(struct s2n_config *config, s2n_cert_auth_typ
 int s2n_config_set_client_auth_type(struct s2n_config *config, s2n_cert_auth_type client_auth_type)
 {
     POSIX_ENSURE_REF(config);
-    config->client_cert_auth_type = client_auth_type;
     config->client_cert_auth_type_overridden = true;
+    config->client_cert_auth_type = client_auth_type;
     return 0;
 }
 

tls/s2n_connection.c

@@ -777,7 +777,7 @@ int s2n_connection_get_client_auth_type(struct s2n_connection *conn,
 
 int s2n_connection_set_client_auth_type(struct s2n_connection *conn, s2n_cert_auth_type client_cert_auth_type)
 {
-    conn->client_cert_auth_type_overridden = 1;
+    conn->client_cert_auth_type_overridden = true;
     conn->client_cert_auth_type = client_cert_auth_type;
     return 0;
 }

tls/s2n_connection.h

@@ -133,6 +133,15 @@ struct s2n_connection {
     /* Indicates whether the connection should request OCSP stapling from the peer */
     unsigned request_ocsp_status : 1;
 
+    /* Whether to use client_cert_auth_type stored in s2n_config or in this s2n_connection.
+     *
+     * By default the s2n_connection will defer to s2n_config->client_cert_auth_type
+     * on whether or not to use Client Auth. But users can override Client Auth
+     * at the connection level using s2n_connection_set_client_auth_type() without
+     * mutating s2n_config since s2n_config can be shared between multiple s2n_connections.
+     */
+    unsigned client_cert_auth_type_overridden : 1;
+
     /* The configuration (cert, key .. etc ) */
     struct s2n_config *config;
 
@@ -224,15 +233,8 @@ struct s2n_connection {
     /* The PRF needs some storage elements to work with */
     struct s2n_prf_working_space *prf_space;
 
-    /* Whether to use client_cert_auth_type stored in s2n_config or in this s2n_connection.
-     *
-     * By default the s2n_connection will defer to s2n_config->client_cert_auth_type on whether or not to use Client Auth.
-     * But users can override Client Auth at the connection level using s2n_connection_set_client_auth_type() without mutating
-     * s2n_config since s2n_config can be shared between multiple s2n_connections. */
-    uint8_t client_cert_auth_type_overridden;
-
-    /* Whether or not the s2n_connection should require the Client to authenticate itself to the server. Only used if
-     * client_cert_auth_type_overridden is non-zero. */
+    /* Whether or not the s2n_connection should require the Client to authenticate itself to the server.
+     * Only used if client_cert_auth_type_overridden is true. */
     s2n_cert_auth_type client_cert_auth_type;
 
     /* Our workhorse stuffers, used for buffering the plaintext