Adapt the low-level correspondence SAW proof script to the new
LLVM-Crucible interface
import "spec/s2n_advance_message.cry";
-load_crucible_llvm_module "bitcode/all_llvm.bc";
+llvm <- llvm_load_module "bitcode/all_llvm.bc";
+//load_llvm_cfg llvm "s2n_advance_message";
+//load_llvm_cfg llvm "s2n_conn_set_handshake_type";
print "Loaded bitcode via Crucible";
////////////////////////////////////////////////////////////////
@@ -264,17 +266,17 @@ let s2n_connection_is_managed_corked_spec = do {
};
-let s2n_advance_message_proof = do {
+let s2n_handshake_io_lowlevel = do {
// Dependencies specifications/overrides
- s2n_socket_write_uncork <- crucible_llvm_unsafe_assume_spec "s2n_socket_write_uncork" s2n_socket_write_uncork_spec;
- s2n_socket_write_cork <- crucible_llvm_unsafe_assume_spec "s2n_socket_write_cork" s2n_socket_write_cork_spec;
- s2n_socket_was_corked <- crucible_llvm_unsafe_assume_spec "s2n_socket_was_corked" s2n_socket_was_corked_spec;
- s2n_connection_is_managed_corked <- crucible_llvm_unsafe_assume_spec "s2n_connection_is_managed_corked" s2n_connection_is_managed_corked_spec;
- s2n_is_caching_enabled <- crucible_llvm_unsafe_assume_spec "s2n_is_caching_enabled" s2n_is_caching_enabled_spec;
+ s2n_socket_write_uncork <- crucible_llvm_unsafe_assume_spec llvm "s2n_socket_write_uncork" s2n_socket_write_uncork_spec;
+ s2n_socket_write_cork <- crucible_llvm_unsafe_assume_spec llvm "s2n_socket_write_cork" s2n_socket_write_cork_spec;
+ s2n_socket_was_corked <- crucible_llvm_unsafe_assume_spec llvm "s2n_socket_was_corked" s2n_socket_was_corked_spec;
+ s2n_connection_is_managed_corked <- crucible_llvm_unsafe_assume_spec llvm "s2n_connection_is_managed_corked" s2n_connection_is_managed_corked_spec;
+ s2n_is_caching_enabled <- crucible_llvm_unsafe_assume_spec llvm "s2n_is_caching_enabled" s2n_is_caching_enabled_spec;
let dependencies = [s2n_socket_write_uncork, s2n_socket_write_cork, s2n_socket_was_corked, s2n_connection_is_managed_corked];
- s2n_advance_message_proof <- crucible_llvm_verify "s2n_advance_message" dependencies true s2n_advance_message_spec yices;
- s2n_conn_set_handshake_type_proof <- crucible_llvm_verify "s2n_conn_set_handshake_type" [s2n_is_caching_enabled] true s2n_conn_set_handshake_type_spec yices;
+ s2n_advance_message_proof <- crucible_llvm_verify llvm "s2n_advance_message" dependencies true s2n_advance_message_spec yices;
+ s2n_conn_set_handshake_type_proof <- crucible_llvm_verify llvm "s2n_conn_set_handshake_type" [s2n_is_caching_enabled] true s2n_conn_set_handshake_type_spec yices;
print "done";
return ();
};
