From cc6f3c1bc59608a80bdaf107b02d28e69e155527 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 18 May 2021 10:37:58 -0700 Subject: [PATCH 01/17] add vim-saw --- vim-saw/ftdetect/saw.vim | 1 + vim-saw/ftplugin/saw.vim | 7 +++++++ vim-saw/ftplugin/saw/repl.vim | 34 ++++++++++++++++++++++++++++++++++ vim-saw/syntax/saw.vim | 7 +++++++ 4 files changed, 49 insertions(+) create mode 100644 vim-saw/ftdetect/saw.vim create mode 100644 vim-saw/ftplugin/saw.vim create mode 100644 vim-saw/ftplugin/saw/repl.vim create mode 100644 vim-saw/syntax/saw.vim diff --git a/vim-saw/ftdetect/saw.vim b/vim-saw/ftdetect/saw.vim new file mode 100644 index 0000000000..121b01ba77 --- /dev/null +++ b/vim-saw/ftdetect/saw.vim @@ -0,0 +1 @@ +autocmd BufNewFile,BufRead *.saw set filetype=saw diff --git a/vim-saw/ftplugin/saw.vim b/vim-saw/ftplugin/saw.vim new file mode 100644 index 0000000000..10001f697c --- /dev/null +++ b/vim-saw/ftplugin/saw.vim @@ -0,0 +1,7 @@ +" mappings to copy top-level statements that can then be pasted in a SAW REPL +" running in a vim terminal window +nnoremap vip:call Join_and_copy(visualmode()) +nnoremap vip:call Copy(visualmode()) + +" a mapping to paste in terminal mode: +tnoremap "" diff --git a/vim-saw/ftplugin/saw/repl.vim b/vim-saw/ftplugin/saw/repl.vim new file mode 100644 index 0000000000..22d7476963 --- /dev/null +++ b/vim-saw/ftplugin/saw/repl.vim @@ -0,0 +1,34 @@ +function Join_and_copy(type) + if a:type ==# 'V' " only do stuff in line-wise visual mode + normal! `y + split __scratch__ + setlocal buftype=nofile + setlocal bufhidden=delete + normal! p + normal! Gdd + %s/^\s*\/\/.*\n//eg " delete blank lines + %s/\/\/.*\n/\r/eg " remove end-of-line comments + " join lines and yank: + normal! ggVGJyy + q " close scratch split + endif +endfunction + +function Copy(type) + if a:type ==# 'V' " only do stuff in line-wise visual mode + normal! `y + split __scratch__ + setlocal buftype=nofile + setlocal bufhidden=delete + normal! p + normal! Gdd + %s/^\s*\/\/.*\n//eg " delete blank lines + %s/\/\/.*\n/\r/eg " remove end-of-line comments + %s/\n/\\\r/g " add backslash at end of lines + " remove backslash at end of last line: + normal! G$x + " yank: + normal! ggVGy + q " close scratch split + endif +endfunction diff --git a/vim-saw/syntax/saw.vim b/vim-saw/syntax/saw.vim new file mode 100644 index 0000000000..4e77e6cc9a --- /dev/null +++ b/vim-saw/syntax/saw.vim @@ -0,0 +1,7 @@ +syn keyword SAWKeyword do let include import +hi link SAWKeyword Keyword +setlocal commentstring=//%s " is this useless? the doc says only used for folding +setlocal comments=s1:/*,mb:*,ex:*/,://" +syntax match SAWComment "\v//.*$" contains=@Spell +highlight link SAWComment Comment +setlocal formatoptions=tcqr From db113ed46bf549a80b64f832b4bc79d964c7c4bf Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 18 May 2021 10:47:55 -0700 Subject: [PATCH 02/17] add /**/ comments to syntax --- vim-saw/syntax/saw.vim | 1 + 1 file changed, 1 insertion(+) diff --git a/vim-saw/syntax/saw.vim b/vim-saw/syntax/saw.vim index 4e77e6cc9a..5ef6b6f604 100644 --- a/vim-saw/syntax/saw.vim +++ b/vim-saw/syntax/saw.vim @@ -3,5 +3,6 @@ hi link SAWKeyword Keyword setlocal commentstring=//%s " is this useless? the doc says only used for folding setlocal comments=s1:/*,mb:*,ex:*/,://" syntax match SAWComment "\v//.*$" contains=@Spell +syntax region SAWComment start="/\*" end="\*/" contains=@Spell highlight link SAWComment Comment setlocal formatoptions=tcqr From 2893a8d30d03a7c37e557756760f4e0aa8b9b901 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 18 May 2021 11:18:09 -0700 Subject: [PATCH 03/17] some improvements --- vim-saw/ftplugin/saw.vim | 7 ++++--- vim-saw/ftplugin/saw/repl.vim | 20 +++++++++++++------- 2 files changed, 17 insertions(+), 10 deletions(-) diff --git a/vim-saw/ftplugin/saw.vim b/vim-saw/ftplugin/saw.vim index 10001f697c..3f96549d0c 100644 --- a/vim-saw/ftplugin/saw.vim +++ b/vim-saw/ftplugin/saw.vim @@ -1,7 +1,8 @@ " mappings to copy top-level statements that can then be pasted in a SAW REPL " running in a vim terminal window -nnoremap vip:call Join_and_copy(visualmode()) -nnoremap vip:call Copy(visualmode()) - +nnoremap vip:call Join_and_copy(visualmode()) +nnoremap vip:call Copy(visualmode()) +vnoremap :call Join_and_copy(visualmode()) +vnoremap :call Copy(visualmode()) " a mapping to paste in terminal mode: tnoremap "" diff --git a/vim-saw/ftplugin/saw/repl.vim b/vim-saw/ftplugin/saw/repl.vim index 22d7476963..86010ed8c3 100644 --- a/vim-saw/ftplugin/saw/repl.vim +++ b/vim-saw/ftplugin/saw/repl.vim @@ -5,15 +5,21 @@ function Join_and_copy(type) setlocal buftype=nofile setlocal bufhidden=delete normal! p - normal! Gdd - %s/^\s*\/\/.*\n//eg " delete blank lines - %s/\/\/.*\n/\r/eg " remove end-of-line comments + call DeleteBlank() " join lines and yank: normal! ggVGJyy q " close scratch split endif endfunction +function DeleteBlank() + %g/^\s*\n/d + %g/^\n/d + %g/^\s*\/\/.*\n/d + %s/\/\/.*\n/\r/eg " remove end-of-line comments +endfunction + + function Copy(type) if a:type ==# 'V' " only do stuff in line-wise visual mode normal! `y @@ -21,11 +27,11 @@ function Copy(type) setlocal buftype=nofile setlocal bufhidden=delete normal! p - normal! Gdd - %s/^\s*\/\/.*\n//eg " delete blank lines - %s/\/\/.*\n/\r/eg " remove end-of-line comments + call DeleteBlank() %s/\n/\\\r/g " add backslash at end of lines - " remove backslash at end of last line: + " remove last line (is blank) + normal! Gdd + " remove backslash at end of (new) last line: normal! G$x " yank: normal! ggVGy From 04528e95852fe569f8c0b3cb8f7debdd51a4339d Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 18 May 2021 11:24:21 -0700 Subject: [PATCH 04/17] use function! to be able to reload --- vim-saw/ftplugin/saw/repl.vim | 42 +++++++++++++++++------------------ 1 file changed, 20 insertions(+), 22 deletions(-) diff --git a/vim-saw/ftplugin/saw/repl.vim b/vim-saw/ftplugin/saw/repl.vim index 86010ed8c3..b56cac6be4 100644 --- a/vim-saw/ftplugin/saw/repl.vim +++ b/vim-saw/ftplugin/saw/repl.vim @@ -1,33 +1,31 @@ -function Join_and_copy(type) - if a:type ==# 'V' " only do stuff in line-wise visual mode - normal! `y - split __scratch__ - setlocal buftype=nofile - setlocal bufhidden=delete - normal! p - call DeleteBlank() - " join lines and yank: - normal! ggVGJyy - q " close scratch split - endif -endfunction - -function DeleteBlank() +function! DeleteBlank() %g/^\s*\n/d %g/^\n/d %g/^\s*\/\/.*\n/d %s/\/\/.*\n/\r/eg " remove end-of-line comments endfunction +function! CreateSplit() + normal! `y + split __scratch__ + setlocal buftype=nofile + setlocal bufhidden=delete + normal! p + call DeleteBlank() +endfunction + +function! Join_and_copy(type) + if a:type ==# 'V' " only do stuff in line-wise visual mode + call CreateSplit() + " join lines and yank: + normal! ggVGJyy + q " close scratch split + endif +endfunction -function Copy(type) +function! Copy(type) if a:type ==# 'V' " only do stuff in line-wise visual mode - normal! `y - split __scratch__ - setlocal buftype=nofile - setlocal bufhidden=delete - normal! p - call DeleteBlank() + call CreateSplit() %s/\n/\\\r/g " add backslash at end of lines " remove last line (is blank) normal! Gdd From 41b92bbb0889679c5c448c8fc91936e474fe87ce Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 18 May 2021 15:44:57 -0700 Subject: [PATCH 05/17] restore position --- vim-saw/ftplugin/saw.vim | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/vim-saw/ftplugin/saw.vim b/vim-saw/ftplugin/saw.vim index 3f96549d0c..e1594d7a1b 100644 --- a/vim-saw/ftplugin/saw.vim +++ b/vim-saw/ftplugin/saw.vim @@ -1,7 +1,7 @@ " mappings to copy top-level statements that can then be pasted in a SAW REPL " running in a vim terminal window -nnoremap vip:call Join_and_copy(visualmode()) -nnoremap vip:call Copy(visualmode()) +nnoremap m`vip:call Join_and_copy(visualmode())'` +nnoremap m`vip:call Copy(visualmode())'` vnoremap :call Join_and_copy(visualmode()) vnoremap :call Copy(visualmode()) " a mapping to paste in terminal mode: From b80ab670820a79d8020b378e228b4efc6ffbae1a Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 18 May 2021 15:45:06 -0700 Subject: [PATCH 06/17] add all saw builtins as keywords --- vim-saw/syntax/saw.vim | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/vim-saw/syntax/saw.vim b/vim-saw/syntax/saw.vim index 5ef6b6f604..98455932ec 100644 --- a/vim-saw/syntax/saw.vim +++ b/vim-saw/syntax/saw.vim @@ -1,4 +1,3 @@ -syn keyword SAWKeyword do let include import hi link SAWKeyword Keyword setlocal commentstring=//%s " is this useless? the doc says only used for folding setlocal comments=s1:/*,mb:*,ex:*/,://" @@ -6,3 +5,6 @@ syntax match SAWComment "\v//.*$" contains=@Spell syntax region SAWComment start="/\*" end="\*/" contains=@Spell highlight link SAWComment Comment setlocal formatoptions=tcqr + +" all SAW builtins included: +syn keyword SAWKeyword do let import abc get_opt offline_cnf abstract_symbolic goal_apply offline_cnf_external add_cryptol_defs goal_assume offline_coq add_cryptol_eqs goal_eval offline_extcore add_prelude_defs goal_eval_unint offline_smtlib2 add_prelude_eqs goal_insert offline_unint_smtlib2 add_x86_preserved_reg goal_intro offline_verilog addsimp goal_num_ite offline_w4_unint_cvc4 addsimp' goal_num_when offline_w4_unint_yices addsimps goal_when offline_w4_unint_z3 addsimps' head parse_core admit hoist_ifs parser_printer_roundtrip approxmc include print assume_unsat java_array print_goal assume_valid java_bool print_goal_consts auto_match java_byte print_goal_depth basic_ss java_char print_goal_size beta_reduce_goal java_class print_term beta_reduce_term java_double print_term_depth boolector java_float print_type caseProofResult java_int prove caseSatResult java_load_class prove_core check_convertible java_long prove_print check_goal java_short qc_print check_term jvm_alloc_array quickcheck codegen jvm_alloc_object read_aig concat jvm_array_is read_bytes core_axiom jvm_elem_is read_core core_thm jvm_execute_func replace crucible_alloc jvm_extract return crucible_alloc_aligned jvm_field_is rewrite crucible_alloc_global jvm_fresh_var rme crucible_alloc_readonly jvm_modifies_elem run crucible_alloc_readonly_aligned jvm_modifies_field sat crucible_alloc_with_size jvm_modifies_static_field sat_print crucible_array jvm_null sbv_abc crucible_conditional_points_to jvm_postcond sbv_boolector crucible_conditional_points_to_untyped jvm_precond sbv_cvc4 crucible_declare_ghost_state jvm_return sbv_mathsat crucible_elem jvm_static_field_is sbv_unint_cvc4 crucible_equal jvm_term sbv_unint_yices crucible_execute_func jvm_unsafe_assume_spec sbv_unint_z3 crucible_field jvm_verify sbv_yices crucible_fresh_cryptol_var lambda sbv_z3 crucible_fresh_expanded_val lambdas set_ascii crucible_fresh_pointer length set_base crucible_fresh_var list_term set_color crucible_ghost_value llvm_alias set_timeout crucible_global llvm_alloc set_x86_stack_base_align crucible_global_initializer llvm_alloc_aligned sharpSAT crucible_java_extract llvm_alloc_global show crucible_llvm_array_size_profile llvm_alloc_readonly show_cfg crucible_llvm_compositional_extract llvm_alloc_readonly_aligned show_term crucible_llvm_extract llvm_alloc_with_size simplify crucible_llvm_unsafe_assume_spec llvm_array skeleton_arg crucible_llvm_verify llvm_array_size_profile skeleton_arg_index crucible_llvm_verify_x86 llvm_array_value skeleton_arg_index_pointer crucible_null llvm_boilerplate skeleton_arg_pointer crucible_packed_struct llvm_cfg skeleton_exec crucible_points_to llvm_compositional_extract skeleton_globals_post crucible_points_to_array_prefix llvm_conditional_points_to skeleton_globals_pre crucible_points_to_untyped llvm_conditional_points_to_at_type skeleton_guess_arg_sizes crucible_postcond llvm_conditional_points_to_untyped skeleton_poststate crucible_precond llvm_declare_ghost_state skeleton_prestate crucible_return llvm_double skeleton_resize_arg crucible_spec_size llvm_elem skeleton_resize_arg_index crucible_spec_solvers llvm_equal split_goal crucible_struct llvm_execute_func str_concat crucible_symbolic_alloc llvm_extract summarize_verification crucible_term llvm_field tail cryptol_add_path llvm_float term_size cryptol_extract llvm_fresh_cryptol_var term_tree_size cryptol_load llvm_fresh_expanded_val test_mr_solver cryptol_prims llvm_fresh_pointer time cryptol_ss llvm_fresh_var trivial cvc4 llvm_ghost_value true default_x86_preserved_reg llvm_global type default_x86_stack_base_align llvm_global_initializer undefined define llvm_int unfold_term disable_crucible_assert_then_assume llvm_load_module unfolding disable_crucible_profiling llvm_null unint_cvc4 disable_smt_array_memory_model llvm_packed_struct_type unint_yices disable_what4_hash_consing llvm_packed_struct_value unint_z3 disable_x86_what4_hash_consing llvm_pointer w4 dsec_print llvm_points_to w4_abc_smtlib2 dump_file_AST llvm_points_to_array_prefix w4_abc_verilog empty_ss llvm_points_to_at_type w4_offline_smtlib2 enable_crucible_assert_then_assume llvm_points_to_untyped w4_unint_cvc4 enable_crucible_profiling llvm_postcond w4_unint_yices enable_deprecated llvm_precond w4_unint_z3 enable_experimental llvm_return with_time enable_lax_arithmetic llvm_sizeof write_aig enable_smt_array_memory_model llvm_spec_size write_aig_external enable_what4_hash_consing llvm_spec_solvers write_cnf enable_x86_what4_hash_consing llvm_struct write_cnf_external env llvm_struct_type write_coq_cryptol_module eval_bool llvm_struct_value write_coq_cryptol_primitives_for_sawcore eval_int llvm_symbolic_alloc write_coq_sawcore_prelude eval_list llvm_term write_coq_term eval_size llvm_type write_core exec llvm_unsafe_assume_spec write_saig exit llvm_verify write_saig' external_aig_solver llvm_verify_x86 write_smtlib2 external_cnf_solver mathsat write_smtlib2_w4 fails module_skeleton write_verilog false nth yices for null z3 fresh_symbolic offline_aig function_skeleton offline_aig_external From 93fb90a98459b5ad9782457c678f4afd1e842105 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Tue, 18 May 2021 16:17:04 -0700 Subject: [PATCH 07/17] preserve patterns history --- vim-saw/ftplugin/saw/repl.vim | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/vim-saw/ftplugin/saw/repl.vim b/vim-saw/ftplugin/saw/repl.vim index b56cac6be4..a006d3f30d 100644 --- a/vim-saw/ftplugin/saw/repl.vim +++ b/vim-saw/ftplugin/saw/repl.vim @@ -1,8 +1,8 @@ function! DeleteBlank() - %g/^\s*\n/d - %g/^\n/d - %g/^\s*\/\/.*\n/d - %s/\/\/.*\n/\r/eg " remove end-of-line comments + keepp %g/^\s*\n/d + keepp %g/^\n/d + keepp %g/^\s*\/\/.*\n/d + keepp %s/\/\/.*\n/\r/eg " remove end-of-line comments endfunction function! CreateSplit() From a2df07df6435cae0ace2d5374d8b3e791298c2e8 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Thu, 10 Jun 2021 16:09:37 -0700 Subject: [PATCH 08/17] switch to vim-slime --- vim-saw/doc/saw.txt | 10 +++++++++ vim-saw/doc/tags | 1 + vim-saw/ftplugin/saw.vim | 8 -------- vim-saw/ftplugin/saw/repl.vim | 38 ----------------------------------- vim-saw/plugin/saw.vim | 20 ++++++++++++++++++ 5 files changed, 31 insertions(+), 46 deletions(-) create mode 100644 vim-saw/doc/saw.txt create mode 100644 vim-saw/doc/tags delete mode 100644 vim-saw/ftplugin/saw.vim delete mode 100644 vim-saw/ftplugin/saw/repl.vim create mode 100644 vim-saw/plugin/saw.vim diff --git a/vim-saw/doc/saw.txt b/vim-saw/doc/saw.txt new file mode 100644 index 0000000000..965c4dd22c --- /dev/null +++ b/vim-saw/doc/saw.txt @@ -0,0 +1,10 @@ +*saw.txt* functionality for developing sawscript scripts + +This plugin adds basic syntax highlighting and a vim-slime override. This +allows using vim-slime to send sawscript snippets from a sawscript file to a +running sawscript interpreter. See the official vim-slime documentation for how +to use vim-slime. The most basic command is , which sends the whole +paragraph the cursor is in. Note that the saw interpreter will correct parse +single top-level statements, but not multpile top-level statements. + +Dependencies: vim-slime diff --git a/vim-saw/doc/tags b/vim-saw/doc/tags new file mode 100644 index 0000000000..2c8d1201a9 --- /dev/null +++ b/vim-saw/doc/tags @@ -0,0 +1 @@ +saw.txt saw.txt /*saw.txt* diff --git a/vim-saw/ftplugin/saw.vim b/vim-saw/ftplugin/saw.vim deleted file mode 100644 index e1594d7a1b..0000000000 --- a/vim-saw/ftplugin/saw.vim +++ /dev/null @@ -1,8 +0,0 @@ -" mappings to copy top-level statements that can then be pasted in a SAW REPL -" running in a vim terminal window -nnoremap m`vip:call Join_and_copy(visualmode())'` -nnoremap m`vip:call Copy(visualmode())'` -vnoremap :call Join_and_copy(visualmode()) -vnoremap :call Copy(visualmode()) -" a mapping to paste in terminal mode: -tnoremap "" diff --git a/vim-saw/ftplugin/saw/repl.vim b/vim-saw/ftplugin/saw/repl.vim deleted file mode 100644 index a006d3f30d..0000000000 --- a/vim-saw/ftplugin/saw/repl.vim +++ /dev/null @@ -1,38 +0,0 @@ -function! DeleteBlank() - keepp %g/^\s*\n/d - keepp %g/^\n/d - keepp %g/^\s*\/\/.*\n/d - keepp %s/\/\/.*\n/\r/eg " remove end-of-line comments -endfunction - -function! CreateSplit() - normal! `y - split __scratch__ - setlocal buftype=nofile - setlocal bufhidden=delete - normal! p - call DeleteBlank() -endfunction - -function! Join_and_copy(type) - if a:type ==# 'V' " only do stuff in line-wise visual mode - call CreateSplit() - " join lines and yank: - normal! ggVGJyy - q " close scratch split - endif -endfunction - -function! Copy(type) - if a:type ==# 'V' " only do stuff in line-wise visual mode - call CreateSplit() - %s/\n/\\\r/g " add backslash at end of lines - " remove last line (is blank) - normal! Gdd - " remove backslash at end of (new) last line: - normal! G$x - " yank: - normal! ggVGy - q " close scratch split - endif -endfunction diff --git a/vim-saw/plugin/saw.vim b/vim-saw/plugin/saw.vim new file mode 100644 index 0000000000..718a6f4231 --- /dev/null +++ b/vim-saw/plugin/saw.vim @@ -0,0 +1,20 @@ +" a function that overrides vim-slime's default behavior: +function SlimeOverride_EscapeText_saw(text) + " create temp buffer + split __saw_slime_temp_buffer__ + setlocal buftype=nofile + " paste text in buffer + set paste + exe "normal! i" . a:text . "\" + set nopaste + " remove blank things + silent! keepp g/^\s*\n/d + silent! keepp g/^\n/d + silent! keepp g/^\s*\/\/.*\n/d + silent! keepp %s/\(\/\/.*\)$//eg " remove end-of-line comments + " copy buffer contents into res, adding a backslash at the end of each line + let res = join(getline(1, '$'), "\\\n") + " q " close scratch split + bdelete __saw_slime_temp_buffer__ " delete temp buffer (the following didn't work reliably: setlocal bufhidden=delete) + return res . "\n" +endfunction From 0731994a44a4d2864a3f2f51e44ea42889898c60 Mon Sep 17 00:00:00 2001 From: Giuliano Losa Date: Thu, 10 Jun 2021 17:15:16 -0700 Subject: [PATCH 09/17] remove tags, fix typo, other minor stuff --- vim-saw/doc/saw.txt | 2 +- vim-saw/doc/tags | 1 - vim-saw/plugin/saw.vim | 8 +++----- 3 files changed, 4 insertions(+), 7 deletions(-) delete mode 100644 vim-saw/doc/tags diff --git a/vim-saw/doc/saw.txt b/vim-saw/doc/saw.txt index 965c4dd22c..820f6291e5 100644 --- a/vim-saw/doc/saw.txt +++ b/vim-saw/doc/saw.txt @@ -4,7 +4,7 @@ This plugin adds basic syntax highlighting and a vim-slime override. This allows using vim-slime to send sawscript snippets from a sawscript file to a running sawscript interpreter. See the official vim-slime documentation for how to use vim-slime. The most basic command is , which sends the whole -paragraph the cursor is in. Note that the saw interpreter will correct parse +paragraph the cursor is in. Note that the saw interpreter will correctly parse single top-level statements, but not multpile top-level statements. Dependencies: vim-slime diff --git a/vim-saw/doc/tags b/vim-saw/doc/tags deleted file mode 100644 index 2c8d1201a9..0000000000 --- a/vim-saw/doc/tags +++ /dev/null @@ -1 +0,0 @@ -saw.txt saw.txt /*saw.txt* diff --git a/vim-saw/plugin/saw.vim b/vim-saw/plugin/saw.vim index 718a6f4231..75b6225b63 100644 --- a/vim-saw/plugin/saw.vim +++ b/vim-saw/plugin/saw.vim @@ -7,14 +7,12 @@ function SlimeOverride_EscapeText_saw(text) set paste exe "normal! i" . a:text . "\" set nopaste - " remove blank things + " remove blank things: silent! keepp g/^\s*\n/d silent! keepp g/^\n/d silent! keepp g/^\s*\/\/.*\n/d - silent! keepp %s/\(\/\/.*\)$//eg " remove end-of-line comments - " copy buffer contents into res, adding a backslash at the end of each line - let res = join(getline(1, '$'), "\\\n") - " q " close scratch split + silent! keepp %s/\/\/.*$//eg " remove end-of-line comments + let res = join(getline(1, '$'), "\\\n") " copy buffer contents into res, adding a backslash at the end of each line bdelete __saw_slime_temp_buffer__ " delete temp buffer (the following didn't work reliably: setlocal bufhidden=delete) return res . "\n" endfunction From 86bb800644bfc39d1f929569f202fb1be6b9ce7d Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 14 Jul 2021 14:23:24 -0700 Subject: [PATCH 10/17] Add test case for unfinished proofs. Fixes #316 --- intTests/test0069_unfinished/test.saw | 14 ++++++++++++++ intTests/test0069_unfinished/test.sh | 3 +++ 2 files changed, 17 insertions(+) create mode 100644 intTests/test0069_unfinished/test.saw create mode 100644 intTests/test0069_unfinished/test.sh diff --git a/intTests/test0069_unfinished/test.saw b/intTests/test0069_unfinished/test.saw new file mode 100644 index 0000000000..3399406c50 --- /dev/null +++ b/intTests/test0069_unfinished/test.saw @@ -0,0 +1,14 @@ +enable_experimental; + +let andI = core_axiom "(a b : Bool) -> EqTrue a -> EqTrue b -> EqTrue (and a b)"; +let script = do { simplify (cryptol_ss()); goal_apply andI; trivial; }; + +b <- fresh_symbolic "b" {| Bit |}; + +print "The following proof should fail because the proof is incomplete."; +fails (prove_print script {{ True && b }}); + +print "Now we check that the 'prove' command also does the correct thing."; +r <- prove script {{ True && b }}; +caseProofResult r (\_ -> fails (print "We should not get a theorem!")) + (\x -> do { prove_print z3 {{ x == () }}; return ();} ); diff --git a/intTests/test0069_unfinished/test.sh b/intTests/test0069_unfinished/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test0069_unfinished/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw From 292aafda97e3e630f6ec4cd52394c9b6decce6b8 Mon Sep 17 00:00:00 2001 From: Sam Breese Date: Fri, 16 Jul 2021 01:00:37 -0400 Subject: [PATCH 11/17] Update Macaw and Flexdis86 submodules (#1379) --- deps/flexdis86 | 2 +- deps/macaw | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/deps/flexdis86 b/deps/flexdis86 index 4e6f4950be..6d6e8c39e7 160000 --- a/deps/flexdis86 +++ b/deps/flexdis86 @@ -1 +1 @@ -Subproject commit 4e6f4950be909b41852b50e5648d243d948fa0c9 +Subproject commit 6d6e8c39e754dc4c9910b1c0dc494e2eef8e309f diff --git a/deps/macaw b/deps/macaw index d9fa8af6c8..135fb062bb 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit d9fa8af6c8b2b9519883e150e7bed01665c5f9d4 +Subproject commit 135fb062bb35a145ac21da816244d97e6d70f425 From 1a8f0e01247ecaae5ecc6df49fc505513d7349c3 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Sun, 18 Jul 2021 20:21:41 -0700 Subject: [PATCH 12/17] Incorporate crucible fancy assumptions --- deps/crucible | 2 +- deps/macaw | 2 +- .../Verifier/SAW/Heapster/SAWTranslation.hs | 2 ++ .../src/Verifier/SAW/Heapster/TypeChecker.hs | 1 + src/SAWScript/Crucible/Common.hs | 2 +- src/SAWScript/Crucible/JVM/Builtins.hs | 25 +++++++------- src/SAWScript/Crucible/JVM/Override.hs | 10 +++--- src/SAWScript/Crucible/LLVM/Builtins.hs | 34 +++++++++++-------- src/SAWScript/Crucible/LLVM/Override.hs | 10 +++--- src/SAWScript/Crucible/LLVM/X86.hs | 4 +-- src/SAWScript/X86.hs | 11 +++--- src/SAWScript/X86Spec.hs | 13 +++---- 12 files changed, 65 insertions(+), 51 deletions(-) diff --git a/deps/crucible b/deps/crucible index 584d47d384..168f000959 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 584d47d384104c06a92b3820882639e9898e4b0d +Subproject commit 168f0009591833358b8dc8a9a3f76e09edeb3e4d diff --git a/deps/macaw b/deps/macaw index 135fb062bb..764de152ce 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 135fb062bb35a145ac21da816244d97e6d70f425 +Subproject commit 764de152ceb0166aa04ec1a0ddbb2806b2595926 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index c761009ecf..9da457a795 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -599,6 +599,8 @@ instance TransInfo info => return $ error "translate: RealValRepr" [nuMP| ComplexRealRepr |] -> return $ error "translate: ComplexRealRepr" + [nuMP| SequenceRepr{} |] -> + return $ error "translate: SequenceRepr" [nuMP| BVRepr w |] -> returnType1 =<< bitvectorTransM (translate w) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs index 3724d07053..2579b458b5 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs @@ -331,6 +331,7 @@ tcExpr WordMapRepr {} e = tcError (pos e) "Expected wordmap" tcExpr StringMapRepr {} e = tcError (pos e) "Expected stringmap" tcExpr SymbolicArrayRepr {} e = tcError (pos e) "Expected symbolicarray" tcExpr SymbolicStructRepr{} e = tcError (pos e) "Expected symbolicstruct" +tcExpr SequenceRepr {} e = tcError (pos e) "Expected sequencerepr" -- | Check for a unit literal tcUnit :: AstExpr -> Tc (PermExpr UnitType) diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index e6cca931a6..45f9681972 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/src/SAWScript/Crucible/Common.hs @@ -58,7 +58,7 @@ sawCoreState sym = pure (onlineUserState (W4.sbUserState sym)) ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann) -> AbortedResult Sym ext -> PP.Doc ann -ppAbortedResult _ (AbortedExec InfeasibleBranch _) = +ppAbortedResult _ (AbortedExec InfeasibleBranch{} _) = PP.pretty "Infeasible branch" ppAbortedResult ppGP (AbortedExec abt gp) = do PP.vcat diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 795da169d1..6032f84365 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -59,7 +59,6 @@ import qualified Data.Map as Map import Data.Maybe (fromMaybe, isNothing) import Data.Set (Set) import qualified Data.Set as Set -import qualified Data.Sequence as Seq import Data.Text (Text) import qualified Data.Text as Text import Data.Time.Clock (getCurrentTime, diffUTCTime) @@ -132,6 +131,7 @@ import SAWScript.Crucible.JVM.Override import SAWScript.Crucible.JVM.ResolveSetupValue import SAWScript.Crucible.JVM.BuiltinsJVM () +type AssumptionReason = (W4.ProgramLoc, String) type SetupValue = MS.SetupValue CJ.JVM type Lemma = MS.ProvedSpec CJ.JVM type MethodSpec = MS.CrucibleMethodSpecIR CJ.JVM @@ -276,7 +276,7 @@ verifyObligations :: JVMCrucibleContext -> MethodSpec -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> [(String, W4.ProgramLoc, Term)] -> TopLevel (SolverStats, Set TheoremNonce) verifyObligations cc mspec tactic assumes asserts = @@ -333,7 +333,7 @@ verifyPrestate :: MethodSpec -> Crucible.SymGlobalState Sym -> IO ([(J.Type, JVMVal)], - [Crucible.LabeledPred Term Crucible.AssumptionReason], + [Crucible.LabeledPred Term AssumptionReason], Map AllocIndex JVMRefVal, Crucible.SymGlobalState Sym) verifyPrestate cc mspec globals0 = @@ -511,7 +511,7 @@ setupPrestateConditions :: JVMCrucibleContext -> Map AllocIndex JVMRefVal -> [SetupCondition] -> - IO [Crucible.LabeledPred Term Crucible.AssumptionReason] + IO [Crucible.LabeledPred Term AssumptionReason] setupPrestateConditions mspec cc env = aux [] where tyenv = MS.csAllocations mspec @@ -523,11 +523,11 @@ setupPrestateConditions mspec cc env = aux [] do val1' <- resolveSetupVal cc env tyenv nameEnv val1 val2' <- resolveSetupVal cc env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' - let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition") + let lp = Crucible.LabeledPred t (loc, "equality precondition") aux (lp:acc) xs aux acc (MS.SetupCond_Pred loc tm : xs) = - let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in + let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in aux (lp:acc) xs aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ @@ -593,7 +593,7 @@ verifySimulate :: [Crucible.GenericExecutionFeature Sym] -> MethodSpec -> [(a, JVMVal)] -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> W4.ProgramLoc -> [Lemma] -> Crucible.SymGlobalState Sym -> @@ -630,9 +630,10 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat = mapM_ (registerOverride opts cc simctx top_loc) (groupOn (view csMethodName) (map (view MS.psSpec) lemmas)) liftIO $ putStrLn "registering assumptions" - liftIO $ do - preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes - Crucible.addAssumptions sym (Seq.fromList preds) + liftIO $ + for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) -> + do expr <- resolveSAWPred cc p + Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr) liftIO $ putStrLn "simulating function" fnCall Crucible.executeCrucible (map Crucible.genericToExecutionFeature feats) @@ -731,14 +732,14 @@ verifyPoststate cc mspec env0 globals ret = obligations <- io $ Crucible.getProofObligations sym io $ Crucible.clearProofObligations sym - io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations) + io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations) where sym = cc^.jccBackend verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError loc err))) = do st <- sawCoreState sym - hypTerm <- scAndList sc =<< mapM (toSC sym st) (toListOf (folded . Crucible.labeledPred) hyps) + hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps conclTerm <- toSC sym st concl obligation <- scImplies sc hypTerm conclTerm return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, loc, obligation) diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 4d43bcc447..7e9c35f199 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -243,13 +243,15 @@ methodSpecHandler opts sc cc top_loc css h = do case res of Left (OF loc rsn) -> -- TODO, better pretty printing for reasons - liftIO $ Crucible.abortExecBecause - (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn))) + liftIO + $ Crucible.abortExecBecause + $ Crucible.AssertionFailure + $ Crucible.SimError loc + $ Crucible.AssertFailureSimError "assumed false" (show rsn) Right (ret,st') -> do liftIO $ forM_ (st'^.osAssumes) $ \asum -> Crucible.addAssumption (cc ^. jccBackend) - (Crucible.LabeledPred asum - (Crucible.AssumptionReason (st^.osLocation) "override postcondition")) + $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum Crucible.writeGlobals (st'^.overrideGlobals) Crucible.overrideReturn' (Crucible.RegEntry retTy ret) , Just (W4.plSourceLoc (cs ^. MS.csLoc)) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 25a76c0196..e7a33e0f30 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -198,6 +198,8 @@ import SAWScript.Crucible.LLVM.Override import SAWScript.Crucible.LLVM.ResolveSetupValue import SAWScript.Crucible.LLVM.MethodSpecIR +type AssumptionReason = (W4.ProgramLoc, String) + type MemImpl = Crucible.MemImpl Sym data LLVMVerificationException @@ -603,7 +605,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp = verifyObligations :: LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> ProofScript () - -> [Crucible.LabeledPred Term Crucible.AssumptionReason] + -> [Crucible.LabeledPred Term AssumptionReason] -> [(String, W4.ProgramLoc, Term)] -> TopLevel (SolverStats, Set TheoremNonce) verifyObligations cc mspec tactic assumes asserts = @@ -738,7 +740,7 @@ verifyPrestate :: MS.CrucibleMethodSpecIR (LLVM arch) -> Crucible.SymGlobalState Sym -> IO ([(Crucible.MemType, LLVMVal)], - [Crucible.LabeledPred Term Crucible.AssumptionReason], + [Crucible.LabeledPred Term AssumptionReason], Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)), Crucible.SymGlobalState Sym) verifyPrestate opts cc mspec globals = @@ -772,7 +774,7 @@ assumptionsContainContradiction :: (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> TopLevel Bool assumptionsContainContradiction cc tactic assumptions = do @@ -803,7 +805,7 @@ computeMinimalContradictingCore :: (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> TopLevel () computeMinimalContradictingCore cc tactic assumes = do @@ -814,8 +816,9 @@ computeMinimalContradictingCore cc tactic assumes = findM (assumptionsContainContradiction cc tactic) cores >>= \case Nothing -> printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction." Just core -> - forM_ core $ \ assumption -> - printOutLnTop Warn (show . Crucible.ppAssumptionReason $ assumption ^. Crucible.labeledPredMsg) + forM_ core $ \assume -> + case assume^.Crucible.labeledPredMsg of + (loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason) printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous." -- | Checks whether the given list of assumptions contains a contradiction, and @@ -824,7 +827,7 @@ checkAssumptionsForContradictions :: (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> TopLevel () checkAssumptionsForContradictions cc tactic assumes = whenM @@ -953,7 +956,7 @@ setupPrestateConditions :: Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> Crucible.SymGlobalState Sym -> [MS.SetupCondition (LLVM arch)] -> - IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term Crucible.AssumptionReason]) + IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason]) setupPrestateConditions mspec cc mem env = aux [] where tyenv = MS.csAllocations mspec @@ -965,11 +968,11 @@ setupPrestateConditions mspec cc mem env = aux [] do val1' <- resolveSetupVal cc mem env tyenv nameEnv val1 val2' <- resolveSetupVal cc mem env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' - let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition") + let lp = Crucible.LabeledPred t (loc, "equality precondition") aux (lp:acc) globals xs aux acc globals (MS.SetupCond_Pred loc tm : xs) = - let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in + let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in aux (lp:acc) globals xs aux acc globals (MS.SetupCond_Ghost () _loc var val : xs) = @@ -1155,7 +1158,7 @@ verifySimulate :: [Crucible.GenericExecutionFeature Sym] -> MS.CrucibleMethodSpecIR (LLVM arch) -> [(Crucible.MemType, LLVMVal)] -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> W4.ProgramLoc -> [MS.ProvedSpec (LLVM arch)] -> Crucible.SymGlobalState Sym -> @@ -1209,8 +1212,9 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as do mapM_ (registerOverride opts cc simCtx top_loc) (groupOn (view csName) funcLemmas) liftIO $ - do preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes - Crucible.addAssumptions sym (Seq.fromList preds) + for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) -> + do expr <- resolveSAWPred cc p + Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr) Crucible.regValue <$> (Crucible.callBlock cfg entryId args') res <- Crucible.executeCrucible execFeatures initExecState case res of @@ -1302,7 +1306,7 @@ verifyPoststate cc mspec env0 globals ret = obligations <- io $ Crucible.getProofObligations sym io $ Crucible.clearProofObligations sym - sc_obligations <- io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations) + sc_obligations <- io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations) return (sc_obligations, st) where @@ -1310,7 +1314,7 @@ verifyPoststate cc mspec env0 globals ret = verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) = do st <- Common.sawCoreState sym - hypTerm <- toSC sym st =<< W4.andAllOf sym (folded . Crucible.labeledPred) hyps + hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps conclTerm <- toSC sym st concl obligation <- scImplies sc hypTerm conclTerm return (unlines ["safety assertion:", show err], loc, obligation) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 39a9924072..826f1d0f4d 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -475,13 +475,15 @@ methodSpecHandler opts sc cc top_loc css h = do case res of Left (OF loc rsn) -> -- TODO, better pretty printing for reasons - liftIO $ Crucible.abortExecBecause - (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn))) + liftIO + $ Crucible.abortExecBecause + $ Crucible.AssertionFailure + $ Crucible.SimError loc + $ Crucible.AssertFailureSimError "assumed false" (show rsn) Right (ret,st') -> do liftIO $ forM_ (st'^.osAssumes) $ \asum -> Crucible.addAssumption (cc^.ccBackend) - (Crucible.LabeledPred asum - (Crucible.AssumptionReason (st^.osLocation) "override postcondition")) + $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum Crucible.writeGlobals (st'^.overrideGlobals) Crucible.overrideReturn' (Crucible.RegEntry retTy ret) , Just (W4.plSourceLoc (cs ^. MS.csLoc)) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 43f48450c2..88dbcfff99 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -914,8 +914,8 @@ assertPost globals env premem preregs = do st <- case result of Left err -> throwX86 $ show err Right (_, st) -> pure st - liftIO . forM_ (view O.osAssumes st) $ \p -> - C.addAssumption sym . C.LabeledPred p $ C.AssumptionReason (st ^. O.osLocation) "precondition" + liftIO . forM_ (view O.osAssumes st) $ + C.addAssumption sym . C.GenericAssumption (st ^. O.osLocation) "precondition" liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) -> C.addAssertion sym $ C.LabeledPred p r diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 384d75b38f..01b143ff21 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -27,7 +27,7 @@ module SAWScript.X86 ) where -import Control.Lens (toListOf, folded, (^.)) +import Control.Lens ((^.)) import Control.Exception(Exception(..),throwIO) import Control.Monad.IO.Class(liftIO) @@ -72,7 +72,8 @@ import Lang.Crucible.Simulator.ExecutionTree ) import Lang.Crucible.Simulator.SimError(SimError(..), SimErrorReason) import Lang.Crucible.Backend - (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,proofGoalsToList) + (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,goalsToList + ,assumptionsPred) import Lang.Crucible.FunctionHandle(HandleAllocator,newHandleAllocator,insertHandleMap,emptyHandleMap) @@ -564,15 +565,15 @@ gGoal sc g0 = boolToProp sc [] =<< go (gAssumes g) getGoals :: Sym -> IO [Goal] getGoals sym = - do obls <- proofGoalsToList <$> getProofObligations sym + do obls <- maybe [] goalsToList <$> getProofObligations sym st <- sawCoreState sym mapM (toGoal st) obls where toGoal st (ProofGoal asmps g) = - do as <- mapM (toSC sym st) (toListOf (folded . labeledPred) asmps) + do a1 <- toSC sym st =<< assumptionsPred sym asmps p <- toSC sym st (g ^. labeledPred) let SimError loc msg = g^.labeledPredMsg - return Goal { gAssumes = as + return Goal { gAssumes = [a1] , gShows = p , gLoc = loc , gMessage = msg diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index 1c53e145d8..05ff826a3e 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -103,9 +103,9 @@ import qualified Lang.Crucible.LLVM.MemModel as Crucible import Lang.Crucible.Simulator.SimError(SimErrorReason(AssertFailureSimError)) import Lang.Crucible.Backend - (addAssumption, getProofObligations, proofGoalsToList - ,assert, AssumptionReason(..) - ,LabeledPred(..), ProofGoal(..), labeledPredMsg) + (addAssumption, getProofObligations, goalsToList + ,assert, CrucibleAssumption(..) + ,ProofGoal(..), labeledPredMsg) import Lang.Crucible.Simulator.ExecutionTree import Lang.Crucible.Simulator.OverrideSim @@ -826,7 +826,8 @@ makeEquiv opts s (Pair (Rep t _) (Equiv xs ys)) = let same a = do p <- evalSame sym t v a let loc = mkProgramLoc "" InternalPos - addAssumption sym (LabeledPred p (AssumptionReason loc "equivalance class assumption")) + addAssumption sym + $ GenericAssumption loc "equivalance class assumption" p mapM_ same rest @@ -847,7 +848,7 @@ addAsmp opts s (msg,p) = _ -> do p' <- evalProp opts p s let loc = mkProgramLoc "" InternalPos -- FIXME - addAssumption (optsSym opts) (LabeledPred p' (AssumptionReason loc msg)) + addAssumption (optsSym opts) (GenericAssumption loc msg p') setCryPost :: forall p. (Eval p, Crucible.HasLLVMAnn Sym) => Opts -> S p -> (String,Prop p) -> IO (S p) setCryPost opts s (_nm,p) = @@ -1132,7 +1133,7 @@ debugPPReg r s = _debugDumpGoals :: Sym -> IO () _debugDumpGoals sym = - do obls <- proofGoalsToList <$> getProofObligations sym + do obls <- maybe [] goalsToList <$> getProofObligations sym mapM_ sh (toList obls) where sh (ProofGoal _hyps g) = print (view labeledPredMsg g) From 6ef2c2e8572679b8ff2291b1865ebb2c932babab Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Sun, 18 Jul 2021 20:29:20 -0700 Subject: [PATCH 13/17] Update crucible to get llvm debug information --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 168f000959..f2abe5388c 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 168f0009591833358b8dc8a9a3f76e09edeb3e4d +Subproject commit f2abe5388cee9f717af7a1dccf956a6896b47c51 From 0ffefe0a11faea35993f292aa7bca98e4c40cf95 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Mon, 19 Jul 2021 08:47:47 -0700 Subject: [PATCH 14/17] recompile salsa20.c to update debug information --- examples/salsa20/salsa20.bc | Bin 11968 -> 12032 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/examples/salsa20/salsa20.bc b/examples/salsa20/salsa20.bc index 808474461be045342e3a2a861484595acf0b0ce0..bac4c70a9e7afd28d59c3f736e33af889cc93008 100644 GIT binary patch literal 12032 zcmb_?dsti7mG3@!oFjyg4j^n{3w#9Fl^ucw*ciWJNeCMpk`aE@N!+o-E8t)d58L26 z=@AkUc1TC|(3G^9R@hET8aKg>Z^mDylaY9pIK(B1r{%hC0(R=_X55yvX+D3sndbiX zk%VcQ`S0?fqqEmpd+oK>Ui-J#+DGq)7bg<@>G8RpM+ipAH1(ZZg8bZd@ge1yLM27Yvd^m6RN!x^?oaGDFpJM!)0mEnGMK~+zgXVjGKND1`vwo|g23DtSMP_ng0c#|op@*7r}R|WHr4edKA zj88!BaRKAuyCAD4L8$3gq-LM><8s445Y(qs^!6tDM=SVq5hHU-VNFrwOeTvAGbWtq zGOG%<5>}@6=9Jqn85#3rvf_EGT5OnDDc`{>(qt=7be-KHlt$J#(wLPKt7Mh@R!1`b z^lLkW@4e7)~~r4~vGt zks#M;4zz^0!xMp`VBp9gcSH!Z3V|Xa&^{Ds$9=u8vxn;p1&SPQDw zqf-?)Yz`EOfg@$ykx-yD7$`Dxhsy$o$t_#vM*~JNlJWjP(xfeOcp&4_K+?=?#=DV> zTLZ=q2a+y%Gu|D@xEjuQKaz1(%(!GSPBOx^*^H|~#g9(91Bb;xQ7GWyIgH+US997uoG~1ML;lC^zRt2hn@4i&6jk_0|5y8Sm}(9yhMCM6 zIAqrNcgpm0M^%BAy)d8a?BI^lxx*v|iuk}$3)g1mIx$~m+~a1B=tvi)CiC)u@fIe9 z$^3{B1FasebAmfUR7X`@XK|pFPHUhQb2>=Fpp*R4Wt=lCZ!t$0O&U{eKu|E#vQ-$YOe{gd$8SvK(cIZMoUg-UPHh{jF^|Na`hkr zCQ#HLIAYDcHMS+LYxn}1MLU?GYSY$c-(?xP3;y(HpmOZ)4O;%bZ zBcdemoRD8)WUd$sAw!~R_ev*EG>RBWAu2U5wt7zzmpMieNUp1Fw>Dj=5Se&C7gMt8 zTh?4+(8ee#l4#iRtisQPtucy~>vi}PWcKURlPiL~2`jdZD@xR-%p<aR`>*J77s1l8%v&K3- zv$?0F*gw*1m)25Se~acO(fyv+ej;iMHFkt)1{P19MJciQmQKnyPn2x#m2aNx=xz6K z-^3Cs3wS)-QIGs^N5CTl(kGL(w}aYQi>}F{yD_Job7~9u(Tw+jXr_!|cV?aC_{N|4 zHcpkSzaZcAGv6k^eBs_cJcIV#`{p9EPdmUZ}SD;QvXPCZ^`<}kxdsP>nBEF z?QNIt_cQFAp!=;w_gg{tsZ-m;Yj0SzX#RPI{oRcAL#Or* zjlWKTkW2V(%`6j2dNk$#)zf-dwXOzrgC9it*?zY<2w$-%5J7 za&KF8YlEkKb!~_Hpr^664K%51b)&oKQQ+>vm`9fa&VP1V(fn|SNySx2R z+y3@LO>GU2Hr3V$4NdJkLEpK%q@;A`PI|l5R$j4tN2%k8yR}Z(6BXvDtvd9mP~KG6 z9H$(qu6MWYZ)-SO>ntx3DryhcHm;|+Fi}f zjj+XWf7|K@+|~cEb8lW-&10(%wY9EpXsT{JR8zZpe|x6~#_T@?or?Fj=heq<=5?h* z{{I}LupmAPy?d;-v#q_g)_t(4p$ZywywFZ(l@LppwIW-kSleaYm96sQYhSjiqUeg= z@&O+5{mc@|#PFJ3#7l@g4LMwR6K7>v1K})}1@iM^pCA;fsw`}FsjO1;%KQvK#mb^n zSYu1CxFUfRL6V7fBz@B2DlZxlS6^fC>P;)U{&Tn-R_r_#$MIR4g{Ur?GRB{B(q>wa7q}mP+|1JZp;$DhqOj z$+8d^KFNezj6ZM5n`N6^>MDV)pGh&U_uvNq&ny+YHVpcf4$5neGmol264-*2{?NYZ z>DyQLO^jaNH~!Jqgx7ne=GFHnKAOI?Z*qG0^3AQLDIw{KD`|(j`qjtU%CqljJF|4T zO9K8E;Rc$JC#qY`z%1_QUQd6?WlCz1@Hi>Vg!CGO%Bl59@ zkp1}1+BOlaT+)+HX>U1IJ}QeYm+IC|PkUhjLZhj;1bGXXc(Bv%I9*KD+cO_n1fh#$4j7CtUjbE)>_L zF{_T%SH4X-uUCQd$8%$pbIuf-F^K%K0?Nq51a2q7N@odBz)0f=-zUtrb^2a!*^9@i28$yQHCKmQrvp` z?3v^1&BXP#&?6f%UFqwWL<^i&joLc>h{;VY1SFa=1ca z+k3{6YGVDnL8-CsecqC4<9}(^EaiJjNjA%oE?4Mh%x&azx*1%yd_q$@OSLnsSkfya zVB2<=E%INK?LTmtXB%~-N7>l5^U}N$+ZzknCj2qBF~>ZcO=A1^g=~{?HvgJ=Hb!Fm z*+RA{iLKXQB&sg&pV*h^vzfo*I)%>{BfU0v>RVU@$j_J_FVFdt7w?jmwrv zgMQ@E9+^`Vs)@DSR;M}f!{RcA zJh`+>rJ;?zXw;=YDfH)?pQy@G65)BFkRAJny=Ms-Ns1^~+VG(9s>a7->@7AHjkEfi z@z9;)g@Te8npCSSQs*Q|5}QRE*9~}5BnbHiG2JK2Rqr6;LtXX5lomWdFz$Khc8r^F zBHdS&8$`Bh@5!%r_KsDniRBu9JV zt9+>J1wzs-=onO@;}qjot zU`x$Fzl=<#7^x^dMCBw`kB1D2Z|TWQSCN9;e_lp{+n}NS z-Zwx_oN(1?)c=e3;XYX|CpL@tpj$;r<{bgm+r{UH6htRFXI~Y?VEAI!p z2}zMxQEL8AuyWR^m~`4mMq{$T;-o#tLWrO`D|KvM-<~*s`^Oh#t^72TgGIst#a{WxVKcf2vz`}r^i5*iv#x%^0p08 zuKu?W1Z-G;5rr|HxEDWr53w%hiYI)VApUk&8{#v+nD7dD`C`^YN!L9}(!bn;*!(v$ zy7p-4*tfdJVYG)DZC`!g9wMg7!28MRY9+ZS>JE&DrV{gAN-`lHrwo~3$kQI4;}B(5 zhF_r(H9ZKQdL5m?Tcr_*>WGR;0jCt0pPWYbTcSmg$`YlO%I-q_G9mUP$Y;8IUxNe! z2~Q^VWT|LGJ~M+Q@M#tLgtiFdy|(1VzedCM@WT%ysCJMJ{iH2A?Bp| zWeb6G_iGT2uPWYwW-n45hF5o05-|xnir9(?h5SbpR{d+5L&CGe&zLfEzE0s;+Eb6= zJ5^zm_Eft6j`kA1k{|8ER%)+E<|{3ueRQ9Y_EWlvO8cqW!S2F6-A7w%5ASbmXm4+< zt!=7la5o(R{iU-vZpdf8FL#FIB4ZtulMPTt&U0-;$9ZuJwzaNhyFM_E+6cCI?FiVcOg=(jgY$FLj>I)ggww#o(hSWLgkxdwy z(k0@=%86cE3+G!#teoHaJt+`eDnROWEx(13qclWkyb$Dx__4M!EzmNZK)OVUhDhI>r)%n@Pp)Yf%X{7nz4nArAQ$`gPyh57)+71uO03=cenjvp% zG;i9!>4I!C(cI0OoOi4=8#+Db9Yr>@bvE&M)t=1id z25~st9xwCKQj}+i`J_2rY4wg;&18Gdc01!-p6^kM+mCy9k_vu!MzccY7THw4rOcPm z^#Yr!IGD6TC0`nk;lIy)q?E`{)15}EAtfH#KV{F;m=$Tv2I&Q%ovf?o0fLQIeezwl zAw1jiIZY|zY$jb*l#S=_vb{pt?kr@>kFr&HD5PFma#6}k{x8@{=$#JhV6$<6#M6v( z(HuxhZs?+;iPsfh3dQ7@fFasVTqro>Zw5`_d+7t_r~cCMG!h0RJgDAAuq zHz=BG2;LqU;cWmbSE9H)H~o&0#70Rh)JrugsT_GUendLT=h5 zSCm_S9CJm#V}QEC8*_z)y25gNdm0hn4bgP8d>=U5rOe>LtevneoMZ({al!*>(YZPy z>9axL<2x@o;G@&=wMyhT&ZRsOyW)iMG(!H5K)is@oUGm0fDKUYL8{y>(TWY2?w|&W z&CfZWhn;QCAcAdq9#W%IQfg#A3G-^gfMjpVcVRQ__8kH83gch76PtH0+zSH@h*}mAiz+` zJkCdFJqW9o=OeodE~82K-h>sH(9saF@|trVB#kG&W3V%%eLUnkE+AF~Y}jJsj8GgpC&Dl9!@Oc+>ivGC;Ld*-WUJf#_Uayj%T`A%EeV|FWu2m=|P&?9nz24nc z-&WglG`g4H@a?{JcQ1dabdKAjOV_uVw_4K_~*7|$BywFL&17W z=)NssXt|=)4z(hxAQsIX=fdG3V_scLm0zZiCP1=%W#t<0BCr7p}hQoYe)v_6W? zd_o*gv)Gpbc3VEAkVo*L=p5nRM_v%CWvuv&$a`XmYl+h-G`Dve)58zwcf z+*-unc*xw%03v(oGI_zu0+ws&GO={8Qz?mc6^~^ytiMWQNCLy1R-cnrFb;%cuR)LE zl__FrX06_dk?y4<9C=wTXHOu^d(nO^DQ$;9M_p&SH!h=Lw1P7covx zlyf^O;M@q7PQN`FOEHsE%; zX91+VYTZf__LR5=pt4t;j7F}{OY4zUG%wD`SfTlTzIn$03SdLN8D)X*?W8WO$FykW zT8%vLDOz%_+K1}b&=W&q#iHn%bi##$mLPVSrTpG?n2E7f<`?KpyxD6zukMM%@}AlC z(oAfiGqK0CfzE`pA2YGHJA#>5Qw1^S=0Y)yiKvr+G1~&aPh5ebwkO{mEg8Ggv?voL z=-NAA1$5n-dD=$zAgM4*)8k>HI$AQA3@91I35uYl_tXz!QA-H=@PG!W@6^hYp~k~* z+9+@VO6rw5T8qh&F=zfLr#or>VfPwoFp)jTR-Wnwu8tdc%5Zq1&ZXDk(ES5%KQqC7*>qNaVo5PP2&=}hoA8#t)hDk^&Czj?u9xo?CM3u@~SqGfDxOiQ)^8#~)BjQ%N zK`NJS0^0=&^B&*xI;l>^DUY7Ghhr6@?01Orb>e4)OsVLGSTBD`N1};H^Ux>Q2CS;V z_+FgOBZT(3e$#9Fm~}$QC5#I3*5vsMLmIKrh9XlO;dzSv(ON+Kn_8d{bohM}Tp_(# zjQVy|L7Av;Ynl&LHP*H^A8M+J)pkpLn}xf+Z8<*0{c0WC$&;|cmQ)OXF2MmG{Hcoj z^U|j@QIyjIE8XvKq4-$sV&MUOJv?Ccy{Ld?FEk86^az zV@4G`Jr#*mYT)eIBsxV6=yWHls<#NLo`tH{|0}A82`o2WC6(xKC!oNra!6*5MF<=pWLNy`2wFnLv=%?p> zF(;U#l3f`-LK$FfrnvY0<(TR5KyyH_*wjeg1nBqR@lQ0G^NxnKZF3{MJj)&#(*jU4& z%9qx};HoWu8ynYYsc%xe3(rWgaX=F#ya$358{3nj1O!XmEwR}6PkQzt#l}m2l3ced z9viurrBHCiV`FGMJRdAlYz$qA5_lFM-^0joZr$$j=u3bqdvSC@N@;|>d`apQf|NCM ziY{)DbdMldoX^u>StXYU%sNDmM5u}qY#^XkM8aVUaNF{+XOFGL>4ozJbdtRkHD^9H z&iz@^{TOsVL`NMepeHYWUZi!w4{5NRi+R8;VSX~ zg|!A8Ei4H}fUTEe7*pZjO5dprB-3{)_5M=z2&*{H$CJsLIf}L;659R=cNA?Cm-wX= z#%GV0_(AU<@l1D}GECq?OZ?o!Jjz3yxy`4(c2;^1;-?Jp!?g23J5o5{yAa1Yb-Dy` zgod#%wqK5AB_i)!Ljk6~&q-*SQ|(++jx;fy&ffP{AuW>8v?wVJS)dfsb&05oMOqb~ z>6Vde^x*j&7ldT9EI?__YjeGA(7&CEQ{ru5Fuezp_%jqYO~@W`P++BRBu=kKqvst| zaR9Fp%IPtO7u0;4C&(>DB!0nqT|PL z4{X{61rAaV{NUcW2mT2PcuHt)>4V+91_KsEWE&^FQ20gM+%aly@JDnxEj0H!HMdMd zZL=b?j@lN=f#_i?ElPJmqLe?%PE)@`86Sx=3eaKZNm{6?V0tv^^Zi06TMGw;<}Dti z7O$OxOPOR?G{QOrn#wa7Xl$rOXk;+Win!%p*ftD!Fu`D6!*jYSjjl&`$bsJ zV7+{Aoo(tqtP$yuO?ttISRR8%r5AG7|3c$aS{!n^LTFO=@qbG-79b(^%CSQ_^OBCv z!jzr9v>S{7=@Mwr1b>ShOhKbo^%tDX+CA`a3Pd=ildO;b8ap)hUZ6d)Y%~j-Sb`Mz z8b5>DBnWCaErPsw;!}r^x&2<2mCM zv}sOG_dm)Ml^*@3KM5O@dJ^)#alZtgKjQ=Flzvx>uleWnKK>Ij;5)%k5)XY*4R3!z zatKjDRx;Wqe5fBNU6l*m06h(DxJL@II6W^$FI_+<0wE=!W9ua}$)n>?eo9B(Bk5QR zT6&C5WnQy`Uzc}zYTP%&y)DX^`Ub7pwsp<_|S=q^Y_K*&wq)27Ido51$-9j za~^amKa9^p`NN=7pHJbVz$Y&M=b+Q~I`ogOBZ(d(d;@~N2^!|^Kj_@;-(TI_)YhIy z_pA6>eO@zd#eM`-S@~#R=*6PaVZY`-|4x>-OMx zQuiKoS2wqHiMR}I_pIhyht<8 literal 11968 zcmch7eOwb)*8iPMm;{)F0fGeZWdL7LQ6~xVQndyWC~CAQNNKg}L|#M}Fo;sDeHjQK zD!S3K7OQmwRTta3ixn-pcAG%7tQ%WYT5)SzsFr2-@v&HKS9jg+bM8!h>F)E#^ZEVp zOJs5`ZAhE=pZ}^tYMK1o`t}lqB?eG zYL9###pqLZ5w-LLKV`&N`L>mUHeHssD=^K&=rzeo?YscJd37 zGz70~bG8}Jju0Scu@<4_@ENt$sJw`-*rK}r1+O4MUToAdH?q{Xxu8-M^j((vnnQg% zOI^yVM|#zRMzxSqOV09|Qc&%z)266q`|MiNtR_>Gt9#Y~`>bA5N{=b3iJW!7Gz;Bf zgTBvFy9U(X_EJM^&|t6nn_g;UME#cm^_?vBcfHg%F7;n})uqs3Kwaumf5WJU5OZ@x zUFuNZa!|_v|Lp*x5a+qk2}Y9dw9lCTDk~&Z;HnI7wbT=)!s; zUChF2=kT~ychx+f(b1X8?>Fl0eYfl0F|2I*KgRtRT z(6_w$4k+VNf6J)vJk+G!t^E-^_9_}L{K?1=?IrA1?7?wpwaKbXjWkAW%?HP7615E| z-gvwvvxZd}!SVCJ?-ckwwAR?n(4q3yW=0uGU1KKF@+B4~gxJC&6a&xoF%AA~L7hA_ z_CPIMuGO|UG$EG8#=u&Sg?ZOKn%E^bhRDZzg9U;(!)~pKQ|dDiB@3t?KQHavXd=!V zEI(rm5TYa3of9tVR`#$qb1`Q&*_Z$o{v!0IDfHK zF3Yqig`UYMAf$$EO2B$1yyPNh-SwO0v?nSRRf3{2ZgXPsW}9~N3(bm`8pvduJ=sAf z33gQ>IICCvqPTvQM#YP~Vm)|GP}rP`a#m5*OWhO{FEWZsr=o)OJw3)K)(MIyg3Ot0 ztT{s%<7F)K2xLUa#rzo|@PzoPPYz^6{KFmR*(e}zA$|$bi{yv|pW+u?J`rgHq&DA> zO%S})My7p%sGgK=v|kq>j*;3fW-}=a`a0Dok47|XJN)82gNRR-+CuaW#bZ;rVD0cm zgjbJ@Kq~muk8RdO1X~=9{u7@%D>uc=cPisD(+;J_&+tE`cgzfNI72f6cG+UdJ@Z=W zpy{xq5!wg_d1-YmEX!%YewIy)Y z-c38Fteg_?#+1LmadhWK-GYk1`~`$SAo$l{)rX%=44+6|)1UqJ;F{l9%5F|*ym@5d zjl!D;=^5{;b{r|WSvbA1bh?Eqva|Gkexw);74W|w8txkY>(K9q(Mlc_72tn7es^}B z_SPLeU-t)Br?Zr4tPY{~(`r`}?Y*4yX>ZnrJ`M8LqZYY+lAYuxkhcppO`ejLO1+q`drnpJu?U@r_S3H#zOFrI4 zjLAeIl7T-&vf25#ZF8Ax`hJS2+JX-{jTgi{Ggry};uctY5NyNK^sW^AZfH)C~K ze#wS{!Wk>pZ?qLw%viBub=i7@e#QFf#ZmIL0}A^j6Pfkr#Mdi_axSsM+mj6GX0PXV8W#)*Qi|e=9oA=I){)~*znMOOY0TkLm7#Z z{~q2TCe#4#`-uZX^N&@doJfovM zCE;NMmP;$ZTeNdeWE6bvZC1%#rN$`;U4{MU-?gD6^G|~FOC*qpBZmljza_%8kM@RN zS@x!O*`BM*-i-Q>d*rgHjI@zP@D?oFRfu*qo~OPhkglIa745`fh=C+R6P3%~i{44r zyiK~)$VDeBxGH@is?c*Q)~$VE-P#Rh1wXw(x)h{?HwSP1%tUe2K9R~D1+Hz|W=@#%brDMp&{dk2Mff+*OTyf%f zr!ngQYLcO5;x?k5K1B12sG*7|M9)EWT2!YFv|} zc4f0|PoOLU@U!V5e$MR9c(V?G4|hJWHcO0Wymse34z*yXf2Gs zz|Xq>z7Sv)gL`&aEwnnmc+cHKY6kv>3x-b+Vz@g7Dl<*Kj$K& z%--{S#OL+a@GAGH9xA`YTDFRNydTkkNn4UOY&&I8{uBw=^B;Aspnw`GFkf@(g zw7Se%GC4}Ng7ve9lc8jL?rsH>Ur|wE$R|kz8*Q_}nLLWC(sBAIS-Df{H1NYvVlKrQ zva?Ou6&1J}i@Pnt-E^p8HJZs847#M01jI!tE0W3ibSChc%Yzy|-9z+W^|-FPJV0$F zZ0{f)w8SxBp|wBV=@^quHOZAxPW#% zef`*gJ79orKxUsrG1;$?HgJV?K=C!*=^EHVc>2A_i##RT`_;+hbgpV8(j^*@0qLVC z2m51nAiZB}Y*eXTDwnrDb$o+?C9#-%JIRKU#$#62f8}^d&ef|Rr>{h7sd*qLDGB5x zMo~@dq8d>St)`7&MTB;?PH5g6B}7CBdsW@@naM}3S^hN>dPIE&T&U+dx?ZAPUQ_Hp zUs^1zR8mrsJ~0WeRdci7*0+S37?duhNQ&OXf+Yu=ZdG6USN58rJ*}N#D%Imdwx1XnBsB97pedJNk zRqWCAFlsSRf(|6|<(Zdk%fuFtg)$z(i$;GjDk|UYWV^%J(HC}QJ_@xhddP=mtHOYZ`ajo#L_d5M?l6QQ60=w!qeDU<$0d*Nb`vkf*;yJ5W;!jXGHZ}IK8L@I61q1S&!e(+QfdlG9Zd2O&Ia><<@%mG$@79p25*Y8e&d^DY>@0F-=fx ztWs1om(x&I{x?)|g4#f*jqP%e`M70t5$7j%vqyQ!IX$L1jpQ6}RpWY_Vv|y_F>|xc zrg+gtR#t7cv6~~j!Ri|h^&l5i#sys)QIBM)4UA{Zm(ip9qsMev#};v0W}OyG;SO^4 zX{e8(TprO>@`_ExilpMr>)>ODJ+oTX5zs?N$a2%}wa~N6_|> zCtI&gMEFY+f0vAoH=6rpu~+VlOUb>Sb)H8%3NFnppJOy!J@IW`7kocAIj5c3X_{#t z!-7}^J0{nanfTAp%Va`#X%sO51_ponA$zHVF&kJTY&&EH8$3AglrM?L)fWYS@4vMF0>{1V=gq9sx^7d#kB^nxse#u7=jCp$!9FJ8Ohzed|j}s zp_)KzM*a%*I{9C433?kYbG=%ItEN^VI%D)GqEV|wPU<&M;?H&BI^X$sxO6uX!J&mV z%Ei|%R!Ks7u@L)T;POz2-YN>wXnaE6#X=m93(fVkX`zP_dT=_2!77Ssrw(IL zUM#BJXOBD78-bb}5#-mCcD#b>qhu64krtk%yU-c z)zfJ(&3#Wfg(erA74B{^3@iA~Xu-vIq2@wu1CPJEMhk9b8;#%wZEGDTJX=%Tg|v;v zcA{Cwo|WBG@VlMO98yLYC{Nz(Xo60XkBYEp(J`6|feG_<_etY9=-QJO;6EUnSVSw| zuoHm#tu(lziLn$;b z|E!=5oH||z7(ig2TRBB5_>))#P-dmlUw99OJJ0AsjD7`Kp_I#J;wh_W>-hO#tMg1b z<*Fhpsa0^(R+kI2q;V9;-3W5Cw*405UgSY;uw91CR`8tic-(v$t78q6d|BoMqA_WG ziHpKF%kj-irM==!G28&mi~)8AOfFg6BOujh0cqGK=PvBlUY6g+xR2cG&eRbN?a&Bc7a>Z-hxYI`qP=W#=(jNHN3BoNZ zY1sZG=yfAzlRtl&P~Ue2fv0{q@H3fK$06q^DjGlhy2_v5?b@SbZ?;zX3&U9b7h8_X zjW*Cg`N7>hSzNRbL8i?}*o~$r>)z0@cVhB=2>GBYPo`blPA*XbGy=M62^(xz3Vnf{ zaVN(5pjTX;%=sh>t6Y`Ff?GAU{^Wox29_^Cy`MwV5x`j67*~UuIaK7oKZ0C2gW8RT zgG8S%n~%co$Y7K`xP_rzfU^bdpkcZ00Ib-~fTKW2lz9cc3UFtJsSnCv>iaRtBybtY zjs||K2F^N>%Wk(_dtG4b=8iFUM~x!Q!Gfw5@h3{3rI~b;$jF2%?{5eTcK4s!IHAWj zXJ>c+@3#9IA3Uqseo5&G)@BZdp0_dc2F*`ipkH_;K)K|u+0b|V&4`*yIWN3Sod4SV z-zh@5Ed=_7j`GM{?6x;S|yJ%7;r$^f0W{a3=V}D-TU4)y?)gMW=t^O+w*0lq=**sJadn~hYA(^oOXC(` z#jr|6OXHWeTJazZ${CeTdBU* zHT(SwjO_NnWrsK_``b|&VBND!H229XLD)GLm47Rp?GIk9r(ZAAnv7xLR<>9+dG?=&5ReDj)x-?m48zBLY)}NYTFqx z2z}Xxg8+wvz+KGku#>&+NUsbyFplI_@<^B@2ADtMZm-~O0NDzg;uy-p+xm&DBBB#c zb4Wp{hfVC}0%2!3M2x!`1Sk#zmTM;qM+pI=_xU!6vlc{Daxlk!CIPk*Z|3B%8$`;! zY24%Il=)Ahg+RQAdZK~i$I!=6<0Sb7k(g;r%)JKK&$D6bHdhzkfWXV>jh;rLTG1U3 z6rVcN3V~Q|LZC--zVUi07idgo5Q+d_{9w&{lB0JXW-bPQksB=kAuaQ%1D`9U1uL9b zH;}NjbShlK%Eo34;3fG3J7%X_0~_NXgvM-0Z?0pYT@;*GzsrZM&wPzpX z)`u7KmWAT_!1hJvMx@D%*32g;O|Co3ATwI3vve9gl4tO8oY&y>!UxH)UJOoK8r||} zx(BkAUrLEgmyLp)<*{_-u}nowSLoVoIzt;OMh2dG2M6rl`>IIYgy1ZwNO%N|2jjoDwG$$2BKF})UEje) zN^yYP=ERkV$plXw!n!p-F19)-FbaihX5n;$MI1%!GM>XLo@yomlY)H7C|7(ctUaTH zwRco~EYp@LM<-yOjgXHArZldM3*@=hW(u+frT>I!kTqDlkaHzqEjsv!A7mhz#W38f zXEH!ut$F7tGzPHA`0Mim2V@x_bZ75pGPV%<$GDI9Wu>MAH2oU!Z3_(lvb`8*246BI zX8@|HFt0MwK-FfNe@-w7cyQZiGAGdae&viaZCv5e-4f6Bp~Jp?uMySUcrMgX{~vI{O$p0nOo_LGPVTNV9Ve1kJYD1WccSS$gk)|@%ycw` z)WcFul0&EjuF&Fb>4<2ATyXq*ohZJUWI&qeg?*l|aCDT|!=baGGQ1=>aC#_EAlZNN zbo7oL$zhYvn_W&UcflSm4@qB+Ni~$8? z6ApADZ;%YS&!Tu#H8v=zNaJn#|`~z@u zyyWCzI}gkPKmwcNwhT@~-;uDY@5;LY{se(e;~A#v+6e*VFOZj@TKGW;&dJbcO>Fn~ zW_A9h#9vB{uPS|wKY!+H-2TX+S#%wu@aKp0N^kyjg&6fF+9e8!$ifloS2aNX;K2J@nVp@+EM6xdZH{g;~J3Y6^k^{FZV8z8pnTyB-4sG zh>0%OLsP>_x7Jh5WD3&wrIBo(WZj%EouBk zO)#pEL!^eJqW@(gQ?%4x7nT`&btWu>__DGHg+Io_xTf^+FfRE;&czMj++K*0iK&@n zS&f4lgP%PXFD>RsW|1y*Cxsc7@fXR_RVOmsO<*|kE4Ty!48~QJiwx(g#?PFOKdT)# z+V||A_uv`-_%qKq&iCvderA09nLG}j(HV3P&gc&ccl@{ocyA>D)LS+CKg4yHT!mpu zRpYvAiT3X@)(%|{8L3wZ2WHFcD*K1X;%|n{-`o{>U)mA1lO66Au;0zFZyL1>>h%LU zn{0WN=+)yPwjX7k!cN%rn&uDD*{D&Ifo`Z+*-9L0*8z1|13p?I?eFHaTj7xSXZwkv z+$JTq9B8P4nxj?on-5X^T_a3FXIR`gA|I3E{63(21?0h@iMX(s!nP3J5DjDt3xO4k zb*mDD!FpF3q`mxZw-HlZSbZ-jF>&Eu*sCp(D&8X?lz^?xiOV3HCnSSX?}1X)0hf!> zD2K$S%J@fhT9#F-;yKxW;oy+xcOU`p=`JMF>N_L*C15m z$h?+$D*m)J(2kji2P<$vRTH+OPhv#AE@mbaDZiy_fOuVzNEAon~oKmA=aY|s7^FGB^PT?j0<@F5k% zDWy!?9p_7oizZ2|SoE66qS>GOh{Cz-3>)kymG?}>}G>yEd%uQ3e-fLduBdA}cO7yiGvx$`JJqMrv$6S0EkCC{AH#?*>e7Ts0 zci^mO#FvJ*xg$GeMgkVL-&pPkVT%J~JgQ8?ASe~v&x8rLYS}#;ii7_N;_@>CGQ*5X zR@59U0MvQ%Oc;6&g6bf(Z7PoKaF~P7K7_yqz|fSovM$8M;+(}zZJmlVu-(5_jd}*+ zbj@mCoDOF&n4MqL5_|?u0%}y6XOJFX*U#Jha8ViswoEi-espnJI@7OskVo6s$LB7A zV(Lnz9ts~Rp&lb9)K@G7ZCbd@5}my8%s69eLU!$yOlj28WlH$6aI#czT`ryBYm~*; zu8%)?oN;lY<6u53i_m!Z1b@%Q|0zPOapW`Gp$UFn1IKy1nU(zd%l(*`#Z0)*=hw#S zh^vI?*K_vE_e zE=UEzQh7L@7r(45{6-F+4{(5Uc@O0LX{nlw$xY_fO~%EVr-C)6jZLX3O(5uDeI}pD zVI)1&T}saj#q`|t8*ITrxZuibZ^Qu!6Q`!&l{dl}#uHP*P$aDJh4RBVAG-vt(!(e# z71*(iUP3_b*#JEg_s+z@!zg2SCl(eqPIrdp!WsWjFym$716IVEZTa znSR1_(BP#K5LlJg3*EkoJRsv%+K_AX=rcG4`wD*aEremnF8ag;!(0L=o(RK)R8jf} z4C7q~WyUeEom_(C78mRgWY@t2PvV|#EOtLr3!WgT2kLK<)EC?^2f)C}9FU1HK$Bs; zidJGA>}>I!eVlzjIvw{gg~4gahEk)CQ%a?ykm&BEkCM602p^el@TGB6B*Z^c8t*%F zD4qUbGlaPdIjJ39ruTI#OYn6oOZ0UsOZN3y`-HDg5U45QvK2o64VO*E;HK2c8dHiU zZE;h2YLj`RCS$b*K>L5fW%rTCad}BQEbXbc=Lh+4Ic0v3h|9(0FZyt~xb#H{muu)d zxF*853?b)8xI9RS-2j)14_1$T9G8n#Fbw1Jor^eo$GF^fkrZ*6w{NTumw9`~O1O*! zff6p;J;oprm)64|P{L*2YA0;&N4U(hkCkxwwx|)tW$PUz;_{haD}1;N|FuHIW#>5~ zHV)%*y1thbak;z%1WLHP961c7?;~7Zb}B?%x~7O4tvxHa;^v@YT#bD87XqO6612|# zg%Cm64g$eAWQS}g7W+i(Ci%n)8;HmAV8wligUwC{7#xSDj z{|S%3dkl}5zs*gic}*ERALZlnnZpy6YX%lFeFJ;hHUfT{_3@*nHd6elM*NkgjTmI? z!En@rf6;j90FIxhappbpH@Lu0E=Qg2agb+rr%4^&!W}w((xG4MP~+>+iaWgflMaq9 zEFsm`p#^t1@RJTb&>;b5c#D68+z<$9;dcrYfy49Lb5R^rt!C3d38Nn{&l~?8gaU8| zSo|vLV_eY4dKHpy4QluM1a4--x4|RO82>8#UpC0H|%D&a2{4oO1KuNntz?S@P%OkOqo_t_we+HhkXQ)$$|K>f(@-#%yidKNtN~ zSp|(VhIg%aRFgPVAraF2os;@)w+e#-vCV4g+lD+Fv z()d|9-+}ARv5MS(K;isDIe!A*vWiN4Ta*JmM=H(B7xgVWXG__62C|gCdYmivs|lJc zo8$S$`~=J@aj+3SA8;^~q;Ou#JjS)Ey=-v=U|jr75-#@OG@XcA{$-3g0b@?^!P@%L zA*iS19_cndKBpVgj%R3*rv&7f; Date: Mon, 19 Jul 2021 13:39:07 -0700 Subject: [PATCH 15/17] update crucible to ignore old dbg metadata --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index f2abe5388c..708719b32c 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit f2abe5388cee9f717af7a1dccf956a6896b47c51 +Subproject commit 708719b32c43a2dfd63a5b357d96676fda7ba4d8 From 14c2f75d9a296898aa21cab40eee05dd7f1d099a Mon Sep 17 00:00:00 2001 From: Chris Phifer Date: Tue, 20 Jul 2021 18:55:41 -0500 Subject: [PATCH 16/17] Implement a command to introduce new SAWCore primitives via Heapster (#1384) The CI failures here are a known issue with the build system, and have nothing to do with this PR. --- src/SAWScript/HeapsterBuiltins.hs | 48 +++++++++++++++++++++++++++++++ src/SAWScript/Interpreter.hs | 9 ++++++ 2 files changed, 57 insertions(+) diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs index ff2491c915..1900049dd8 100644 --- a/src/SAWScript/HeapsterBuiltins.hs +++ b/src/SAWScript/HeapsterBuiltins.hs @@ -40,6 +40,7 @@ module SAWScript.HeapsterBuiltins , heapster_find_trait_method_symbol , heapster_assume_fun , heapster_assume_fun_rename + , heapster_assume_fun_rename_prim , heapster_assume_fun_multi , heapster_print_fun_trans , heapster_export_coq @@ -869,6 +870,53 @@ heapster_assume_fun_rename _bic _opts henv nm nm_to perms_string term_string = (globalOpenTerm term_ident) liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'' +-- | Create a new SAW core primitive named @nm@ with type @tp@ in the module +-- associated with the supplied Heapster environment, and return its identifier +insPrimitive :: HeapsterEnv -> String -> Term -> TopLevel Ident +insPrimitive henv nm tp = + do sc <- getSharedContext + let mnm = heapsterEnvSAWModule henv + let ident = mkSafeIdent mnm nm + i <- liftIO $ scFreshGlobalVar sc + liftIO $ scRegisterName sc i (ModuleIdentifier ident) + let pn = PrimName i ident tp + t <- liftIO $ scFlatTermF sc (Primitive pn) + liftIO $ scRegisterGlobal sc ident t + liftIO $ scModifyModule sc mnm $ \m -> + insDef m $ Def { defIdent = ident, + defQualifier = PrimQualifier, + defType = tp, + defBody = Nothing } + return ident + +-- | Assume that the given named function has the supplied type and translates +-- to a SAW core definition given by the second name +heapster_assume_fun_rename_prim :: BuiltinContext -> Options -> HeapsterEnv -> + String -> String -> String -> TopLevel () +heapster_assume_fun_rename_prim _bic _opts henv nm nm_to perms_string = + do Some lm <- failOnNothing ("Could not find symbol: " ++ nm) + (lookupModContainingSym henv nm) + sc <- getSharedContext + let w = llvmModuleArchReprWidth lm + leq_proof <- case decideLeq (knownNat @1) w of + Left pf -> return pf + Right _ -> fail "LLVM arch width is 0!" + env <- liftIO $ readIORef $ heapsterEnvPermEnvRef henv + (Some cargs, Some ret) <- lookupFunctionType lm nm + let args = mkCruCtx cargs + withKnownNat w $ withLeqProof leq_proof $ do + SomeFunPerm fun_perm <- + parseFunPermStringMaybeRust "permissions" w env args ret perms_string + env' <- liftIO $ readIORef (heapsterEnvPermEnvRef henv) + fun_typ <- liftIO $ translateCompleteFunPerm sc env fun_perm + term_ident <- insPrimitive henv nm_to fun_typ + let env'' = permEnvAddGlobalSymFun env' + (GlobalSymbol $ fromString nm) + w + fun_perm + (globalOpenTerm term_ident) + liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'' + -- | Assume that the given named function has the supplied type and translates -- to a SAW core definition given by name heapster_assume_fun :: BuiltinContext -> Options -> HeapsterEnv -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index fc2b49e190..aa0b8de25d 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3187,6 +3187,15 @@ primitives = Map.fromList , " trans is not an identifier then it is bound to the defined name nm_to." ] + , prim "heapster_assume_fun_rename_prim" + "HeapsterEnv -> String -> String -> String -> TopLevel HeapsterEnv" + (bicVal heapster_assume_fun_rename_prim) + Experimental + [ + "heapster_assume_fun_rename_prim nm nm_to perms assumes that function nm" + , " has permissions perms as a primitive." + ] + , prim "heapster_assume_fun_multi" "HeapsterEnv -> String -> [(String, String)] -> TopLevel HeapsterEnv" (bicVal heapster_assume_fun_multi) From d2b99cae4525f87af759c69dbe7ff00b15dfd78b Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Wed, 21 Jul 2021 15:26:49 -0700 Subject: [PATCH 17/17] heapster-saw: Use LLVM debug information to choose permission variable names (#1385) heapster-saw: Initial debug names propagated into heapster permissions --- heapster-saw/heapster-saw.cabal | 1 + .../Verifier/SAW/Heapster/NamePropagation.hs | 65 +++ .../Verifier/SAW/Heapster/TypedCrucible.hs | 492 ++++++++++++------ 3 files changed, 398 insertions(+), 160 deletions(-) create mode 100644 heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs diff --git a/heapster-saw/heapster-saw.cabal b/heapster-saw/heapster-saw.cabal index 7c904aa5ff..c8d2a8c1cf 100644 --- a/heapster-saw/heapster-saw.cabal +++ b/heapster-saw/heapster-saw.cabal @@ -52,6 +52,7 @@ library Verifier.SAW.Heapster.Parser Verifier.SAW.Heapster.Permissions Verifier.SAW.Heapster.PermParser + Verifier.SAW.Heapster.NamePropagation Verifier.SAW.Heapster.RustTypes Verifier.SAW.Heapster.SAWTranslation Verifier.SAW.Heapster.Token diff --git a/heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs b/heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs new file mode 100644 index 0000000000..5fd0d662a2 --- /dev/null +++ b/heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs @@ -0,0 +1,65 @@ +{-# Language ScopedTypeVariables #-} +{-# Language GADTs #-} +module Verifier.SAW.Heapster.NamePropagation where + +import Data.Functor.Constant +import Data.Parameterized.TraversableFC ( FoldableFC(toListFC), FunctorFC(fmapFC) ) +import Lang.Crucible.Analysis.Fixpoint +import Lang.Crucible.CFG.Core ( Some(Some), CFG(cfgHandle) ) +import Lang.Crucible.FunctionHandle ( FnHandle(handleArgTypes) ) +import Lang.Crucible.LLVM.Extension ( LLVM, LLVMStmt(..), LLVM_Dbg(..) ) +import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.Map as PM +import qualified Text.LLVM.AST as L + +type NameDom = Pointed (Constant String) + +nameJoin :: Constant String a -> Constant String a -> NameDom a +nameJoin (Constant x) (Constant y) | x == y = Pointed (Constant x) +nameJoin _ _ = Top + +nameDomain :: Domain (Pointed (Constant String)) +nameDomain = pointed nameJoin (==) WTO + +nameInterpretation :: Interpretation LLVM NameDom +nameInterpretation = Interpretation + { interpExpr = \_ _ _ names -> (Just names, Bottom) + , interpCall = \_ _ _ _ _ names -> (Just names, Bottom) + , interpReadGlobal = \_ names -> (Just names, Bottom) + , interpWriteGlobal = \_ _ names -> Just names + , interpBr = \_ _ _ _ names -> (Just names, Just names) + , interpMaybe = \_ _ _ names -> (Just names, Bottom, Just names) + , interpExt = \_ stmt names -> + let names' = + case stmt of + LLVM_Debug (LLVM_Dbg_Declare ptr di _) | Just n <- L.dilvName di -> + modifyAbstractRegValue names ptr (\_ -> Pointed (Constant ("&" ++ n))) + LLVM_Debug (LLVM_Dbg_Addr ptr di _) | Just n <- L.dilvName di -> + modifyAbstractRegValue names ptr (\_ -> Pointed (Constant ("&" ++ n))) + LLVM_Debug (LLVM_Dbg_Value _ val di _) | Just n <- L.dilvName di -> + modifyAbstractRegValue names val (\_ -> Pointed (Constant n)) + _ -> names + in (Just names', Bottom) + } + +computeNames :: + forall blocks init ret. + CFG LLVM blocks init ret -> + Ctx.Assignment (Constant [Maybe String]) blocks +computeNames cfg = + case alg of + (_, end, _) -> fmapFC (\(Ignore (Some p)) -> Constant (toListFC flatten (_paRegisters p))) end + where + flatten :: NameDom a -> Maybe String + flatten Top = Nothing + flatten Bottom = Nothing + flatten (Pointed (Constant x)) = Just x + + sz = Ctx.size (handleArgTypes (cfgHandle cfg)) + alg = + forwardFixpoint' + nameDomain + nameInterpretation + cfg + PM.empty + (Ctx.replicate sz Bottom) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index 6eb98d5af4..3a48529668 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -77,6 +77,7 @@ import Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB import Verifier.SAW.Heapster.CruUtil import Verifier.SAW.Heapster.GenMonad import Verifier.SAW.Heapster.Implication +import Verifier.SAW.Heapster.NamePropagation import Verifier.SAW.Heapster.Permissions import Verifier.SAW.Heapster.Widening @@ -939,7 +940,6 @@ instance SubstVar PermVarSubst m => [nuMP| TypedLLVMIte w r1 r2 r3 |] -> TypedLLVMIte (mbLift w) <$> genSubst s r1 <*> genSubst s r2 <*> genSubst s r3 - instance (PermCheckExtC ext, SubstVar PermVarSubst m) => Substable PermVarSubst (TypedStmt ext rets ps_in ps_out) m where genSubst s mb_x = case mbMatch mb_x of @@ -1268,7 +1268,9 @@ data TypedBlock phase ext (blocks :: RList (RList CrucibleType)) tops ret args = -- disallowed for user-supplied permissions typedBlockCanWiden :: Bool, -- | The entrypoints into this block - _typedBlockEntries :: [Some (TypedEntry phase ext blocks tops ret args)] + _typedBlockEntries :: [Some (TypedEntry phase ext blocks tops ret args)], + -- | Debug name information for the current block + _typedBlockNames :: [Maybe String] } makeLenses ''TypedBlock @@ -1312,34 +1314,40 @@ entryByID entryID = -- | Build an empty 'TypedBlock' -emptyBlockOfSort :: Assignment CtxRepr cblocks -> TypedBlockSort -> - Block ext cblocks ret cargs -> - TypedBlock TCPhase ext (CtxCtxToRList - cblocks) tops ret (CtxToRList cargs) -emptyBlockOfSort cblocks sort blk +emptyBlockOfSort :: + [Maybe String] -> + Assignment CtxRepr cblocks -> + TypedBlockSort -> + Block ext cblocks ret cargs -> + TypedBlock TCPhase ext (CtxCtxToRList + cblocks) tops ret (CtxToRList cargs) +emptyBlockOfSort names cblocks sort blk | Refl <- reprReprToCruCtxCtxEq cblocks = TypedBlock (indexCtxToMember (size cblocks) $ - blockIDIndex $ blockID blk) blk sort True [] + blockIDIndex $ blockID blk) blk sort True [] names -- | Build a block with a user-supplied input permission -emptyBlockForPerms :: Assignment CtxRepr cblocks -> - Block ext cblocks ret cargs -> CruCtx tops -> - TypeRepr ret -> CruCtx ghosts -> - MbValuePerms ((tops :++: CtxToRList cargs) :++: ghosts) -> - MbValuePerms (tops :> ret) -> - TypedBlock TCPhase ext (CtxCtxToRList - cblocks) tops ret (CtxToRList cargs) -emptyBlockForPerms cblocks blk tops ret ghosts perms_in perms_out +emptyBlockForPerms :: + [Maybe String] -> + Assignment CtxRepr cblocks -> + Block ext cblocks ret cargs -> CruCtx tops -> + TypeRepr ret -> CruCtx ghosts -> + MbValuePerms ((tops :++: CtxToRList cargs) :++: ghosts) -> + MbValuePerms (tops :> ret) -> + TypedBlock TCPhase ext (CtxCtxToRList + cblocks) tops ret (CtxToRList cargs) +emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out | Refl <- reprReprToCruCtxCtxEq cblocks , blockID <- indexCtxToMember (size cblocks) $ blockIDIndex $ blockID blk , args <- mkCruCtx (blockInputs blk) = TypedBlock blockID blk JoinSort False - [Some $ TypedEntry { + [Some TypedEntry { typedEntryID = TypedEntryID blockID 0, typedEntryTops = tops, typedEntryArgs = args, typedEntryRet = ret, typedEntryCallers = [], typedEntryGhosts = ghosts, typedEntryPermsIn = perms_in, typedEntryPermsOut = perms_out, typedEntryBody = Nothing }] + names -- | Transition a 'TypedBlock' from type-checking to translation phase, by -- making sure that all of data needed for the translation phase is present @@ -1548,6 +1556,7 @@ funPermToBlockInputs fun_perm = -- supplied 'PermEnv' along with a list of 'Bool' flags indicating which blocks -- are at the head of a loop (or other strongly-connected component) initTypedBlockMap :: + KnownRepr ExtRepr ext => PermEnv -> FunPerm ghosts (CtxToRList init) ret -> CFG ext cblocks init ret -> @@ -1557,26 +1566,34 @@ initTypedBlockMap :: initTypedBlockMap env fun_perm cfg sccs = let block_map = cfgBlockMap cfg cblocks = fmapFC blockInputs block_map + namess = computeCfgNames knownRepr (size sccs) cfg ret = funPermRet fun_perm tops = funPermTops fun_perm top_perms_in = funPermToBlockInputs fun_perm perms_out = funPermOuts fun_perm in assignToRListRList - (\(Pair blk (Constant is_scc)) -> + (\(Pair blk (Pair (Constant is_scc) (Constant names))) -> let blkID = blockID blk hints = lookupBlockHints env (cfgHandle cfg) cblocks blkID in case hints of _ | Just Refl <- testEquality (cfgEntryBlockID cfg) blkID -> - emptyBlockForPerms cblocks blk tops ret CruCtxNil top_perms_in perms_out + emptyBlockForPerms names cblocks blk tops ret CruCtxNil top_perms_in perms_out (find isBlockEntryHint -> Just (BlockEntryHintSort tops' ghosts perms_in)) | Just Refl <- testEquality tops tops' -> - emptyBlockForPerms cblocks blk tops ret ghosts perms_in perms_out + emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out _ | is_scc || any isJoinPointHint hints -> - emptyBlockOfSort cblocks JoinSort blk - _ -> emptyBlockOfSort cblocks MultiEntrySort blk) $ - Ctx.zipWith Pair block_map sccs + emptyBlockOfSort names cblocks JoinSort blk + _ -> emptyBlockOfSort names cblocks MultiEntrySort blk) $ + Ctx.zipWith Pair block_map (Ctx.zipWith Pair sccs namess) +computeCfgNames :: + ExtRepr ext -> + Size cblocks -> + CFG ext cblocks init ret -> + Ctx.Assignment (Constant [Maybe String]) cblocks +computeCfgNames ExtRepr_LLVM _ cfg = computeNames cfg +computeCfgNames ExtRepr_Unit s _ = Ctx.replicate s (Constant []) -- | A typed Crucible CFG data TypedCFG @@ -1675,6 +1692,7 @@ makeLenses ''TopPermCheckState -- | Build an empty 'TopPermCheckState' from a Crucible 'BlockMap' emptyTopPermCheckState :: HasPtrWidth w => + KnownRepr ExtRepr ext => PermEnv -> FunPerm ghosts (CtxToRList init) ret -> EndianForm -> @@ -1788,21 +1806,27 @@ data PermCheckState ext blocks tops ret ps = stCurEntry :: !(Some (TypedEntryID blocks)), stVarTypes :: !(NameMap TypeRepr), stPPInfo :: !PPInfo, - stErrPrefix :: !(Maybe (Doc ())) + stErrPrefix :: !(Maybe (Doc ())), + stDebug :: ![Maybe String] } -- | Build a default, empty 'PermCheckState' -emptyPermCheckState :: KnownRepr ExtRepr ext => PermSet ps -> - RAssign ExprVar tops -> TypedEntryID blocks args -> - PermCheckState ext blocks tops ret ps -emptyPermCheckState perms tops entryID = +emptyPermCheckState :: + KnownRepr ExtRepr ext => + PermSet ps -> + RAssign ExprVar tops -> + TypedEntryID blocks args -> + [Maybe String] -> + PermCheckState ext blocks tops ret ps +emptyPermCheckState perms tops entryID names = PermCheckState { stCurPerms = perms, stExtState = emptyPermCheckExtState knownRepr, stTopVars = tops, stCurEntry = Some entryID, stVarTypes = NameMap.empty, stPPInfo = emptyPPInfo, - stErrPrefix = Nothing } + stErrPrefix = Nothing, + stDebug = names } -- | Like the 'set' method of a lens, but allows the @ps@ argument to change setSTCurPerms :: PermSet ps2 -> PermCheckState ext blocks tops ret ps1 -> @@ -1815,6 +1839,13 @@ modifySTCurPerms :: (PermSet ps1 -> PermSet ps2) -> PermCheckState ext blocks tops ret ps2 modifySTCurPerms f_perms st = setSTCurPerms (f_perms $ stCurPerms st) st +nextDebugName :: + PermCheckM ext cblocks blocks tops ret a ps a ps + (Maybe String) +nextDebugName = + do st <- get + put st { stDebug = drop 1 (stDebug st)} + pure (foldr (\x _ -> x) Nothing (stDebug st)) -- | The generalized monad for permission-checking type PermCheckM ext cblocks blocks tops ret r1 ps1 r2 ps2 = @@ -1870,14 +1901,16 @@ setInputExtState ExtRepr_LLVM _ _ = -- of top-level arguments, local arguments, ghost variables, and permissions on -- all three, and return a result inside a binding for these variables runPermCheckM :: - KnownRepr ExtRepr ext => TypedEntryID blocks some_args -> + KnownRepr ExtRepr ext => + [Maybe String] -> + TypedEntryID blocks some_args -> CruCtx args -> CruCtx ghosts -> MbValuePerms ((tops :++: args) :++: ghosts) -> (RAssign ExprVar tops -> RAssign ExprVar args -> RAssign ExprVar ghosts -> DistPerms ((tops :++: args) :++: ghosts) -> PermCheckM ext cblocks blocks tops ret () ps_out r ((tops :++: args) :++: ghosts) ()) -> TopPermCheckM ext cblocks blocks tops ret (Mb ((tops :++: args) :++: ghosts) r) -runPermCheckM entryID args ghosts mb_perms_in m = +runPermCheckM names entryID args ghosts mb_perms_in m = get >>= \(TopPermCheckState {..}) -> let args_prxs = cruCtxProxies args ghosts_prxs = cruCtxProxies ghosts in @@ -1885,16 +1918,66 @@ runPermCheckM entryID args ghosts mb_perms_in m = flip nuMultiWithElim1 (mbValuePermsToDistPerms mb_perms_in) $ \ns perms_in -> let (tops_args, ghosts_ns) = RL.split Proxy ghosts_prxs ns (tops_ns, args_ns) = RL.split Proxy args_prxs tops_args - st = emptyPermCheckState (distPermSet perms_in) tops_ns entryID in + (arg_names, local_names) = initialNames args names + st = emptyPermCheckState (distPermSet perms_in) tops_ns entryID local_names in let go x = runGenStateContT x st (\_ () -> pure ()) in go $ - setVarTypes "top" tops_ns stTopCtx >>> - setVarTypes "local" args_ns args >>> - setVarTypes "ghost" ghosts_ns ghosts >>> + setVarTypes "top" (noNames' stTopCtx) tops_ns stTopCtx >>> + setVarTypes "local" arg_names args_ns args >>> + setVarTypes "ghost" (noNames' ghosts) ghosts_ns ghosts >>> setInputExtState knownRepr ghosts ghosts_ns >>> m tops_ns args_ns ghosts_ns perms_in +rassignLen :: RAssign f x -> Int +rassignLen = go 0 + where + go :: Int -> RAssign f x -> Int + go acc MNil = acc + go acc (xs :>: _) = (go $! (acc+1)) xs + +initialNames :: + CruCtx tps -> + [Maybe String] -> + (RAssign (Constant (Maybe String)) tps, [Maybe String]) +initialNames CruCtxNil xs = (MNil, xs) +initialNames (CruCtxCons ts _) xs = + case initialNames ts xs of + (ys, z:zs) -> (ys :>: Constant z, zs) + (ys, [] ) -> (ys :>: Constant Nothing, []) + +-- | Compute an empty debug name assignment from a known context +noNames :: + KnownRepr CruCtx tps => + RAssign (Constant (Maybe String)) tps +noNames = noNames' knownRepr + +-- | Compute an empty debug name assignment from a given context +noNames' :: + CruCtx tps -> + RAssign (Constant (Maybe String)) tps +noNames' CruCtxNil = MNil +noNames' (CruCtxCons xs _) = noNames' xs :>: Constant Nothing + +-- | Call 'debugNames'' with a known type list. +dbgNames :: + KnownRepr CruCtx tps => + PermCheckM ext cblocks blocks tops ret a ps a ps + (RAssign (Constant (Maybe String)) tps) +dbgNames = dbgNames' knownRepr + +-- | Pop as many local variable names from the debug information +-- as needed to populate the given type list. +dbgNames' :: + CruCtx tps -> + PermCheckM ext cblocks blocks tops ret a ps a ps + (RAssign (Constant (Maybe String)) tps) +dbgNames' CruCtxNil = pure MNil +dbgNames' (CruCtxCons ts _) = + do ns <- dbgNames' ts + n <- nextDebugName + pure (ns :>: Constant n) + -- | Emit a 'TypedBlockMapDelta', which must be 'Closed', in an -- 'InnerPermCheckM' computation innerEmitDelta :: Closed (TypedBlockMapDelta blocks tops ret) -> @@ -2093,20 +2176,34 @@ getVarTypes MNil = pure CruCtxNil getVarTypes (xs :>: x) = CruCtxCons <$> getVarTypes xs <*> getVarType x -- | Remember the type of a free variable, and ensure that it has a permission -setVarType :: String -> ExprVar a -> TypeRepr a -> - PermCheckM ext cblocks blocks tops ret r ps r ps () -setVarType str x tp = +setVarType :: + String -> + Maybe String -> + ExprVar a -> + TypeRepr a -> + PermCheckM ext cblocks blocks tops ret r ps r ps () +setVarType str dbg x tp = + let str' = + case dbg of + Nothing -> str + Just d -> "C[" ++ d ++ "]" + in modify $ \st -> st { stCurPerms = initVarPerm x (stCurPerms st), stVarTypes = NameMap.insert x tp (stVarTypes st), - stPPInfo = ppInfoAddExprName str x (stPPInfo st) } + stPPInfo = ppInfoAddExprName str' x (stPPInfo st) } -- | Remember the types of a sequence of free variables -setVarTypes :: String -> RAssign Name tps -> CruCtx tps -> - PermCheckM ext cblocks blocks tops ret r ps r ps () -setVarTypes _ _ CruCtxNil = pure () -setVarTypes str (xs :>: x) (CruCtxCons tps tp) = - setVarTypes str xs tps >>> setVarType str x tp +setVarTypes :: + String -> + RAssign (Constant (Maybe String)) tps -> + RAssign Name tps -> + CruCtx tps -> + PermCheckM ext cblocks blocks tops ret r ps r ps () +setVarTypes _ MNil MNil CruCtxNil = pure () +setVarTypes str (ds :>: Constant d) (ns :>: n) (CruCtxCons ts t) = + do setVarTypes str ds ns ts + setVarType str d n t -- | Get the current 'PPInfo' permGetPPInfo :: PermCheckM ext cblocks blocks tops ret r ps r ps PPInfo @@ -2330,9 +2427,10 @@ convertRegType _ loc reg (BVRepr w1) tp2@(BVRepr w2) | Left LeqProof <- decideLeq (knownNat :: NatRepr 1) w2 , NatCaseGT LeqProof <- testNatCases w1 w2 = withKnownNat w2 $ - emitStmt knownRepr loc (TypedSetReg tp2 $ - TypedExpr (BVTrunc w2 w1 $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg tp2 $ + TypedExpr (BVTrunc w2 w1 $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType _ loc reg (BVRepr w1) tp2@(BVRepr w2) @@ -2342,9 +2440,10 @@ convertRegType _ loc reg (BVRepr w1) tp2@(BVRepr w2) -- FIXME: should this use endianness? -- (stEndianness <$> top_get) >>>= \endianness -> withKnownNat w2 $ - emitStmt knownRepr loc (TypedSetReg tp2 $ - TypedExpr (BVSext w2 w1 $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg tp2 $ + TypedExpr (BVSext w2 w1 $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType ExtRepr_LLVM loc reg (LLVMPointerRepr w1) (BVRepr w2) @@ -2352,7 +2451,7 @@ convertRegType ExtRepr_LLVM loc reg (LLVMPointerRepr w1) (BVRepr w2) withKnownNat w1 $ stmtProvePerm reg (llvmExEqWord w1) >>>= \sbst -> let e = substLookup sbst Member_Base in - emitLLVMStmt knownRepr loc (DestructLLVMWord reg e) >>>= \x -> + emitLLVMStmt knownRepr Nothing loc (DestructLLVMWord reg e) >>>= \x -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType ext loc reg (LLVMPointerRepr w1) (BVRepr w2) = @@ -2361,7 +2460,7 @@ convertRegType ext loc reg (LLVMPointerRepr w1) (BVRepr w2) = convertRegType ExtRepr_LLVM loc reg (BVRepr w2) (LLVMPointerRepr w1) | Just Refl <- testEquality w1 w2 = withKnownNat w1 $ - emitLLVMStmt knownRepr loc (ConstructLLVMWord reg) >>>= \x -> + emitLLVMStmt knownRepr Nothing loc (ConstructLLVMWord reg) >>>= \x -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType ext loc reg (BVRepr w1) (LLVMPointerRepr w2) = convertRegType ext loc reg (BVRepr w1) (BVRepr w2) >>>= \reg' -> @@ -2393,9 +2492,10 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = | Just (Some off) <- someNat (bytesToBits off_bytes) , Left off_sz_w_pf <- decideLeq (addNat off sz) w -> withLeqProof sz_pf $ withLeqProof off_sz_w_pf $ - emitStmt knownRepr loc (TypedSetReg (BVRepr sz) $ - TypedExpr (BVSelect off sz w $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg (BVRepr sz) $ + TypedExpr (BVSelect off sz w $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) @@ -2406,9 +2506,10 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = - intValue sz) , Left idx_sz_w_pf <- decideLeq (addNat idx sz) w -> withLeqProof sz_pf $ withLeqProof idx_sz_w_pf $ - emitStmt knownRepr loc (TypedSetReg (BVRepr sz) $ - TypedExpr (BVSelect idx sz w $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg (BVRepr sz) $ + TypedExpr (BVSelect idx sz w $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) _ -> error "extractBVBytes: negative offset!" @@ -2418,26 +2519,32 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = -- function says how that statement modifies the current permissions, given the -- freshly-bound names for the return values. Return those freshly-bound names -- for the return values. -emitStmt :: CruCtx rets -> ProgramLoc -> - TypedStmt ext rets ps_in ps_out -> - StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in - (RAssign Name rets) -emitStmt tps loc stmt = +emitStmt :: + CruCtx rets -> + RAssign (Constant (Maybe String)) rets -> + ProgramLoc -> + TypedStmt ext rets ps_in ps_out -> + StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in + (RAssign Name rets) +emitStmt tps names loc stmt = gopenBinding ((TypedConsStmt loc stmt (cruCtxProxies tps) <$>) . strongMbM) (mbPure (cruCtxProxies tps) ()) >>>= \(ns, ()) -> - setVarTypes "x" ns tps >>> + setVarTypes "x" names ns tps >>> gmodify (modifySTCurPerms (applyTypedStmt stmt ns)) >>> pure ns -- | Call emitStmt with a 'TypedLLVMStmt' -emitLLVMStmt :: TypeRepr tp -> ProgramLoc -> +emitLLVMStmt :: + TypeRepr tp -> + Maybe String -> + ProgramLoc -> TypedLLVMStmt tp ps_in ps_out -> StmtPermCheckM LLVM cblocks blocks tops ret ps_out ps_in (Name tp) -emitLLVMStmt tp loc stmt = - RL.head <$> emitStmt (singletonCruCtx tp) loc (TypedLLVMStmt stmt) +emitLLVMStmt tp name loc stmt = + RL.head <$> emitStmt (singletonCruCtx tp) (RL.singleton (Constant name)) loc (TypedLLVMStmt stmt) -- | A program location for code which was generated by the type-checker checkerProgramLoc :: ProgramLoc @@ -2513,17 +2620,23 @@ getRelevantPerms (namesListToNames -> SomeRAssign ns) = -- to, and then pretty-print the permissions on those variables and all -- variables they contain, as well as the top-level input variables and the -- extension-specific variables -ppCruRegsAndTopsPerms :: CtxTrans ctx -> [Some (Reg ctx)] -> - PermCheckM ext cblocks blocks tops ret r ps r ps (Doc (), Doc ()) -ppCruRegsAndTopsPerms ctx regs = +ppCruRegsAndTopsPerms :: + [Maybe String] -> + CtxTrans ctx -> + [Some (Reg ctx)] -> + PermCheckM ext cblocks blocks tops ret r ps r ps (Doc (), Doc ()) +ppCruRegsAndTopsPerms names ctx regs = permGetPPInfo >>>= \ppInfo -> gets stTopVars >>>= \tops -> gets (permCheckExtStateNames . stExtState) >>>= \(Some ext_ns) -> let vars_pp = fillSep $ punctuate comma $ - map (\case Some r -> - pretty r <+> pretty '=' <+> - permPretty ppInfo (tcReg ctx r)) regs + map (\(Some r) -> + let name = listToMaybe (drop (indexVal (regIndex r)) names) in + pretty r <+> pretty '=' <+> + permPretty ppInfo (tcReg ctx r) <> + foldMap (\n -> pretty " @" <+> pretty n) name) + (nub regs) vars = namesToNamesList tops ++ namesToNamesList ext_ns ++ map (\(Some r) -> SomeName $ typedRegVar $ tcReg ctx r) regs in @@ -2532,10 +2645,15 @@ ppCruRegsAndTopsPerms ctx regs = Some perms -> pure (vars_pp, permPretty ppInfo perms) -- | Set the current prefix string to give context to error messages -setErrorPrefix :: ProgramLoc -> Doc () -> CtxTrans ctx -> [Some (Reg ctx)] -> - PermCheckM ext cblocks blocks tops ret r ps r ps () -setErrorPrefix loc stmt_pp ctx regs = - ppCruRegsAndTopsPerms ctx regs >>>= \(regs_pp, perms_pp) -> +setErrorPrefix :: + [Maybe String] -> + ProgramLoc -> + Doc () -> + CtxTrans ctx -> + [Some (Reg ctx)] -> + PermCheckM ext cblocks blocks tops ret r ps r ps () +setErrorPrefix names loc stmt_pp ctx regs = + ppCruRegsAndTopsPerms names ctx regs >>>= \(regs_pp, perms_pp) -> let prefix = PP.sep [PP.group (pretty "At" <+> ppShortFileName (plSourceLoc loc) @@ -2787,7 +2905,9 @@ tcEmitStmt' ctx loc (SetReg tp (App e)) = traverseFC (tcRegWithVal ctx) e >>= \e_with_vals -> tcExpr e_with_vals >>= \maybe_val -> let typed_e = TypedExpr e_with_vals maybe_val in - emitStmt (singletonCruCtx tp) loc (TypedSetReg tp typed_e) >>>= \(_ :>: x) -> + let rets = (singletonCruCtx tp) in + dbgNames' rets >>= \names -> + emitStmt rets names loc (TypedSetReg tp typed_e) >>>= \(_ :>: x) -> stmtRecombinePerms >>> pure (addCtxName ctx x) @@ -2827,9 +2947,11 @@ tcEmitStmt' ctx loc (CallHandle ret freg_untyped _args_ctx args_untyped) = stmtProvePermsAppend CruCtxNil (emptyMb $ eqDistPerms ghosts_ns gexprs) >>>= \_ -> stmtProvePerm freg (emptyMb $ ValPerm_Conj1 $ Perm_Fun fun_perm) >>>= \_ -> - (emitStmt (singletonCruCtx ret) loc - (TypedCall freg fun_perm (varsToTypedRegs - ghosts_ns) gexprs args)) >>>= \(_ :>: ret') -> + let rets = singletonCruCtx ret in + dbgNames' rets >>>= \names -> + emitStmt rets names loc + (TypedCall freg fun_perm + (varsToTypedRegs ghosts_ns) gexprs args) >>>= \(_ :>: ret') -> stmtRecombinePerms >>> pure (addCtxName ctx ret') @@ -2838,7 +2960,7 @@ tcEmitStmt' ctx loc (Assert reg msg) = getRegEqualsExpr treg >>= \case PExpr_Bool True -> pure ctx PExpr_Bool False -> stmtFailM (\_ -> pretty "Failed assertion") - _ -> ctx <$ emitStmt CruCtxNil loc (TypedAssert (tcReg ctx reg) (tcReg ctx msg)) + _ -> ctx <$ emitStmt CruCtxNil MNil loc (TypedAssert (tcReg ctx reg) (tcReg ctx msg)) tcEmitStmt' _ _ _ = error "tcEmitStmt: unsupported statement" @@ -2858,8 +2980,9 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerExpr w blk_reg off_reg) = tblk_reg = tcReg ctx blk_reg in resolveConstant tblk_reg >>= \case Just 0 -> + nextDebugName >>>= \name -> withKnownNat w $ - emitLLVMStmt knownRepr loc (ConstructLLVMWord toff_reg) >>>= \x -> + emitLLVMStmt knownRepr name loc (ConstructLLVMWord toff_reg) >>>= \x -> stmtRecombinePerms >>> pure (addCtxName ctx x) _ -> stmtFailM (\i -> pretty "LLVM_PointerExpr: Non-zero pointer block: " @@ -2882,14 +3005,18 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerBlock w ptr_reg) = withKnownNat w $ getAtomicOrWordLLVMPerms tptr_reg >>>= \case Left e -> - emitLLVMStmt knownRepr loc (AssertLLVMWord tptr_reg e) >>>= \ret -> + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc (AssertLLVMWord tptr_reg e) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) Right _ -> stmtRecombinePerms >>> stmtProvePerm tptr_reg (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr tptr_reg) >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr tptr_reg) >>> + dbgNames >>>= \names -> + emitStmt + knownRepr names loc + (TypedSetReg knownRepr $ TypedExpr (NatLit 1) (Just $ PExpr_Nat 1)) >>>= \(_ :>: ret) -> stmtRecombinePerms >>> @@ -2912,17 +3039,20 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerOffset w ptr_reg) = getAtomicOrWordLLVMPerms tptr_reg >>>= \eith -> case eith of Left e -> - emitLLVMStmt knownRepr loc (DestructLLVMWord + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc (DestructLLVMWord tptr_reg e) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) Right _ -> stmtRecombinePerms >>> stmtProvePerm tptr_reg (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr tptr_reg) >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BVLit w $ BV.mkBV w 0) - (Just $ bvInt 0)) >>>= \(_ :>: ret) -> + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr tptr_reg) >>> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BVLit w $ BV.mkBV w 0) + (Just $ bvInt 0)) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -2935,17 +3065,22 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerIte w cond_reg then_reg else_reg) = telse_reg = tcReg ctx else_reg in getRegEqualsExpr tcond_reg >>= \case PExpr_Bool True -> - emitStmt knownRepr loc (TypedSetRegPermExpr knownRepr $ PExpr_Var $ - typedRegVar tthen_reg) >>>= \(_ :>: ret) -> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetRegPermExpr knownRepr $ + PExpr_Var $ typedRegVar tthen_reg) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) PExpr_Bool False -> - emitStmt knownRepr loc (TypedSetRegPermExpr knownRepr $ PExpr_Var $ - typedRegVar telse_reg) >>>= \(_ :>: ret) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetRegPermExpr knownRepr $ + PExpr_Var $ typedRegVar telse_reg) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) _ -> - emitLLVMStmt knownRepr loc (TypedLLVMIte w + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc (TypedLLVMIte w tcond_reg tthen_reg telse_reg) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -2962,15 +3097,20 @@ tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions tp conds reg) = rest_m PExpr_Bool False -> stmtFailM (\_ -> pretty err_str) _ -> - emitStmt knownRepr loc (TypedSetRegPermExpr knownRepr $ - PExpr_String err_str) >>>= \(_ :>: str_var) -> + emitStmt knownRepr noNames loc + (TypedSetRegPermExpr knownRepr $ + PExpr_String err_str) >>>= \(MNil :>: str_var) -> stmtRecombinePerms >>> - emitStmt CruCtxNil loc (TypedAssert tcond_reg $ - TypedReg str_var) >>>= \_ -> + emitStmt CruCtxNil MNil loc + (TypedAssert tcond_reg $ + TypedReg str_var) >>>= \MNil -> stmtRecombinePerms >>> rest_m) - (emitStmt (singletonCruCtx tp) loc (TypedSetRegPermExpr tp $ PExpr_Var $ - typedRegVar treg) >>>= \(_ :>: ret) -> + (let rets = singletonCruCtx tp in + dbgNames' rets >>>= \names -> + emitStmt rets names loc + (TypedSetRegPermExpr tp $ PExpr_Var $ + typedRegVar treg) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret)) conds @@ -3019,7 +3159,7 @@ emitTypedLLVMLoad :: (Name (LLVMPointerType sz)) emitTypedLLVMLoad _ loc treg fp ps = withLifetimeCurrentPerms (llvmFieldLifetime fp) $ \cur_perms -> - emitLLVMStmt knownRepr loc (TypedLLVMLoad treg fp ps cur_perms) + emitLLVMStmt knownRepr Nothing loc (TypedLLVMLoad treg fp ps cur_perms) -- | Emit a 'TypedLLVMStore' instruction, assuming the given LLVM field @@ -3030,6 +3170,7 @@ emitTypedLLVMLoad _ loc treg fp ps = emitTypedLLVMStore :: (HasPtrWidth w, 1 <= sz, KnownNat sz) => Proxy arch -> + Maybe String -> ProgramLoc -> TypedReg (LLVMPointerType w) -> LLVMFieldPerm w sz -> @@ -3039,9 +3180,9 @@ emitTypedLLVMStore :: (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) (Name UnitType) -emitTypedLLVMStore _ loc treg_ptr fp e ps = +emitTypedLLVMStore _ name loc treg_ptr fp e ps = withLifetimeCurrentPerms (llvmFieldLifetime fp) $ \cur_perms -> - emitLLVMStmt knownRepr loc (TypedLLVMStore treg_ptr fp e ps cur_perms) + emitLLVMStmt knownRepr name loc (TypedLLVMStore treg_ptr fp e ps cur_perms) open :: HasPtrWidth wptr => f (LLVMPointerType wptr) -> NatRepr wptr open _ = ?ptrWidth @@ -3088,7 +3229,8 @@ tcEmitLLVMStmt arch ctx loc (LLVM_Store _ ptr tp storage _ val) stmtProvePerm tptr (llvmWriteTrueExLPerm sz $ bvInt 0) >>>= \sbst -> let l = substLookup sbst Member_Base in let fp = llvmFieldWriteTrueL sz (bvInt 0) l in - emitTypedLLVMStore arch loc tptr fp + nextDebugName >>>= \name -> + emitTypedLLVMStore arch name loc tptr fp (PExpr_Var $ typedRegVar tval') DistPermsNil >>>= \z -> stmtRecombinePerms >>> pure (addCtxName ctx z) @@ -3104,13 +3246,15 @@ tcEmitLLVMStmt arch ctx loc (LLVM_MemClear _ (ptr :: Reg ctx (LLVMPointerType wp (forM_ @_ @_ @_ @() flds $ \case LLVMArrayField fp -> stmtProvePerm tptr (emptyMb $ ValPerm_Conj1 $ Perm_LLVMField fp) >>> - emitTypedLLVMStore arch loc tptr fp (PExpr_LLVMWord (bvInt 0)) DistPermsNil >>> + emitTypedLLVMStore arch Nothing loc tptr fp (PExpr_LLVMWord (bvInt 0)) DistPermsNil >>> stmtRecombinePerms) >>> -- Return a fresh unit variable - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr EmptyApp - (Just PExpr_Unit)) >>>= \(_ :>: z) -> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr EmptyApp + (Just PExpr_Unit)) >>>= \(MNil :>: z) -> stmtRecombinePerms >>> pure (addCtxName ctx z) @@ -3143,7 +3287,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_Alloca w _ sz_reg _ _) = case (maybe_fp, fp_perm, maybe_sz) of (Just fp, ValPerm_Conj [Perm_LLVMFrame fperms], Just sz) -> stmtProvePerm fp (emptyMb fp_perm) >>>= \_ -> - emitLLVMStmt knownRepr loc (TypedLLVMAlloca fp fperms sz) >>>= \y -> + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc + (TypedLLVMAlloca fp fperms sz) >>>= \y -> stmtRecombinePerms >>> pure (addCtxName ctx y) (_, _, Nothing) -> @@ -3160,11 +3306,13 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_Alloca w _ sz_reg _ _) = tcEmitLLVMStmt _arch ctx loc (LLVM_PushFrame _ _) = fmap stArchWidth top_get >>>= \SomePtrWidth -> withKnownNat ?ptrWidth $ - emitLLVMStmt knownRepr loc TypedLLVMCreateFrame >>>= \fp -> + emitLLVMStmt knownRepr Nothing loc TypedLLVMCreateFrame >>>= \fp -> setFramePtr ?ptrWidth (TypedReg fp) >>> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetReg knownRepr - (TypedExpr EmptyApp Nothing)) >>>= \(_ :>: y) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr + (TypedExpr EmptyApp Nothing)) >>>= \(MNil :>: y) -> stmtRecombinePerms >>> pure (addCtxName ctx y) @@ -3178,8 +3326,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PopFrame _) = | Some del_perms <- llvmFrameDeletionPerms fperms -> stmtProvePerms knownRepr (distPermsToExDistPerms del_perms) >>>= \_ -> stmtProvePerm fp (emptyMb fp_perm) >>>= \_ -> - emitLLVMStmt knownRepr loc (TypedLLVMDeleteFrame - fp fperms del_perms) >>>= \y -> + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc + (TypedLLVMDeleteFrame fp fperms del_perms) >>>= \y -> modify (\st -> st { stExtState = PermCheckExtState_LLVM Nothing }) >>> pure (addCtxName ctx y) _ -> stmtFailM (const $ pretty "LLVM_PopFrame: no frame perms") @@ -3189,8 +3338,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrAddOffset _w _ ptr off) = let tptr = tcReg ctx ptr toff = tcReg ctx off in getRegEqualsExpr toff >>>= \off_expr -> + nextDebugName >>>= \name -> withKnownNat ?ptrWidth $ - emitLLVMStmt knownRepr loc (OffsetLLVMValue tptr off_expr) >>>= \ret -> + emitLLVMStmt knownRepr name loc (OffsetLLVMValue tptr off_expr) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3208,7 +3358,8 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_LoadHandle _ _ ptr args ret) = , Just Refl <- testEquality tp (FunctionHandleRepr args ret) -> stmtEmbedImplM (implCopyConjM x ps i >>> recombinePerm x (ValPerm_Conj ps)) >>> - emitLLVMStmt (FunctionHandleRepr args ret) loc + nextDebugName >>>= \name -> + emitLLVMStmt (FunctionHandleRepr args ret) name loc (TypedLLVMLoadHandle tptr tp p) >>>= \ret' -> stmtRecombinePerms >>> pure (addCtxName ctx ret') @@ -3219,8 +3370,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_ResolveGlobal w _ gsym) = (stPermEnv <$> top_get) >>>= \env -> case lookupGlobalSymbol env gsym w of Just (p, _) -> + nextDebugName >>>= \name -> withKnownNat ?ptrWidth $ - emitLLVMStmt knownRepr loc (TypedLLVMResolveGlobal gsym p) >>>= \ret -> + emitLLVMStmt knownRepr name loc (TypedLLVMResolveGlobal gsym p) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) Nothing -> @@ -3318,17 +3470,19 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) -- FIXME: if we have bvEq e1' e2' or not (bvCouldEqual e1' e2') then we -- should return a known Boolean value in place of the Nothing (PExpr_LLVMWord e1', PExpr_LLVMWord e2') -> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr e1') >>>= \(_ :>: n1) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr e1') >>>= \(MNil :>: n1) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr e2') >>>= \(_ :>: n2) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr e2') >>>= \(MNil :>: n2) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BaseIsEq knownRepr - (RegWithVal (TypedReg n1) e1') - (RegWithVal (TypedReg n2) e2')) - Nothing) >>>= \(_ :>: ret) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BaseIsEq knownRepr + (RegWithVal (TypedReg n1) e1') + (RegWithVal (TypedReg n2) e2')) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3337,17 +3491,19 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) -- FIXME: test off1 == off2 like above (asLLVMOffset -> Just (x1', off1), asLLVMOffset -> Just (x2', off2)) | x1' == x2' -> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr off1) >>>= \(_ :>: n1) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr off1) >>>= \(MNil :>: n1) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr off2) >>>= \(_ :>: n2) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr off2) >>>= \(MNil :>: n2) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BaseIsEq knownRepr - (RegWithVal (TypedReg n1) off1) - (RegWithVal (TypedReg n2) off2)) - Nothing) >>>= \(_ :>: ret) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BaseIsEq knownRepr + (RegWithVal (TypedReg n1) off1) + (RegWithVal (TypedReg n2) off2)) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3357,10 +3513,12 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) (PExpr_LLVMWord _e, asLLVMOffset -> Just (x', _)) -> let r' = TypedReg x' in stmtProvePerm r' (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr r') >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BoolLit False) - Nothing) >>>= \(_ :>: ret) -> + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr r') >>> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BoolLit False) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3368,10 +3526,12 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) (asLLVMOffset -> Just (x', _), PExpr_LLVMWord _e) -> let r' = TypedReg x' in stmtProvePerm r' (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr r') >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BoolLit False) - Nothing) >>>= \(_ :>: ret) -> + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr r') >>> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BoolLit False) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3382,6 +3542,14 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) sep [pretty "Could not compare LLVM pointer values", permPretty i x1, pretty "and", permPretty i x2]) +tcEmitLLVMStmt _arch ctx loc LLVM_Debug{} = +-- let tptr = tcReg ctx ptr in + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr (TypedExpr EmptyApp Nothing)) >>>= \(MNil :>: ret) -> + stmtRecombinePerms >>> + pure (addCtxName ctx ret) + tcEmitLLVMStmt _arch _ctx _loc stmt = error ("tcEmitLLVMStmt: unimplemented statement - " ++ show (ppApp (\_ -> mempty) stmt)) @@ -3701,30 +3869,32 @@ tcTermStmt _ tstmt = -- an empty stack of distinguished permissions tcEmitStmtSeq :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => + [Maybe String] -> CtxTrans ctx -> StmtSeq ext cblocks ret ctx -> PermCheckM ext cblocks blocks tops ret () RNil (TypedStmtSeq ext blocks tops ret RNil) RNil () -tcEmitStmtSeq ctx (ConsStmt loc stmt stmts) = - setErrorPrefix loc (ppStmt (Ctx.size ctx) stmt) ctx (stmtInputRegs stmt) >>> - tcEmitStmt ctx loc stmt >>>= \ctx' -> tcEmitStmtSeq ctx' stmts -tcEmitStmtSeq ctx (TermStmt loc tstmt) = - setErrorPrefix loc (pretty tstmt) ctx (termStmtRegs tstmt) >>> +tcEmitStmtSeq names ctx (ConsStmt loc stmt stmts) = + setErrorPrefix names loc (ppStmt (Ctx.size ctx) stmt) ctx (stmtInputRegs stmt) >>> + tcEmitStmt ctx loc stmt >>>= \ctx' -> tcEmitStmtSeq names ctx' stmts +tcEmitStmtSeq names ctx (TermStmt loc tstmt) = + setErrorPrefix names loc (pretty tstmt) ctx (termStmtRegs tstmt) >>> tcTermStmt ctx tstmt >>>= \typed_tstmt -> gmapRet (>> return (TypedTermStmt loc typed_tstmt)) -- | Type-check the body of a Crucible block as the body of an entrypoint tcBlockEntryBody :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => + [Maybe String] -> Block ext cblocks ret args -> TypedEntry TCPhase ext blocks tops ret (CtxToRList args) ghosts -> TopPermCheckM ext cblocks blocks tops ret (Mb ((tops :++: CtxToRList args) :++: ghosts) (TypedStmtSeq ext blocks tops ret ((tops :++: CtxToRList args) :++: ghosts))) -tcBlockEntryBody blk entry@(TypedEntry {..}) = - runPermCheckM typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $ +tcBlockEntryBody names blk entry@(TypedEntry {..}) = + runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $ \tops_ns args_ns ghosts_ns perms -> let ctx = mkCtxTrans (blockInputs blk) args_ns ns = RL.append (RL.append tops_ns args_ns) ghosts_ns in @@ -3740,7 +3910,7 @@ tcBlockEntryBody blk entry@(TypedEntry {..}) = pretty "Input perms:" <> align (permPretty i perms)) >>> stmtRecombinePerms >>> - tcEmitStmtSeq ctx (blk ^. blockStmts) + tcEmitStmtSeq names ctx (blk ^. blockStmts) -- | Prove that the permissions held at a call site from the given source @@ -3755,7 +3925,7 @@ proveCallSiteImpl :: ((tops :++: args) :++: vars) tops args ghosts) proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out = - fmap CallSiteImpl $ runPermCheckM srcID args vars mb_perms_in $ + fmap CallSiteImpl $ runPermCheckM [] srcID args vars mb_perms_in $ \tops_ns args_ns _ perms_in -> let perms_out = give (cruCtxProxies ghosts) $ @@ -3825,22 +3995,23 @@ widenEntry (TypedEntry {..}) = -- 'True', recompute the entrypoint input permissions using widening visitEntry :: (PermCheckExtC ext, CtxToRList cargs ~ args, KnownRepr ExtRepr ext) => + [Maybe String] -> Bool -> Block ext cblocks ret cargs -> TypedEntry TCPhase ext blocks tops ret args ghosts -> TopPermCheckM ext cblocks blocks tops ret (Some (TypedEntry TCPhase ext blocks tops ret args)) -- If the entry is already complete, do nothing -visitEntry _ _ entry +visitEntry _ _ _ entry | isJust $ completeTypedEntry entry = trace ("visitEntry " ++ show (typedEntryID entry) ++ ": no change") $ return $ Some entry -- Otherwise, visit the call sites, widen if needed, and type-check the body -visitEntry _ _ (TypedEntry {..}) +visitEntry _ _ _ (TypedEntry {..}) | tracePretty (vsep [pretty ("visitEntry " ++ show typedEntryID ++ " with input perms:"), permPretty emptyPPInfo typedEntryPermsIn]) False = undefined -visitEntry can_widen blk entry = +visitEntry names can_widen blk entry = mapM (traverseF $ visitCallSite entry) (typedEntryCallers entry) >>= \callers -> if can_widen && any (anyF typedCallSiteImplFails) callers then @@ -3849,17 +4020,18 @@ visitEntry can_widen blk entry = -- If we widen then we are throwing away the old body, so all of its -- callees are no longer needed and can be deleted modifying stBlockMap (deleteEntryCallees $ typedEntryID entry) >> - visitEntry False blk entry' + visitEntry names False blk entry' else if isJust (typedEntryBody entry) then -- If the body was complete when we started and we are not widening, there -- is no reason to re-type-check the body, so just update the callers return $ Some $ entry { typedEntryCallers = callers } else - do body <- maybe (tcBlockEntryBody blk entry) return (typedEntryBody entry) + do body <- maybe (tcBlockEntryBody names blk entry) return (typedEntryBody entry) return $ Some $ entry { typedEntryCallers = callers, typedEntryBody = Just body } + -- | Visit a block by visiting all its entrypoints visitBlock :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => @@ -3870,7 +4042,7 @@ visitBlock blk@(TypedBlock {..}) = (stCBlocksEq <$> get) >>= \Refl -> flip (set typedBlockEntries) blk <$> mapM (\(Some entry) -> - visitEntry typedBlockCanWiden typedBlockBlock entry) _typedBlockEntries + visitEntry _typedBlockNames typedBlockCanWiden typedBlockBlock entry) _typedBlockEntries -- | Flatten a list of topological ordering components to a list of nodes in -- topological order paired with a flag denoting which nodes were loop heads