Library POLAR_parse_client_hello_pp
Require Import ssreflect ssrbool.
Require Import machine_int.
Import MachineInt.
Require Import C_pp.
Require Import POLAR_parse_client_hello.
Require Import POLAR_library_functions_pp.
Goal typ_to_string PolarSSL.ssl_session "" = "struct ssl_session { int cipher; int length; char * id; }"%string.
Goal typ_to_string PolarSSL.ssl_context "" = "struct ssl_context { int state; int major_ver; int minor_ver; int max_major_ver; int max_minor_ver; struct ssl_session { int cipher; int length; char * id; } * session; char * in_hdr; char * in_msg; int in_left; int * ciphers; char * randbytes; }"%string.
Goal pp_cmd PolarSSL.ssl_parse_client_hello "" = "ret = ssl_fetch_input(ssl, 5); if ((_Bool)((ret) != (0))) { ; } else { buf = *(&(ssl->in_hdr)); _buf0_ = *(buf); if ((_Bool)(((_buf0_) & (-128)) != (0))) { ret = -38912; ; } else { if ((_Bool)((_buf0_) != (22))) { ret = -38912; ; } else { _buf1_ = *((buf) + (1)); if ((_Bool)((_buf1_) != (3))) { ret = -38912; ; } else { _buf3_ = *((buf) + (3)); _buf4_ = *((buf) + (4)); n = ((((int)_buf3_)) << (8)) | (((int)_buf4_)); if ((_Bool)((n) < (45))) { ret = -38912; ; } else { if ((_Bool)((n) > (512))) { ret = -38912; ; } else { ret = ssl_fetch_input(ssl, (5) + (n)); if ((_Bool)((ret) != (0))) { ; } else { buf = *(&(ssl->in_msg)); _n0_ = *(&(ssl->in_left)); n = (_n0_) - (5); md5_update(&(ssl->fin_md5), buf, n); sha1_update(&(ssl->fin_sha1), buf, n); _buf0_ = *(buf); if ((_Bool)((_buf0_) != (1))) { ret = -38912; ; } else { _buf4_ = *((buf) + (4)); if ((_Bool)((_buf4_) != (3))) { ret = -38912; ; } else { *(&(ssl->major_ver)) = 3; _buf5_ = *((buf) + (5)); *(&(ssl->minor_ver)) = ((_buf5_) <= (2)) ? (_buf5_) : (2); *(&(ssl->max_major_ver)) = _buf4_; *(&(ssl->max_minor_ver)) = _buf5_; _it_ = memcpy(&(ssl->randbytes), (buf) + (6), 32); _buf1_ = *((buf) + (1)); if ((_Bool)((_buf1_) != (0))) { ret = -38912; ; } else { _buf2_ = *((buf) + (2)); _buf3_ = *((buf) + (3)); if ((_Bool)((n) != ((4) + (((((int)_buf2_)) << (8)) | (((int)_buf3_)))))) { ret = -38912; ; } else { sess_len = *((buf) + (38)); if ((_Bool)(((sess_len) < (0)) || ((sess_len) > (32)))) { ret = -38912; ; } else { _ssl_session_0_ = *(&(ssl->session)); *(&(_ssl_session_0_->length)) = sess_len; _it_ = memset(&(_ssl_session_0_->id), 0, 32); _ssl_session_0_length_ = *(&(_ssl_session_0_->length)); _it_ = memcpy(&(_ssl_session_0_->id), (buf) + (39), _ssl_session_0_length_); _buf39_plus_sess_len_ = *((buf) + ((39) + (sess_len))); _buf40_plus_sess_len_ = *((buf) + ((40) + (sess_len))); ciph_len = ((((int)_buf39_plus_sess_len_)) << (8)) | (((int)_buf40_plus_sess_len_)); if ((_Bool)((((ciph_len) < (2)) || ((ciph_len) > (256))) || (((ciph_len) % (1 << 1)) != (0)))) { ret = -38912; ; } else { comp_len = *((buf) + (((41) + (sess_len)) + (ciph_len))); if ((_Bool)(((comp_len) < (1)) || ((comp_len) > (16)))) { ret = -38912; ; } else { _goto_have_cipher_ = 0; i = 0; _ssl_ciphers_ = *(&(ssl->ciphers)); _ssl_ciphers_i_ = *((_ssl_ciphers_) + (i)); while ((_Bool)(((_goto_have_cipher_) == (0)) && ((_ssl_ciphers_i_) != (0)))) { j = 0; p = ((buf) + (41)) + (sess_len); while ((_Bool)(((_goto_have_cipher_) == (0)) && ((j) < (ciph_len)))) { _p0_ = *(p); if ((_Bool)((_p0_) == (0))) { _p1_ = *((p) + (1)); _ssl_ciphers_ = *(&(ssl->ciphers)); _ssl_ciphers_i_ = *((_ssl_ciphers_) + (i)); if ((_Bool)((_p1_) == (_ssl_ciphers_i_))) { _goto_have_cipher_ = 1; } else { j = (j) + (2); p = (p) + (2); } } else { j = (j) + (2); p = (p) + (2); } } i = (i) + (1); _ssl_ciphers_ = *(&(ssl->ciphers)); _ssl_ciphers_i_ = *((_ssl_ciphers_) + (i)); } if ((_Bool)((_goto_have_cipher_) != (0))) { *(&(_ssl_session_0_->cipher)) = _ssl_ciphers_i_; *(&(ssl->in_left)) = 0; _ssl_state_ = *(&(ssl->state)); *(&(ssl->state)) = (_ssl_state_) + (1); ret = 0; ; } else { ret = -16384; ; } } } } } } } } } } } } } } }"%string.
Require Import machine_int.
Import MachineInt.
Require Import C_pp.
Require Import POLAR_parse_client_hello.
Require Import POLAR_library_functions_pp.
Goal typ_to_string PolarSSL.ssl_session "" = "struct ssl_session { int cipher; int length; char * id; }"%string.
Goal typ_to_string PolarSSL.ssl_context "" = "struct ssl_context { int state; int major_ver; int minor_ver; int max_major_ver; int max_minor_ver; struct ssl_session { int cipher; int length; char * id; } * session; char * in_hdr; char * in_msg; int in_left; int * ciphers; char * randbytes; }"%string.
Goal pp_cmd PolarSSL.ssl_parse_client_hello "" = "ret = ssl_fetch_input(ssl, 5); if ((_Bool)((ret) != (0))) { ; } else { buf = *(&(ssl->in_hdr)); _buf0_ = *(buf); if ((_Bool)(((_buf0_) & (-128)) != (0))) { ret = -38912; ; } else { if ((_Bool)((_buf0_) != (22))) { ret = -38912; ; } else { _buf1_ = *((buf) + (1)); if ((_Bool)((_buf1_) != (3))) { ret = -38912; ; } else { _buf3_ = *((buf) + (3)); _buf4_ = *((buf) + (4)); n = ((((int)_buf3_)) << (8)) | (((int)_buf4_)); if ((_Bool)((n) < (45))) { ret = -38912; ; } else { if ((_Bool)((n) > (512))) { ret = -38912; ; } else { ret = ssl_fetch_input(ssl, (5) + (n)); if ((_Bool)((ret) != (0))) { ; } else { buf = *(&(ssl->in_msg)); _n0_ = *(&(ssl->in_left)); n = (_n0_) - (5); md5_update(&(ssl->fin_md5), buf, n); sha1_update(&(ssl->fin_sha1), buf, n); _buf0_ = *(buf); if ((_Bool)((_buf0_) != (1))) { ret = -38912; ; } else { _buf4_ = *((buf) + (4)); if ((_Bool)((_buf4_) != (3))) { ret = -38912; ; } else { *(&(ssl->major_ver)) = 3; _buf5_ = *((buf) + (5)); *(&(ssl->minor_ver)) = ((_buf5_) <= (2)) ? (_buf5_) : (2); *(&(ssl->max_major_ver)) = _buf4_; *(&(ssl->max_minor_ver)) = _buf5_; _it_ = memcpy(&(ssl->randbytes), (buf) + (6), 32); _buf1_ = *((buf) + (1)); if ((_Bool)((_buf1_) != (0))) { ret = -38912; ; } else { _buf2_ = *((buf) + (2)); _buf3_ = *((buf) + (3)); if ((_Bool)((n) != ((4) + (((((int)_buf2_)) << (8)) | (((int)_buf3_)))))) { ret = -38912; ; } else { sess_len = *((buf) + (38)); if ((_Bool)(((sess_len) < (0)) || ((sess_len) > (32)))) { ret = -38912; ; } else { _ssl_session_0_ = *(&(ssl->session)); *(&(_ssl_session_0_->length)) = sess_len; _it_ = memset(&(_ssl_session_0_->id), 0, 32); _ssl_session_0_length_ = *(&(_ssl_session_0_->length)); _it_ = memcpy(&(_ssl_session_0_->id), (buf) + (39), _ssl_session_0_length_); _buf39_plus_sess_len_ = *((buf) + ((39) + (sess_len))); _buf40_plus_sess_len_ = *((buf) + ((40) + (sess_len))); ciph_len = ((((int)_buf39_plus_sess_len_)) << (8)) | (((int)_buf40_plus_sess_len_)); if ((_Bool)((((ciph_len) < (2)) || ((ciph_len) > (256))) || (((ciph_len) % (1 << 1)) != (0)))) { ret = -38912; ; } else { comp_len = *((buf) + (((41) + (sess_len)) + (ciph_len))); if ((_Bool)(((comp_len) < (1)) || ((comp_len) > (16)))) { ret = -38912; ; } else { _goto_have_cipher_ = 0; i = 0; _ssl_ciphers_ = *(&(ssl->ciphers)); _ssl_ciphers_i_ = *((_ssl_ciphers_) + (i)); while ((_Bool)(((_goto_have_cipher_) == (0)) && ((_ssl_ciphers_i_) != (0)))) { j = 0; p = ((buf) + (41)) + (sess_len); while ((_Bool)(((_goto_have_cipher_) == (0)) && ((j) < (ciph_len)))) { _p0_ = *(p); if ((_Bool)((_p0_) == (0))) { _p1_ = *((p) + (1)); _ssl_ciphers_ = *(&(ssl->ciphers)); _ssl_ciphers_i_ = *((_ssl_ciphers_) + (i)); if ((_Bool)((_p1_) == (_ssl_ciphers_i_))) { _goto_have_cipher_ = 1; } else { j = (j) + (2); p = (p) + (2); } } else { j = (j) + (2); p = (p) + (2); } } i = (i) + (1); _ssl_ciphers_ = *(&(ssl->ciphers)); _ssl_ciphers_i_ = *((_ssl_ciphers_) + (i)); } if ((_Bool)((_goto_have_cipher_) != (0))) { *(&(_ssl_session_0_->cipher)) = _ssl_ciphers_i_; *(&(ssl->in_left)) = 0; _ssl_state_ = *(&(ssl->state)); *(&(ssl->state)) = (_ssl_state_) + (1); ret = 0; ; } else { ret = -16384; ; } } } } } } } } } } } } } } }"%string.