Skip to content

Commit

Permalink
Merge branch 'collected_fixes' into riscv-symbexec
Browse files Browse the repository at this point in the history
  • Loading branch information
@andreaslindner
andreaslindner committed Jan 19, 2025
2 parents f51a82a + aac1a8e commit 14d03fe
Show file tree
Hide file tree
Showing 16 changed files with 1,583 additions and 886 deletions.
21 changes: 18 additions & 3 deletions src/theory/tools/symbexec/bir_symbScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -374,7 +374,7 @@ Theorem bir_vars_of_exp_LIST_thm:
!e x.
MEM x (bir_vars_of_exp_LIST e) <=> x IN (bir_vars_of_exp e)
Proof
Induct_on `e` >> (
Induct_on `e` >> (
FULL_SIMP_TAC (std_ss++LIST_ss++PRED_SET_ss)
[bir_vars_of_exp_def, bir_vars_of_exp_LIST_def, APPEND_distinct_thm]
)
Expand All @@ -393,18 +393,33 @@ Theorem birs_senv_typecheck_thm:
!e senv.
birs_senv_typecheck e senv <=> bir_envty_includes_vs (birs_envty_of_senv senv) (bir_vars_of_exp e)
Proof
REWRITE_TAC
REWRITE_TAC
[birs_senv_typecheck_def, bir_envty_includes_vs_def,
birs_envty_of_senv_def, bir_envty_includes_v_def, EVERY_MEM, bir_vars_of_exp_LIST_thm] >>
METIS_TAC []
QED

Theorem bir_envty_includes_v_senv_gen_env_thm:
!v l.
bir_envty_includes_v (birs_envty_of_senv (birs_gen_env l)) v =
(OPTION_BIND (birs_gen_env l (bir_var_name v)) type_of_bir_exp = SOME (bir_var_type v))
Proof
fs[birs_envty_of_senv_def, bir_envty_includes_v_def]
QED

Theorem bir_envty_includes_vs_EMPTY:
!envty.
bir_envty_includes_vs envty EMPTY
Proof
fs[bir_envty_includes_vs_def]
QED

Theorem birs_senv_typecheck_IMP_birs_eval_exp_subst_type_thm:
!e senv.
(birs_senv_typecheck e senv) ==>
(type_of_bir_exp (birs_eval_exp_subst e senv) = type_of_bir_exp e)
Proof
SIMP_TAC std_ss [birs_eval_exp_subst_ALT_thm, birs_eval_exp_subst_ALT_def] >>
SIMP_TAC std_ss [birs_eval_exp_subst_ALT_thm, birs_eval_exp_subst_ALT_def] >>

REPEAT STRIP_TAC >>
`FEVERY
Expand Down
36 changes: 26 additions & 10 deletions src/theory/tools/symbexec/bir_symb_simpScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -934,11 +934,14 @@ end;

Theorem birs_simplification_Mem_Match_32_8_thm = LIST_CONJ [
gen_birs_simplification_Mem_Match_prove 32 8 8,
gen_birs_simplification_Mem_Match_prove 32 8 16,
gen_birs_simplification_Mem_Match_prove 32 8 32
(* TODO: should probably add 64 bit values here too *)
];

Theorem birs_simplification_Mem_Match_64_8_thm = LIST_CONJ [
gen_birs_simplification_Mem_Match_prove 64 8 8,
gen_birs_simplification_Mem_Match_prove 64 8 16,
gen_birs_simplification_Mem_Match_prove 64 8 32,
gen_birs_simplification_Mem_Match_prove 64 8 64
];
Expand Down Expand Up @@ -1431,22 +1434,35 @@ fun gen_simp_mem_bypass_thm memadsz memvalsz ldsz stsz =


Theorem birs_simplification_Mem_Bypass_32_8_thm = LIST_CONJ [
gen_simp_mem_bypass_thm 32 8 8 8,
gen_simp_mem_bypass_thm 32 8 8 16,
gen_simp_mem_bypass_thm 32 8 8 32,
gen_simp_mem_bypass_thm 32 8 16 8,
gen_simp_mem_bypass_thm 32 8 16 16,
gen_simp_mem_bypass_thm 32 8 16 32,
gen_simp_mem_bypass_thm 32 8 32 8,
gen_simp_mem_bypass_thm 32 8 32 32,
gen_simp_mem_bypass_thm 32 8 8 8,
gen_simp_mem_bypass_thm 32 8 8 32
gen_simp_mem_bypass_thm 32 8 32 16,
gen_simp_mem_bypass_thm 32 8 32 32
(* TODO: should probably add 64 bit values here too *)
];

Theorem birs_simplification_Mem_Bypass_64_8_thm = LIST_CONJ [
gen_simp_mem_bypass_thm 64 8 64 8,
gen_simp_mem_bypass_thm 64 8 64 64,
gen_simp_mem_bypass_thm 64 8 8 8,
gen_simp_mem_bypass_thm 64 8 8 64,
gen_simp_mem_bypass_thm 64 8 8 32,
gen_simp_mem_bypass_thm 64 8 32 32,
gen_simp_mem_bypass_thm 64 8 8 8,
gen_simp_mem_bypass_thm 64 8 8 16,
gen_simp_mem_bypass_thm 64 8 8 32,
gen_simp_mem_bypass_thm 64 8 8 64,
gen_simp_mem_bypass_thm 64 8 16 8,
gen_simp_mem_bypass_thm 64 8 16 16,
gen_simp_mem_bypass_thm 64 8 16 32,
gen_simp_mem_bypass_thm 64 8 16 64,
gen_simp_mem_bypass_thm 64 8 32 8,
gen_simp_mem_bypass_thm 64 8 32 16,
gen_simp_mem_bypass_thm 64 8 32 32,
gen_simp_mem_bypass_thm 64 8 32 64,
gen_simp_mem_bypass_thm 64 8 64 8,
gen_simp_mem_bypass_thm 64 8 64 16,
gen_simp_mem_bypass_thm 64 8 64 32,
gen_simp_mem_bypass_thm 64 8 32 64
gen_simp_mem_bypass_thm 64 8 64 64
];

val _ = export_theory();
6 changes: 4 additions & 2 deletions src/tools/lifter/bir_lifting_machinesLib_instances.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -275,6 +275,7 @@ val _ = assert bmr_rec_sanity_check arm8_bmr_rec
fun m0_reorder_bytes false (b1::b2::bs) =
b2::b1::(m0_reorder_bytes false bs)
| m0_reorder_bytes _ l = l
fun m0_reorder_bytes_data ef = if ef then I else List.rev;

local
val addr_ty = fcpLib.index_type (Arbnum.fromInt 32);
Expand All @@ -285,7 +286,7 @@ fun m0_mk_data_mm ef mem_loc hex_code =
let
val ml_tm =
wordsSyntax.mk_n2w (numSyntax.mk_numeral mem_loc, addr_ty)
val bytes = m0_reorder_bytes ef (bytes_of_hex_code hex_code)
val bytes = m0_reorder_bytes_data ef (bytes_of_hex_code hex_code)
val _ = if (length bytes = 2) orelse (length bytes = 4)
then ()
else failwith "invalid hex-code";
Expand Down Expand Up @@ -449,6 +450,7 @@ val _ = assert bmr_rec_sanity_check (m0_bmr_rec_LittleEnd_Main)
fun m0_mod_reorder_bytes false (b1::b2::bs) =
b2::b1::(m0_mod_reorder_bytes false bs)
| m0_mod_reorder_bytes _ l = l
fun m0_mod_reorder_bytes_data ef = if ef then I else List.rev;

local
val addr_ty = fcpLib.index_type (Arbnum.fromInt 32);
Expand All @@ -458,7 +460,7 @@ in

fun m0_mod_mk_data_mm ef mem_loc hex_code = let
val ml_tm = wordsSyntax.mk_n2w (numSyntax.mk_numeral mem_loc, addr_ty)
val bytes = m0_mod_reorder_bytes ef (bytes_of_hex_code hex_code)
val bytes = m0_mod_reorder_bytes_data ef (bytes_of_hex_code hex_code)
val _ = if (length bytes = 2) orelse (length bytes = 4) then () else failwith "invalid hex-code";
val bytes_tm = listSyntax.mk_list (bytes, val_word_ty)
in
Expand Down
67 changes: 65 additions & 2 deletions src/tools/symbexec/aux_moveawayLib.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,37 @@ in (* local *)
f_wrapped
end;

val EQ_flip = mk_eq o (fn (x,y) => (y,x)) o dest_eq;
fun wrap_cache_result_EQ_BEQ_gen to_intform to_k to_flip_k kcomp f =
let
val (add, lookup) = result_cache kcomp;
fun f_wrapped x =
let
val (x1,x2) = dest_eq x;
val intform = (to_intform x1, to_intform x2);
val k = (to_k intform);
val v_o = lookup k;
in
if isSome v_o then valOf v_o else
let
val v = f x;
in
add (k, v);
add (to_flip_k intform, CONV_RULE (LHS_CONV SYM_CONV) v);
v
end
end;
in
f_wrapped
end;

fun to_eq_string (s1, s2) =
s1^"="^s2;
fun to_flip_eq_string (s1, s2) =
s2^"="^s1;
fun wrap_cache_result_EQ_BEQ_string to_string = wrap_cache_result_EQ_BEQ_gen to_string to_eq_string to_flip_eq_string String.compare;

(*val wrap_cache_result_EQ_BEQ = wrap_cache_result_EQ_BEQ_gen I EQ_flip; *)
fun wrap_cache_result_EQ_BEQ kcomp f =
let
val (add, lookup) = result_cache kcomp;
Expand All @@ -54,7 +85,7 @@ in (* local *)
val v = f k;
in
add (k, v);
add ((*(rhs o concl o SYM_CONV)*)(mk_eq o (fn (x,y) => (y,x)) o dest_eq) k, CONV_RULE (LHS_CONV SYM_CONV) v);
add ((*(rhs o concl o SYM_CONV)*)EQ_flip k, CONV_RULE (LHS_CONV SYM_CONV) v);
v
end
end;
Expand All @@ -71,7 +102,7 @@ in (* local *)
val k_tm = k_tm_fun term;
val _ =
if check_res_tm_fun result then () else
(print_thm thm; print "\n\n"; raise ERR funname "didn't reach a result");
(print "\nunfinished:\n"; print_thm thm; print "\n\n"; raise ERR funname "didn't reach a result");
in (add (k_tm, thm); thm) end;

fun f_wrapped tm =
Expand All @@ -86,6 +117,38 @@ in (* local *)
f_wrapped
end;

local
datatype res_ex_t = Result of thm | Except of exn;
fun capture_res_ex f x =
Result(f x)
handle e => Except e
fun process_res_ex v =
case v of
Result x => x
| Except e => raise e;
in
fun wrap_res_exn f =
let
val (add, lookup) = result_cache Term.compare;
fun f_wrapped k =
let
val v_o = lookup k;
in
case v_o of
SOME v => process_res_ex v
| _ =>
let
val v = capture_res_ex f k;
in
add (k, v);
process_res_ex v
end
end;
in
f_wrapped
end;
end

fun measure_fun s f v =
let
val timer = holba_miscLib.timer_start 0;
Expand Down
Loading

0 comments on commit 14d03fe

Please sign in to comment.