From c1e2566272511a7da8943b5d634a71c33bc08a23 Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Mon, 7 Oct 2024 09:04:29 +0200 Subject: [PATCH 1/3] Moving updated tests and examples + added untracked symbexec README --- .gitignore | 12 +- hol/p4Script.sml | 284 ++++++++++++++---- hol/symb_exec/README.md | 87 ++++++ hol/symb_exec/example_ipsec/Holmakefile | 52 ++++ .../{ => example_ipsec}/basicScript.sml | 28 ++ .../{ => example_ipsec}/basic_altScript.sml | 34 ++- hol/symb_exec/p4_bigstepScript.sml | 10 +- hol/symb_exec/p4_symb_execLib.sml | 2 +- hol/symb_exec/symb_execLib.sml | 11 +- hol/symb_exec/tests/Holmakefile | 52 ++++ .../conditionalScript.sml} | 9 +- .../conditional_thenScript.sml} | 9 +- .../decomposeScript.sml} | 13 +- .../register_readScript.sml} | 12 +- .../register_read_writeScript.sml} | 9 +- .../selectScript.sml} | 12 +- .../table_knownScript.sml} | 14 +- .../table_known_fourScript.sml} | 16 +- .../table_unknownScript.sml} | 5 +- 19 files changed, 543 insertions(+), 128 deletions(-) create mode 100644 hol/symb_exec/README.md create mode 100644 hol/symb_exec/example_ipsec/Holmakefile rename hol/symb_exec/{ => example_ipsec}/basicScript.sml (98%) rename hol/symb_exec/{ => example_ipsec}/basic_altScript.sml (98%) create mode 100644 hol/symb_exec/tests/Holmakefile rename hol/symb_exec/{p4_symb_exec_test1Script.sml => tests/conditionalScript.sml} (97%) rename hol/symb_exec/{p4_symb_exec_test2Script.sml => tests/conditional_thenScript.sml} (97%) rename hol/symb_exec/{p4_symb_exec_test1_decompScript.sml => tests/decomposeScript.sml} (97%) rename hol/symb_exec/{p4_symb_exec_test7Script.sml => tests/register_readScript.sml} (98%) rename hol/symb_exec/{p4_symb_exec_test8Script.sml => tests/register_read_writeScript.sml} (98%) rename hol/symb_exec/{p4_symb_exec_test3Script.sml => tests/selectScript.sml} (96%) rename hol/symb_exec/{p4_symb_exec_test4Script.sml => tests/table_knownScript.sml} (96%) rename hol/symb_exec/{p4_symb_exec_test5Script.sml => tests/table_known_fourScript.sml} (93%) rename hol/symb_exec/{p4_symb_exec_test6Script.sml => tests/table_unknownScript.sml} (99%) diff --git a/.gitignore b/.gitignore index 7de3e6c8..4876a245 100644 --- a/.gitignore +++ b/.gitignore @@ -4,15 +4,9 @@ *.uo *.ui *.dat -hol/*Theory.sig -hol/*Theory.sml -hol/*-heap -hol/p4_from_json/*Theory.sig -hol/p4_from_json/*Theory.sml -hol/p4_from_json/*-heap -hol/symb_exec/*Theory.sig -hol/symb_exec/*Theory.sml -hol/symb_exec/*-heap +*Theory.sig +*Theory.sml +*-heap ## LaTeX stuff *.aux diff --git a/hol/p4Script.sml b/hol/p4Script.sml index 4f0b67a0..55c6f72c 100644 --- a/hol/p4Script.sml +++ b/hol/p4Script.sml @@ -21,10 +21,10 @@ Type bl = ``:bool list`` (* bit-string *) Type i = ``:num`` (* natural number *) Type m = ``:num`` (* indices *) -Type boolv = ``:bool`` - Type bitv = ``:(bl # num)`` +Type boolv = ``:bool`` + Type num_exp = ``:num`` @@ -35,6 +35,11 @@ funn = | funn_ext of x => x (* extern method call *) `; val _ = Hol_datatype ` +varn = + varn_name of x (* variable name *) + | varn_star of funn (* function return placeholder *) +`; +val _ = Hol_datatype ` v = (* value *) v_bool of boolv (* boolean value *) | v_bit of bitv (* bit-string *) @@ -45,18 +50,13 @@ v = (* value *) | v_bot (* no value *) `; val _ = Hol_datatype ` -varn = - varn_name of x (* variable name *) - | varn_star of funn (* function return placeholder *) -`; - -Type v_list = ``:(v list)`` -val _ = Hol_datatype ` status = (* execution status *) status_running | status_returnv of v | status_trans of x (* transition to parser state *) `; + +Type v_list = ``:(v list)`` val _ = Hol_datatype ` mk = (* matching kinds *) mk_exact @@ -68,17 +68,6 @@ mk = (* matching kinds *) `; -val _ = Hol_datatype ` -unop = - unop_neg (* negation *) - | unop_compl (* bitwise complement *) - | unop_neg_signed (* signed negation *) - | unop_un_plus (* unary plus *) -`; -val _ = Hol_datatype ` -cast = - cast_unsigned of m (* unsigned cast *) -`; val _ = Hol_datatype ` binop = binop_mul (* multiplication *) @@ -103,6 +92,30 @@ binop = | binop_bin_or (* binary or *) `; val _ = Hol_datatype ` +cast = + cast_unsigned of m (* unsigned cast *) +`; +val _ = Hol_datatype ` +unop = + unop_neg (* negation *) + | unop_compl (* bitwise complement *) + | unop_neg_signed (* signed negation *) + | unop_un_plus (* unary plus *) +`; + +Type mk_list = ``:(mk list)`` +val _ = Hol_datatype ` +s = (* set *) + s_sing of v (* singleton *) + | s_range of bitv => bitv (* interval *) + | s_mask of bitv => bitv (* bit mask *) + | s_univ (* universal *) +`; + + + +Type s_list = ``:(s list)`` +val _ = Hol_datatype ` e = (* expression *) e_v of v (* value *) | e_var of varn (* variable *) @@ -114,13 +127,11 @@ e = (* expression *) | e_concat of e => e (* concatenation of bit-strings *) | e_slice of e => e => e (* bit-slice *) | e_call of funn => e list (* function or extern call *) - | e_select of e => (v#x) list => x (* select *) + | e_select of e => (s_list#x) list => x (* select *) | e_struct of (x#e) list (* struct *) | e_header of boolv => (x#e) list (* header *) `; -Type mk_list = ``:(mk list)`` - val _ = Hol_datatype ` lval = @@ -146,13 +157,6 @@ struct_ty = | struct_ty_header `; val _ = Hol_datatype ` -d = (* parameter direction *) - d_in - | d_out - | d_inout - | d_none -`; -val _ = Hol_datatype ` tau = (* type *) tau_bool (* boolean *) | tau_bit of num_exp (* bit-string *) @@ -160,6 +164,13 @@ tau = (* type *) | tau_xtl of struct_ty => (x#tau) list (* struct *) | tau_ext (* extern *) `; +val _ = Hol_datatype ` +d = (* parameter direction *) + d_in + | d_out + | d_inout + | d_none +`; Type Ftau = ``:( ( tau # x # d ) list # tau)`` @@ -175,12 +186,19 @@ t = (* type *) t_tau of tau (* BASE TYPE *) | t_string_names_a of x_list (* represents parser states' names ex. a , not literals "a" *) `; +val _ = Hol_datatype ` +s_t = (* value set type *) + s_t_tau of tau (* base type *) + | s_t_top (* wildcard type *) +`; -Type ff = ``:('a -> 'a option)`` +Type taul = ``:(tau list)`` + +Type s_t_list = ``:(s_t list)`` Type ext_fun = ``:(('a # g_scope_list # scope_list) -> (('a # scope_list # status) option))`` -Type taul = ``:(tau list)`` +Type ff = ``:('a -> 'a option)`` Type d_list = ``:(d list)`` @@ -204,42 +222,44 @@ stmt = (* statement *) -Type func_map = ``:((string, (stmt # (string # d) list)) alist)`` - Type b_func_map = ``:((string, (stmt # (string # d) list)) alist)`` +Type func_map = ``:((string, (stmt # (string # d) list)) alist)`` + Type ext_fun_map = ``:((string, ((string # d) list # 'a ext_fun)) alist)`` -Type ext_map = ``:((string, ((((string # d) list # 'a ext_fun) option) # 'a ext_fun_map)) alist)`` - Type pars_map = ``:((string, stmt) alist)`` -Type tbl_map = ``:((string, ((mk list) # (x # e_list))) alist)`` +Type ext_map = ``:((string, ((((string # d) list # 'a ext_fun) option) # 'a ext_fun_map)) alist)`` -Type in_out = ``:(bl # num)`` +Type tbl_map = ``:((string, ((mk list) # (x # e_list))) alist)`` val _ = Hol_datatype ` pbl_type = (* programmable block type *) pbl_type_parser | pbl_type_control `; +Type in_out = ``:(bl # num)`` -Type pblock = ``:(pbl_type # ((string # d) list) # b_func_map # t_scope # pars_map # tbl_map)`` val _ = Hol_datatype ` ffblock = (* fixed-function block *) ffblock_ff of 'a ff `; +Type pblock = ``:(pbl_type # ((string # d) list) # b_func_map # t_scope # pars_map # tbl_map)`` -Type pblock_map = ``:((string, pblock) alist)`` Type ffblock_map = ``:((string, 'a ffblock) alist)`` +Type pblock_map = ``:((string, pblock) alist)`` + Type in_out_list = ``:(in_out list)`` + +Type pblock_list = ``:(pblock list)`` val _ = Hol_datatype ` arch_block = (* architectural block *) arch_block_inp @@ -248,19 +268,17 @@ arch_block = (* architectural block *) | arch_block_out `; -Type pblock_list = ``:(pblock list)`` - -Type input_f = ``:((in_out_list # 'a) -> (in_out_list # 'a) option)`` +Type apply_table_f = ``:((x # e_list # mk_list # (x # e_list) # 'a) -> (x # e_list) option)`` -Type output_f = ``:((in_out_list # 'a) -> (in_out_list # 'a) option)`` +Type copyout_pbl = ``:((g_scope list # 'a # d list # x list # status) -> 'a option)`` Type copyin_pbl = ``:((x list # d list # e list # 'a) -> scope option)`` -Type copyout_pbl = ``:((g_scope list # 'a # d list # x list # status) -> 'a option)`` +Type output_f = ``:((in_out_list # 'a) -> (in_out_list # 'a) option)`` -Type apply_table_f = ``:((x # e_list # mk_list # (x # e_list) # 'a) -> (x # e_list) option)`` +Type input_f = ``:((in_out_list # 'a) -> (in_out_list # 'a) option)`` Type ab_list = ``:(arch_block list)`` @@ -289,9 +307,9 @@ arch_frame_list = (* architecture-level frame list *) | arch_frame_list_regular of frame_list (* regular frame list *) `; -Type cstate = ``:((in_out_list # in_out_list # 'a) # ((num # g_scope_list # arch_frame_list # status) # (num # g_scope_list # arch_frame_list # status)))`` - Type astate = ``:('a aenv # g_scope_list # arch_frame_list # status)`` + +Type cstate = ``:((in_out_list # in_out_list # 'a) # ((num # g_scope_list # arch_frame_list # status) # (num # g_scope_list # arch_frame_list # status)))`` val is_const_def = Define ` (is_const (e_v _) = T) /\ (is_const _ = F) @@ -1890,11 +1908,69 @@ val copyout_def = Define ` | NONE => NONE `; +(* TODO: Handle partiality earlier and let it result in NONE instead of just F + * or being undefined. Since things are being evaluated all the time, we ideally want + * this to not evaluate unnecessarily - not trivial since this function is being held + * in the state *) +Definition p4_match_mask_def: + p4_match_mask val mask k = + (case k of + | v_bit (v', n') => + (case bitv_binop binop_and (v', n') mask of + | SOME res => + (case bitv_binop binop_and val mask of + | SOME res' => + (case bitv_binpred binop_eq res res' of + | SOME bool => bool + | NONE => F) + | NONE => F) + | NONE => F) + | _ => F) +End + +Definition p4_match_range_def: + p4_match_range lo hi k = + case k of + | v_bit (v', n') => + (case bitv_binpred binop_ge (v', n') lo of + | SOME T => + (case bitv_binpred binop_le (v', n') hi of + | SOME T => T + | _ => F) + | _ => F) + | _ => F +End + +Definition match_def: + match v s = + case s of + | s_sing v' => (v = v') + | s_range bitv bitv' => p4_match_range bitv bitv' v + | s_mask bitv bitv' => p4_match_mask bitv bitv' v + | s_univ => T +End + +Definition match_all_def: + (match_all [] = T) /\ + (match_all ((h, h')::t) = + if match h h' + then match_all t + else F) +End + +(* TODO: Hack *) +Definition match_all_e_def: + match_all_e e_l s_l = match_all (ZIP(vl_of_el e_l, s_l)) +End + val sel_def = Define ` - sel v (v_x_list) x = - case (FIND (\(ks, s). ks = v) v_x_list) of - | SOME (v, x') => x' - | NONE => x + sel v (s_list_x_list) x = + case v of + | v_struct x_v_list => + (case (FIND (\(s_list, x'). match_all (ZIP(SND $ UNZIP x_v_list,s_list))) s_list_x_list) of + | SOME (s_list, x') => x' + | NONE => x) + | _ => x `; val fully_reduced_def = Define ` @@ -2146,11 +2222,11 @@ Inductive e_sem: ==> ( ( e_red ctx g_scope_list scope_list (e_acc (e_v (v_header boolv (f_v_list))) f) (e_v v) ([]:frame list) ))) -[e_sel_acc:] (! (v_x_list:(v#x) list) (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (v:v) (x:x) (x':x) . +[e_sel_acc:] (! (s_list_x_list:(s_list#x) list) (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (v:v) (x:x) (x':x) . (clause_name "e_sel_acc") /\ -(( x' = sel v (v_x_list) x )) +(( x' = sel v (s_list_x_list) x )) ==> -( ( e_red ctx g_scope_list scope_list (e_select (e_v v) (v_x_list) x) (e_v (v_str x')) ([]:frame list) ))) +( ( e_red ctx g_scope_list scope_list (e_select (e_v v) (s_list_x_list) x) (e_v (v_str x')) ([]:frame list) ))) [e_concat_arg1:] (! (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (e:e) (e':e) (e'':e) (frame_list:frame_list) . (clause_name "e_concat_arg1") /\ @@ -2182,11 +2258,11 @@ Inductive e_sem: ==> ( ( e_red ctx g_scope_list scope_list (e_slice (e_v (v_bit bitv)) (e_v (v_bit bitv')) (e_v (v_bit bitv''))) (e_v (v_bit bitv''')) ([]:frame list) ))) -[e_sel_arg:] (! (v_x_list:(v#x) list) (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (e:e) (x:x) (e':e) (frame_list:frame_list) . +[e_sel_arg:] (! (s_list_x_list:(s_list#x) list) (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (e:e) (x:x) (e':e) (frame_list:frame_list) . (clause_name "e_sel_arg") /\ (( ( e_red ctx g_scope_list scope_list e e' frame_list ))) ==> -( ( e_red ctx g_scope_list scope_list (e_select e (v_x_list) x) (e_select e' (v_x_list) x) frame_list ))) +( ( e_red ctx g_scope_list scope_list (e_select e (s_list_x_list) x) (e_select e' (s_list_x_list) x) frame_list ))) [e_unop_arg:] (! (ctx:'a ctx) (g_scope_list:g_scope_list) (scope_list:scope_list) (unop:unop) (e:e) (e':e) (frame_list:frame_list) . (clause_name "e_unop_arg") /\ @@ -2638,10 +2714,10 @@ Type t_scope_list_g = ``:(t_scope list)`` Type t_scope_list = ``:(t_scope list)`` -Type t_scopes_frames = ``:(t_scope_list list)`` - Type t_scopes_tup = ``:(t_scope_list_g # t_scope_list)`` +Type t_scopes_frames = ``:(t_scope_list list)`` + val _ = Hol_datatype ` order_elem = (* the individual elements of the order in the state are fun name or tables names *) order_elem_f of funn @@ -2663,10 +2739,10 @@ Type funn_list = ``:( funn list )`` Type order = ``:(order_elem -> order_elem -> bool )`` -Type Prs_n = ``:(string list)`` - Type T_e = ``:( order # funn # delta )`` +Type Prs_n = ``:(string list)`` + (*************************************************) (****** Typing Rules Related definitions *********) @@ -2825,6 +2901,51 @@ slice_length_check w (vec1,len1) (vec2,len2) = bits_length_check w (v2n vec1) (v2n vec2) `; +Definition is_struct_def: + is_struct e = + case e of + e_v v => + (case v of + v_struct x_v_list => T + | _ => F) + | e_struct x_e_list => T + | _ => F +End + +(* 13.6 Select Expressions of P4 spec: of the possible types, only Boolean and bitvector are + * possible in HOL4P4 *) +(* TODO: Nested tuples are not yet allowed by HOL4P4: this would require generalising the s datatype + * and adjusting the import tool *) +Definition correct_value_set_types''_def: + (correct_value_set_types'' [] = T) /\ + (correct_value_set_types'' ((ty,s_ty)::t) = + case s_ty of + | s_t_tau tau => + if ty = tau + then correct_value_set_types'' t + else F + | s_t_top => + correct_value_set_types'' t + ) +End + +Definition correct_value_set_types'_def: + (correct_value_set_types' value_types [] = T) /\ + (correct_value_set_types' value_types (h::t) = + if correct_value_set_types'' (ZIP (value_types, h)) + then correct_value_set_types' value_types t + else F + ) +End + +(* First, check that the lengths agree *) +Definition correct_value_set_types_def: + correct_value_set_types value_types value_set_types = + if EVERY (\l. LENGTH l = LENGTH value_types) value_set_types + then correct_value_set_types' value_types value_set_types + else F +End + (* convert from a bit vector to constant *) val vec_to_const_def = Define ` vec_to_const (vec,len) = @@ -2955,6 +3076,37 @@ Inductive v_typ: ==> ( ( v_typ (v_ext_ref i) (t_tau tau_ext) F ))) End +(** definitions *) + +(* defns s_typ *) +Inductive s_typ: +(* defn s_typ *) + +[s_typ_sing:] (! (v:v) (tau:tau) (b:b) . +(clause_name "s_typ_sing") /\ +(( ( v_typ v (t_tau tau) b ))) + ==> +( ( s_typ (s_sing v) (s_t_tau tau) ))) + +[s_typ_range:] (! (bitv:bitv) (bitv':bitv) (w:i) . +(clause_name "s_typ_range") /\ +(( ( w = bs_width bitv ) ) /\ +( ( w = bs_width bitv' ) )) + ==> +( ( s_typ (s_range bitv bitv') (s_t_tau (tau_bit w )) ))) + +[s_typ_mask:] (! (bitv:bitv) (bitv':bitv) (w:i) . +(clause_name "s_typ_mask") /\ +(( ( w = bs_width bitv ) ) /\ +( ( w = bs_width bitv' ) )) + ==> +( ( s_typ (s_mask bitv bitv') (s_t_tau (tau_bit w )) ))) + +[s_typ_univ:] ( +(clause_name "s_typ_univ") + ==> +( ( s_typ s_univ s_t_top ))) +End (* create a relation between two scopes *) @@ -3122,12 +3274,14 @@ Inductive e_typ: ==> ( ( e_typ t_scopes_tup T_e (e_slice e (e_v (v_bit bitv)) (e_v (v_bit bitv'))) (t_tau (tau_bit ( ( ( ( w1 - w2 ) ) + 1 ) ) )) b ))) -[e_typ_select:] (! (v_x_list:(v#x) list) (t_scopes_tup:t_scopes_tup) (T_e:T_e) (e:e) (x:x) (tau:tau) (b':b) (b:b) . +[e_typ_select:] (! (s_list_x_s_t_list_list:(s_list#x#s_t_list) list) (x'_tau_list:(x#tau) list) (t_scopes_tup:t_scopes_tup) (T_e:T_e) (e:e) (x:x) (struct_ty:struct_ty) (b:b) . (clause_name "e_typ_select") /\ -(( ( e_typ t_scopes_tup T_e e (t_tau tau) b' )) /\ -( !i. (i< LENGTH ((MAP (\(v_,x_) . v_) v_x_list)) ) ==> ( v_typ (EL i ((MAP (\(v_,x_) . v_) v_x_list)) ) (t_tau tau ) b ) )) +(( is_struct e ) /\ +( ( e_typ t_scopes_tup T_e e (t_tau (tau_xtl struct_ty (x'_tau_list))) b )) /\ +( !i. (i < LENGTH ((MAP (\(s_list_,x_,s_t_list_) . s_list_) s_list_x_s_t_list_list)) ) ==> !j. (j < LENGTH (EL i ((MAP (\(s_list_,x_,s_t_list_) . s_list_) s_list_x_s_t_list_list)) )) ==> ( s_typ (EL j (EL i ((MAP (\(s_list_,x_,s_t_list_) . s_list_) s_list_x_s_t_list_list)) )) (EL j (EL i ((MAP (\(s_list_,x_,s_t_list_) . s_t_list_) s_list_x_s_t_list_list)) )) ) ) /\ +( correct_value_set_types ((MAP (\(x'_,tau_) . tau_) x'_tau_list)) ((MAP (\(s_list_,x_,s_t_list_) . s_t_list_) s_list_x_s_t_list_list)) )) ==> -( ( e_typ t_scopes_tup T_e (e_select e (v_x_list) x) (t_string_names_a ( ( ((MAP (\(v_,x_) . x_) v_x_list)) ) ++ ( ([(x)]) ) ) ) F ))) +( ( e_typ t_scopes_tup T_e (e_select e ((MAP (\(s_list_,x_,s_t_list_) . (s_list_,x_)) s_list_x_s_t_list_list)) x) (t_string_names_a ( ( ((MAP (\(s_list_,x_,s_t_list_) . x_) s_list_x_s_t_list_list)) ) ++ ( ([(x)]) ) ) ) F ))) [e_typ_call:] (! (e_tau_x_d_b_list:(e#tau#x#d#b) list) (t_scopes_tup:t_scopes_tup) (order:order) (funn:funn) (delta_g:delta_g) (delta_b:delta_b) (delta_x:delta_x) (delta_t:delta_t) (funn':funn) (tau:tau) . (clause_name "e_typ_call") /\ diff --git a/hol/symb_exec/README.md b/hol/symb_exec/README.md new file mode 100644 index 00000000..56e8e3d7 --- /dev/null +++ b/hol/symb_exec/README.md @@ -0,0 +1,87 @@ +# Symbolic execution + +The state of the single-thread symbolic execution is represented by a tuple of +`npaths` (current number of active symbolic paths), `path_tree` (a tree structure +holding n-chotomy theorems for every symbolic branch), a list of "symbolic states" +which are tuples of `path_id` (a unique number for every path), a number `fv_index `signifying +the current index used for introducing fresh free variables, the current path condition `path_cond`, +the current step theorem `step_thm`, a number representing fuel `fuel` which is decreased by every symbolic +step, and `nobranch_flag` which tells the symbolic executor to not perform a branch step +(typically set immediately after a branch). +Finally, there is a list accumulator of finished states, which unlike the symbolic state +tuple consist only of a path ID, a path condition and a step theorem. + +To initialise the state, the symbolic executor takes an initial path condition and +an (integer) amount of fuel. + +In addition, the symbolic executor has four language-specific static parameters: + +`lang_regular_step: bool -> thm -> thm`: Takes one regular step in the language lang + (takes a flag signifying whether the regular step is made just after a symbolic branch, + a step theorem and transforms it into a new step theorem) + +`lang_init_step_thm:thm`: Step theorem for zero steps + +`lang_should_branch:(int * thm) -> (thm * int list) option`: Decides whether to branch +by looking at the current step theorem, and uses an index when creating fresh HOL4 variables +when overapproximating externs. Returns NONE if branching should not +happen, and an n-chotomy theorem stating that the disjunction of the branch conditions holds +as well as a list of updated free variable indices when branching. + +`lang_is_finished:thm -> bool`: Decides whether symbolic execution should continue +on this path by looking at the current step theorem. + +Note that branching consumes one step of (SML function) fuel. + +## Concurrent version + +The concurrent version retains the same parts of the state, now stored using SML references. +Additions are the number of threads stored as a reference `nthreads_ref` and +furthermore `all_done` (an SML condition variable) and `mutex_exec` (an SML mutex). + +The idea is that the programmer providing the four language-specific static parameters +should not need deal with the concurrency implementation. The concurrency is achieved +by parameterising the symbolic execution in terms of the following four functions: + +`get_job: unit -> (int * int * thm * thm * int * bool) option`: This function returns +the head of the `work_queue` consisting of a path ID, free variable index, path condition, +step theorem, fuel and a flag indicating a preceding symbolic branch. + +`append_jobs: (int * int * thm * thm * int * bool) list -> unit`: This function appends a +list of "symbolic states" to the `work_queue`. + +`update_shared_state: bool -> term list * thm * term list * int list -> int * thm * int -> unit`: +This function takes a debug flag, and a tuple of a list of new path conditions, an n-chotomy theorem, +a list of new branch conditions and a list of new free variable indices (the result of branching), +and a tuple of a path ID, a step thm and fuel. It's used after symbolic branching. + +`finish_job: int * thm * thm -> bool`: This function appends one result to the list +of finished jobs, consisting of a tuple of a path ID, a path condition and a step theorem, +(same as in the single-threaded case). If the `work_queue` is empty, the function +will decrement `nthreads_ref` and return `true`, otherwise `false`. + +`register_new_worker_n: (unit -> unit) -> int -> unit`: This function takes a function +`work_fun:unit -> unit` and an integer `n`, forking `n` threads each computing `work_fun`, +up to the limit `nthreads_max`. + +## Tests and examples + +The tests are located in the `tests` subdirectory. After installation, run them by first executing +`Holmake` in this directory (`hol/symb_exec`), then in `tests`. + +For more information, open a test in e.g. Emacs, then change the line + +```sml +val debug_flag = false; +``` + +to + +```sml +val debug_flag = true; +``` + +and send everything to the REPL to observe debug output of what's going on. + +A mid-size example can be found in `example_ipsec` subdirectory. The Python +script `count_reds.py` can be used on the debug output to generate statistics about the symbolic execution. diff --git a/hol/symb_exec/example_ipsec/Holmakefile b/hol/symb_exec/example_ipsec/Holmakefile new file mode 100644 index 00000000..5489a53f --- /dev/null +++ b/hol/symb_exec/example_ipsec/Holmakefile @@ -0,0 +1,52 @@ +# includes +# ---------------------------------- +DEPENDENCIES = .. + + +# configuration +# ---------------------------------- +HOLHEAP = ../p4_symbexec-heap +NEWHOLHEAP = + +HEAPINC_EXTRA = wordsLib + + +# included lines follow +# ---------------------------------- + +# automatic Holmake targets (all theories and non-"Script.sml" .sml files) +# automatic heap inclusion by name pattern +# ---------------------------------- +SMLFILES = $(subst *.sml,, $(patsubst %Script.sml,%Theory.sml,$(wildcard *.sml))) +TARGETS = $(patsubst %.sml,%.uo,$(SMLFILES)) + +HEAPINC = $(subst *Theory,,$(patsubst %Script.sml,%Theory ,$(wildcard *Script.sml))) \ + $(subst *Syntax,,$(patsubst %.sml,% ,$(wildcard *Syntax.sml))) \ + $(subst *Simps,, $(patsubst %.sml,% ,$(wildcard *Simps.sml ))) \ + $(subst *Lib,, $(patsubst %.sml,% ,$(wildcard *Lib.sml ))) \ + $(HEAPINC_EXTRA) + + +# general configs +# ---------------------------------- +all: $(TARGETS) $(if $(NEWHOLHEAP),$(NEWHOLHEAP),) + +INCLUDES = $(DEPENDENCIES) $(if $(HOLHEAP),$(shell dirname $(HOLHEAP)),) + +EXTRA_CLEANS = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) $(wildcard *.exe) + +OPTIONS = QUIT_ON_FAILURE + +default: all + +.PHONY: all default + + +# holheap part +# ---------------------------------- +ifdef POLY + +$(NEWHOLHEAP): $(TARGETS) $(HOLHEAP) + $(protect $(HOLDIR)/bin/buildheap) $(if $(HOLHEAP),-b $(HOLHEAP),) -o $@ $(HEAPINC) + +endif diff --git a/hol/symb_exec/basicScript.sml b/hol/symb_exec/example_ipsec/basicScript.sml similarity index 98% rename from hol/symb_exec/basicScript.sml rename to hol/symb_exec/example_ipsec/basicScript.sml index 1f238431..456f4f12 100644 --- a/hol/symb_exec/basicScript.sml +++ b/hol/symb_exec/example_ipsec/basicScript.sml @@ -1439,7 +1439,35 @@ val path_cond = ASSUME “^basic_wf_sad_encrypt_tbl_tm /\ val n_max = 300; val debug_flag = true; val p4_is_finished_alt_opt = NONE (* (SOME (is_finished' 5)) *); +(* val postcond = “(\s. (packet_dropped s \/ (?bit_list. get_packet s = SOME bit_list /\ (LENGTH bit_list = 272 \/ LENGTH bit_list = 336 \/ LENGTH bit_list = 400 \/ LENGTH bit_list = 480 \/ LENGTH bit_list = 544)))):v1model_ascope astate -> bool”; +*) +(* Pick the bits at the right positions *) +val etherType = “[eth96; eth97; eth98; eth99; eth100; + eth101; eth102; eth103; eth104; eth105; eth106; eth107; eth108; eth109; + eth110; eth111]:bool list”; +val protocol = “[ip72; ip73; ip74; ip75; ip76; ip77; ip78; ip79]:bool list” + +val IPv4 = “[F; F; F; F; T; F; F; F; F; F; F; F; F; F; F; F]” +val ESP = “[F; F; T; T; F; F; T; F]” + +(* Alternative version: *) +val postcond = + “(\s. (* Either the package is dropped, *) + (packet_dropped s \/ + (* or, if it's not, *) + (?bit_list. get_packet s = SOME bit_list /\ + (* if etherType isn't IPv4, then packet length stays the same; *) + ((^etherType <> ^IPv4 /\ LENGTH bit_list = 336) \/ + (* if packet length increased, then ethertype must have been IPv4 + * and protocol can't have been ESP; *) + ((LENGTH bit_list = 336 \/ LENGTH bit_list = 400 \/ LENGTH bit_list = 480 \/ LENGTH bit_list = 544) /\ + (^etherType = ^IPv4 /\ ^protocol <> ^ESP)) \/ + (* if packet length decreased, then ethertype must have been IPv4 + * and protocol must have been ESP. *) + ((LENGTH bit_list = 336 \/ LENGTH bit_list = 272) /\ + (^etherType = ^IPv4 /\ ^protocol = ^ESP)))))):v1model_ascope astate -> bool”; + val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def, p4_symb_execTheory.get_packet_def, p4_symb_execTheory.packet_dropped_def, p4_v1modelTheory.v1model_is_drop_port_def]; val time_start = Time.now(); diff --git a/hol/symb_exec/basic_altScript.sml b/hol/symb_exec/example_ipsec/basic_altScript.sml similarity index 98% rename from hol/symb_exec/basic_altScript.sml rename to hol/symb_exec/example_ipsec/basic_altScript.sml index 12b82e8e..074b4cea 100644 --- a/hol/symb_exec/basic_altScript.sml +++ b/hol/symb_exec/example_ipsec/basic_altScript.sml @@ -1403,12 +1403,44 @@ val path_cond = ASSUME “^basic_alt_wf_sad_encrypt_tbl_tm /\ val n_max = 300; val debug_flag = true; val p4_is_finished_alt_opt = NONE (* (SOME (is_finished' 5)) *); +(* val postcond = “(\s. (packet_dropped s \/ (?bit_list. get_packet s = SOME bit_list /\ (LENGTH bit_list = 272 \/ LENGTH bit_list = 336 \/ LENGTH bit_list = 400 \/ LENGTH bit_list = 480 \/ LENGTH bit_list = 544)))):v1model_ascope astate -> bool”; +*) +(* Pick the bits at the right positions *) +val etherType = “[eth96; eth97; eth98; eth99; eth100; + eth101; eth102; eth103; eth104; eth105; eth106; eth107; eth108; eth109; + eth110; eth111]:bool list”; +val protocol = “[ip72; ip73; ip74; ip75; ip76; ip77; ip78; ip79]:bool list” + +val IPv4 = “[F; F; F; F; T; F; F; F; F; F; F; F; F; F; F; F]” +val ESP = “[F; F; T; T; F; F; T; F]” + +(* Alternative version: *) +val postcond = + “(\s. (* Either the package is dropped, *) + (packet_dropped s \/ + (* or, if it's not, *) + (?bit_list. get_packet s = SOME bit_list /\ + (* if etherType isn't IPv4, then packet length stays the same; *) + ((^etherType <> ^IPv4 /\ LENGTH bit_list = 336) \/ + (* if packet length increased, then ethertype must have been IPv4 + * and protocol can't have been ESP; *) + ((LENGTH bit_list = 336 \/ LENGTH bit_list = 400 \/ LENGTH bit_list = 480 \/ LENGTH bit_list = 544) /\ + (^etherType = ^IPv4 /\ ^protocol <> ^ESP)) \/ + (* if packet length decreased, then ethertype must have been IPv4 + * and protocol must have been ESP. *) + ((LENGTH bit_list = 336 \/ LENGTH bit_list = 272) /\ + (^etherType = ^IPv4 /\ ^protocol = ^ESP)))))):v1model_ascope astate -> bool”; + val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def, p4_symb_execTheory.get_packet_def, p4_symb_execTheory.packet_dropped_def, p4_v1modelTheory.v1model_is_drop_port_def]; +val postcond_simpset = pure_ss val time_start = Time.now(); -val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms; +(* DEBUG +val ctx_data = (def_term ctx) +*) +val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; val _ = print (String.concat ["Total time consumption: ", (LargeInt.toString $ Time.toMilliseconds ((Time.now()) - time_start)), " ms\n"]); diff --git a/hol/symb_exec/p4_bigstepScript.sml b/hol/symb_exec/p4_bigstepScript.sml index 1a1f577a..775d4314 100644 --- a/hol/symb_exec/p4_bigstepScript.sml +++ b/hol/symb_exec/p4_bigstepScript.sml @@ -69,7 +69,7 @@ End Definition bigstep_e_exec_def: (********************) (* Variable look-up *) - (bigstep_e_exec (scope_lists:scope_list) (INL (e_var x)) n = + (bigstep_e_exec (scope_lists:scope_list) (INL (e_var x)) (n:num) = case lookup_vexp scope_lists x of | SOME v => SOME (INL $ e_v v, n + 1) | NONE => NONE) @@ -1581,7 +1581,7 @@ End (* Version for use with e_multi_exec'_list *) Definition e_multi_exec'_count_def: - (e_multi_exec'_count _ _ _ e 0 = SOME (e, 0)) + (e_multi_exec'_count _ _ _ e 0 = SOME (e, 0:num)) /\ (e_multi_exec'_count (ctx:'a ctx) g_scope_list scope_list e (SUC fuel) = case e_multi_exec'_count ctx g_scope_list scope_list e fuel of @@ -1593,7 +1593,7 @@ Definition e_multi_exec'_count_def: End Definition e_multi_exec'_list_def: - (e_multi_exec'_list _ _ _ e_l 0 = SOME e_l) + (e_multi_exec'_list _ _ _ e_l (0:num) = SOME e_l) /\ (e_multi_exec'_list _ _ _ [] _ = SOME []) /\ @@ -5966,7 +5966,7 @@ End * and since the big-step semantics does not check the length of scope_list, a * non-emptiness requirement on scope_list has been added here *) Definition in_local_fun'_def: - (in_local_fun' ((ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map):'a actx) i (arch_frame_list_regular [(funn_name fname, stmt_stack, scope_list)]) n = + (in_local_fun' ((ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map):'a actx) i (arch_frame_list_regular [(funn_name fname, stmt_stack, scope_list)]) (n:num) = ((scope_list <> []) /\ (ALOOKUP func_map fname = NONE) /\ (case EL i ab_list of @@ -6625,6 +6625,7 @@ Definition small_big_exec_def: | _ => NONE End +(* Theorem small_big_exec_comp_conj: !assl ctx g_scope_list arch_frame_list status i in_out_list in_out_list' ascope g_scope_list' g_scope_list'' n' arch_frame_list' arch_frame_list'' n aenv i' in_out_list'' in_out_list''' ascope' status'. ((assl ==> arch_multi_exec (ctx:'a actx) ((aenv, g_scope_list, arch_frame_list, status_running):'a astate) n = SOME ((i,in_out_list,in_out_list',ascope), g_scope_list', arch_frame_list', status)) /\ @@ -6635,5 +6636,6 @@ small_big_exec ctx ((i,in_out_list,in_out_list',ascope), g_scope_list', arch_fra Proof cheat QED +*) val _ = export_theory (); diff --git a/hol/symb_exec/p4_symb_execLib.sml b/hol/symb_exec/p4_symb_execLib.sml index 8b79892f..f0f7bad6 100644 --- a/hol/symb_exec/p4_symb_execLib.sml +++ b/hol/symb_exec/p4_symb_execLib.sml @@ -2306,7 +2306,7 @@ fun p4_symb_exec nthreads_max debug_flag arch_ty (ctx_def, ctx) (fty_map, b_fty_ (* DEBUG: val lang_regular_step = p4_regular_step (debug_flag, ctx_def, ctx, norewr_eval_ctxt, eval_ctxt) comp_thm; val lang_init_step_thm = init_step_thm; -val lang_should_branch = p4_should_branch (fty_map', b_fty_map') const_actions_tables' path_cond_defs (debug_flag, ctx_def); +val lang_should_branch = p4_should_branch (fty_map', b_fty_map', pblock_action_names_map) const_actions_tables' path_cond_defs (debug_flag, ctx_def); val lang_is_finished = is_finished; val const_actions_tables = const_actions_tables' diff --git a/hol/symb_exec/symb_execLib.sml b/hol/symb_exec/symb_execLib.sml index ed2f924f..96aeac19 100644 --- a/hol/symb_exec/symb_execLib.sml +++ b/hol/symb_exec/symb_execLib.sml @@ -245,15 +245,16 @@ local (* Generic symbolic execution * This has four language-specific parameters: * - * lang_regular_step (thm -> thm): Takes one regular step in the language lang - * (takes a step theorem and transforms it into a new step theorem) + * lang_regular_step (bool -> thm -> thm): Takes one regular step in the language lang + * (takes a step theorem, a flag signifying if this is a regular step just after a branch, + * and transforms it into a new step theorem) * * lang_init_step_thm (thm): Step theorem for zero steps * - * lang_should_branch (thm -> (term list * thm) option): Decides whether to branch + * lang_should_branch ((int * thm) -> (thm * int list) option): Decides whether to branch * by looking at the current step theorem. Returns NONE if branching should not - * happen, and a list of different branch conditions (used to update the path conditions) - * and a disjunction theorem stating that the disjunction of the branch conditions holds. + * happen, and an n-chotomy theorem stating that the disjunction of the branch conditions holds + * and a list of updated free variable indices when branching. * * lang_is_finished (thm -> bool): Decides whether symbolic execution should continue * on this path by looking at the current step theorem: check is performed after taking a step. diff --git a/hol/symb_exec/tests/Holmakefile b/hol/symb_exec/tests/Holmakefile new file mode 100644 index 00000000..5489a53f --- /dev/null +++ b/hol/symb_exec/tests/Holmakefile @@ -0,0 +1,52 @@ +# includes +# ---------------------------------- +DEPENDENCIES = .. + + +# configuration +# ---------------------------------- +HOLHEAP = ../p4_symbexec-heap +NEWHOLHEAP = + +HEAPINC_EXTRA = wordsLib + + +# included lines follow +# ---------------------------------- + +# automatic Holmake targets (all theories and non-"Script.sml" .sml files) +# automatic heap inclusion by name pattern +# ---------------------------------- +SMLFILES = $(subst *.sml,, $(patsubst %Script.sml,%Theory.sml,$(wildcard *.sml))) +TARGETS = $(patsubst %.sml,%.uo,$(SMLFILES)) + +HEAPINC = $(subst *Theory,,$(patsubst %Script.sml,%Theory ,$(wildcard *Script.sml))) \ + $(subst *Syntax,,$(patsubst %.sml,% ,$(wildcard *Syntax.sml))) \ + $(subst *Simps,, $(patsubst %.sml,% ,$(wildcard *Simps.sml ))) \ + $(subst *Lib,, $(patsubst %.sml,% ,$(wildcard *Lib.sml ))) \ + $(HEAPINC_EXTRA) + + +# general configs +# ---------------------------------- +all: $(TARGETS) $(if $(NEWHOLHEAP),$(NEWHOLHEAP),) + +INCLUDES = $(DEPENDENCIES) $(if $(HOLHEAP),$(shell dirname $(HOLHEAP)),) + +EXTRA_CLEANS = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) $(wildcard *.exe) + +OPTIONS = QUIT_ON_FAILURE + +default: all + +.PHONY: all default + + +# holheap part +# ---------------------------------- +ifdef POLY + +$(NEWHOLHEAP): $(TARGETS) $(HOLHEAP) + $(protect $(HOLDIR)/bin/buildheap) $(if $(HOLHEAP),-b $(HOLHEAP),) -o $@ $(HEAPINC) + +endif diff --git a/hol/symb_exec/p4_symb_exec_test1Script.sml b/hol/symb_exec/tests/conditionalScript.sml similarity index 97% rename from hol/symb_exec/p4_symb_exec_test1Script.sml rename to hol/symb_exec/tests/conditionalScript.sml index cadbcf74..31ab17bf 100644 --- a/hol/symb_exec/p4_symb_exec_test1Script.sml +++ b/hol/symb_exec/tests/conditionalScript.sml @@ -4,13 +4,13 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test1"; +val _ = new_theory "conditional"; (* Test 1: * There's a single if-statement that branches on symbolic bits. * Postcondition holds regardless of which path was taken. * - * This tests if basic branching and unification works. *) + * This tests if branching on an if-statement and unification works. *) val symb_exec1_blftymap = ``[]:(string, ((funn, (p_tau list # p_tau)) alist)) alist``; @@ -136,7 +136,7 @@ val symb_exec1_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [([e1; e (* symb_exec: *) (* Parameter assignment for debugging: *) -val debug_flag = true; +val debug_flag = false; val arch_ty = p4_v1modelLib.v1model_arch_ty val ctx = symb_exec1_actx val (fty_map, b_fty_map, pblock_action_names_map) = (symb_exec1_ftymap, symb_exec1_blftymap, symb_exec1_pblock_action_names_map) @@ -151,6 +151,7 @@ val p4_is_finished_alt_opt = NONE val n_max = 50; val postcond = “(\s. packet_has_port s 1 \/ packet_has_port s 2):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] +val postcond_simpset = pure_ss (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl @@ -184,7 +185,7 @@ val (res_id1, res_cond1, res_thm1) = res_elem1 (* Finishes at 45 steps (one step of which is a symbolic branch) * (higher numbers as arguments will work, but do no extra computations) *) -val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; (* diff --git a/hol/symb_exec/p4_symb_exec_test2Script.sml b/hol/symb_exec/tests/conditional_thenScript.sml similarity index 97% rename from hol/symb_exec/p4_symb_exec_test2Script.sml rename to hol/symb_exec/tests/conditional_thenScript.sml index 6ccfcf05..e39e6202 100644 --- a/hol/symb_exec/p4_symb_exec_test2Script.sml +++ b/hol/symb_exec/tests/conditional_thenScript.sml @@ -4,14 +4,14 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test2"; +val _ = new_theory "conditional_then"; (* Test 2: * There's a single if-statement that branches on symbolic bits. * Postcondition holds only for the then-branch. * The precondition states that the then-branch should be taken. * - * This tests if basic pruning works. *) + * This tests if pruning after an if-statement works. *) val symb_exec2_blftymap = ``[]:(string, ((funn, (p_tau list # p_tau)) alist)) alist``; @@ -138,7 +138,7 @@ val symb_exec2_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [([e1; e (* symb_exec: *) (* Parameter assignment for debugging: *) -val debug_flag = true +val debug_flag = false val arch_ty = p4_v1modelLib.v1model_arch_ty val ctx = symb_exec2_actx val (fty_map, b_fty_map, pblock_action_names_map) = (symb_exec2_ftymap, symb_exec2_blftymap, symb_exec2_pblock_action_names_map) @@ -154,6 +154,7 @@ val fuel = 2 val n_max = 50; val postcond = “(\s. packet_has_port s 1):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] +val postcond_simpset = pure_ss (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl *) @@ -171,6 +172,6 @@ val (path_tree, [(id, path_cond_res, step_thm)]) = p4_symb_exec 1 debug_flag arc (* Finishes at 45 steps (one step of which is a symbolic branch) * (higher numbers as arguments will work, but do no extra computations) *) -val contract_thm = p4_symb_exec_prove_contract_conc debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond NONE n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract_conc debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never thms_to_add path_cond NONE n_max postcond postcond_rewr_thms postcond_simpset; val _ = export_theory (); diff --git a/hol/symb_exec/p4_symb_exec_test1_decompScript.sml b/hol/symb_exec/tests/decomposeScript.sml similarity index 97% rename from hol/symb_exec/p4_symb_exec_test1_decompScript.sml rename to hol/symb_exec/tests/decomposeScript.sml index 0e1b8fc7..79479c58 100644 --- a/hol/symb_exec/p4_symb_exec_test1_decompScript.sml +++ b/hol/symb_exec/tests/decomposeScript.sml @@ -4,13 +4,14 @@ open p4Theory; open p4_symb_execTheory p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test1_decomp"; +val _ = new_theory "decompose"; -(* Test 1: - * There's a single if-statement that branches on symbolic bits. +(* There's a single if-statement that branches on symbolic bits. * Postcondition holds regardless of which path was taken. * - * This tests if basic branching and unification works. *) + * This tests if basic branching and unification works. + * In addition, the verification is split up into verificaiton of the first + * programmable block, and the subsequent. *) val symb_exec1_blftymap = ``[]:(string, ((funn, (p_tau list # p_tau)) alist)) alist``; @@ -136,7 +137,7 @@ val symb_exec1_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [([e1; e (* symb_exec: *) (* Parameter assignment for debugging: *) -val debug_flag = true; +val debug_flag = false; val arch_ty = p4_v1modelLib.v1model_arch_ty val ctx = symb_exec1_actx val (fty_map, b_fty_map, pblock_action_names_map) = (symb_exec1_ftymap, symb_exec1_blftymap, symb_exec1_pblock_action_names_map) @@ -155,7 +156,7 @@ val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] (* State finish criterion: "block about to start has index block_index_stop" *) (* Straightforward from index 2 to 4, problem at 5 since disjunction is needed *) -val block_index_stop = “2” +val block_index_stop = “2:num” val p4_is_finished_alt_opt1 = SOME (fn step_thm => Teq $ rhs $ concl $ EVAL “p4_block_next ^(optionSyntax.dest_some $ rhs $ snd $ dest_imp $ concl step_thm) ^block_index_stop”); diff --git a/hol/symb_exec/p4_symb_exec_test7Script.sml b/hol/symb_exec/tests/register_readScript.sml similarity index 98% rename from hol/symb_exec/p4_symb_exec_test7Script.sml rename to hol/symb_exec/tests/register_readScript.sml index cff6c9e8..b3e0a9c8 100644 --- a/hol/symb_exec/p4_symb_exec_test7Script.sml +++ b/hol/symb_exec/tests/register_readScript.sml @@ -4,10 +4,11 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test7"; +val _ = new_theory "register_read"; (* Test 7: - * There is a large register array. This is read from at an index using symbolic bits. *) + * There is a large register array. This is read from at an index using symbolic bits. + * The test checks that the symbolic execution does not crash when reading from registers. *) val symb_exec7_blftymap = ``[("p",[]); ("vrfy",[]); ("update",[]); ("egress",[]); ("deparser",[]); ("ingress",[])]:(string, ((funn, (p_tau list # p_tau)) alist)) alist``; @@ -275,7 +276,7 @@ val symb_exec_pblock_map_def = hd $ Defn.eqns_of $ Defn.mk_defn "pblock_map" (mk (* symb_exec: *) (* Parameter assignment for debugging: *) -val debug_flag = true; +val debug_flag = false; val arch_ty = p4_v1modelLib.v1model_arch_ty val ctx = symb_exec7_actx val (fty_map, b_fty_map, pblock_action_names_map) = (symb_exec7_ftymap, symb_exec7_blftymap, symb_exec7_pblock_action_names_map) @@ -285,17 +286,18 @@ val init_astate = symb_exec7_astate_symb val stop_consts_rewr = [“v1model_register_read_inner”, “v1model_register_construct_inner”] val stop_consts_never = [] val thms_to_add = [] -val path_cond = ASSUME “T” +val path_cond = ASSUME T val p4_is_finished_alt_opt = NONE val n_max = 150; val postcond = “(\s. T):v1model_ascope astate -> bool”; val fuel = 1; val postcond_rewr_thms = [] +val postcond_simpset = pure_ss val time_start = Time.now(); (* val p4_symb_exec_fun = (p4_symb_exec 1) *) -val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; val _ = print (String.concat ["Total time consumption: ", (LargeInt.toString $ Time.toMilliseconds ((Time.now()) - time_start)), diff --git a/hol/symb_exec/p4_symb_exec_test8Script.sml b/hol/symb_exec/tests/register_read_writeScript.sml similarity index 98% rename from hol/symb_exec/p4_symb_exec_test8Script.sml rename to hol/symb_exec/tests/register_read_writeScript.sml index 5ec387ef..5638dbad 100644 --- a/hol/symb_exec/p4_symb_exec_test8Script.sml +++ b/hol/symb_exec/tests/register_read_writeScript.sml @@ -4,11 +4,13 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test8"; +val _ = new_theory "register_read_write"; (* Test 8: * There is a large register array. This is read from, then written to, at an index - * using symbolic bits. *) + * using symbolic bits. + * The test checks that the symbolic execution does not crash when reading from and + * writing to registers.*) val symb_exec8_blftymap = ``[("p",[]); ("vrfy",[]); ("update",[]); ("egress",[]); ("deparser",[]); ("ingress",[])]:(string, ((funn, (p_tau list # p_tau)) alist)) alist``; @@ -309,11 +311,12 @@ val n_max = 150; val postcond = “(\s. T):v1model_ascope astate -> bool”; val fuel = 1; val postcond_rewr_thms = [] +val postcond_simpset = pure_ss val time_start = Time.now(); (* val p4_symb_exec_fun = (p4_symb_exec 1) *) -val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; val _ = print (String.concat ["Total time consumption: ", (LargeInt.toString $ Time.toMilliseconds ((Time.now()) - time_start)), diff --git a/hol/symb_exec/p4_symb_exec_test3Script.sml b/hol/symb_exec/tests/selectScript.sml similarity index 96% rename from hol/symb_exec/p4_symb_exec_test3Script.sml rename to hol/symb_exec/tests/selectScript.sml index 306103d0..2e3e372d 100644 --- a/hol/symb_exec/p4_symb_exec_test3Script.sml +++ b/hol/symb_exec/tests/selectScript.sml @@ -4,14 +4,13 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test3"; +val _ = new_theory "select"; (* Test 3: * There's a single select expression that branches on the LSB. - * Postcondition holds only for "accept". - * The precondition states that the accept case should be selected. + * Postcondition holds for both branches. * - * This tests if branching on select statement and following pruning works. *) + * This tests if branching on select statement and following unification works. *) val symb_exec3_blftymap = ``[]:(string, ((funn, (p_tau list # p_tau)) alist)) alist``; @@ -156,11 +155,12 @@ val path_cond_defs = [] val init_astate = symb_exec3_astate_symb val stop_consts_rewr = [] val stop_consts_never = [] -val path_cond = ASSUME “e8 = T” +val path_cond = ASSUME T val p4_is_finished_alt_opt = NONE val n_max = 50; val postcond = “(\s. packet_has_port s 1):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] +val postcond_simpset = pure_ss (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl *) @@ -177,6 +177,6 @@ val [(path_cond_res, step_thm), (path_cond2_res, step_thm2)] = (* Finishes at 45 steps (one step of which is a symbolic branch) * (higher numbers as arguments will work, but do no extra computations) *) -val contract_thm = p4_symb_exec_prove_contract_conc debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract_conc debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; val _ = export_theory (); diff --git a/hol/symb_exec/p4_symb_exec_test4Script.sml b/hol/symb_exec/tests/table_knownScript.sml similarity index 96% rename from hol/symb_exec/p4_symb_exec_test4Script.sml rename to hol/symb_exec/tests/table_knownScript.sml index b3b20075..d6c4dc16 100644 --- a/hol/symb_exec/p4_symb_exec_test4Script.sml +++ b/hol/symb_exec/tests/table_knownScript.sml @@ -4,14 +4,13 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test4"; +val _ = new_theory "table_known"; (* Test 4: * There's a single table application, with two possible outcomes. - * A pre-set entry rules out the postcondition not holding, so - * postcondition holds for all branches. + * The postcondition holds for both outcomes. * - * This tests if branching on apply statement works. *) + * This tests if branching on an apply statement with known table works. *) val symb_exec4_blftymap = ``[]:(string, ((funn, (p_tau list # p_tau)) alist)) alist``; @@ -184,10 +183,11 @@ val path_cond_defs = [] val init_astate = symb_exec4_astate_symb val stop_consts_rewr = [] val stop_consts_never = [] -val path_cond = ASSUME “e8 = T” +val path_cond = ASSUME T val n_max = 50; -val postcond = “(\s. ~(packet_has_port s 1)):v1model_ascope astate -> bool”; +val postcond = “(\s. packet_has_port s 42 \/ packet_has_port s 101):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] +val postcond_simpset = pure_ss (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl val init_step_thm = eval_ctxt_gen (stop_consts_rewr@stop_consts_never) stop_consts_never path_cond (mk_arch_multi_exec (ctx, init_astate, 0)) @@ -216,6 +216,6 @@ val (path_tree, [(n, path_cond_res, step_thm), (n2, path_cond2_res, step_thm2)]) *) -val contract_thm = p4_symb_exec_prove_contract_conc false arch_ty (def_term ctx) (symb_exec4_ftymap, symb_exec4_blftymap, symb_exec4_pblock_action_names_map) ["t"] path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond NONE n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract_conc false arch_ty (def_term ctx) (symb_exec4_ftymap, symb_exec4_blftymap, symb_exec4_pblock_action_names_map) ["t"] path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond NONE n_max postcond postcond_rewr_thms postcond_simpset; val _ = export_theory (); diff --git a/hol/symb_exec/p4_symb_exec_test5Script.sml b/hol/symb_exec/tests/table_known_fourScript.sml similarity index 93% rename from hol/symb_exec/p4_symb_exec_test5Script.sml rename to hol/symb_exec/tests/table_known_fourScript.sml index f1117691..f165c8c2 100644 --- a/hol/symb_exec/p4_symb_exec_test5Script.sml +++ b/hol/symb_exec/tests/table_known_fourScript.sml @@ -4,12 +4,11 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test5"; +val _ = new_theory "table_known_four"; (* Test 5: * There's a single table application, with four possible outcomes. - * The pre-set entries rules out the postcondition not holding, so - * postcondition holds for all branches. + * The postcondition holds for all pre-set entries. * * This tests if multi-case branching on apply statement works. *) @@ -193,16 +192,21 @@ val symb_exec5_astate_symb = rhs $ concl $ EVAL ``p4_append_input_list [([e1; e2 (* symb_exec: *) (* Parameter assignment for debugging: *) +val debug_flag = false val arch_ty = p4_v1modelLib.v1model_arch_ty val ctx = symb_exec5_actx val path_cond_defs = [] val init_astate = symb_exec5_astate_symb val stop_consts_rewr = [] val stop_consts_never = [] -val path_cond = ASSUME “e8 = T” +val path_cond = ASSUME T val n_max = 50; -val postcond = “(\s. ~(packet_has_port s 1)):v1model_ascope astate -> bool”; +val postcond = “(\s. packet_has_port s 42 \/ + packet_has_port s 47 \/ + packet_has_port s 13 \/ + packet_has_port s 101):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] +val postcond_simpset = pure_ss (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl val init_step_thm = eval_ctxt_gen (stop_consts_rewr@stop_consts_never) stop_consts_never path_cond (mk_arch_multi_exec (ctx, init_astate, 0)) @@ -233,6 +237,6 @@ val step_thm = step_thm2; *) -val contract_thm = p4_symb_exec_prove_contract_conc true arch_ty (def_term ctx) (symb_exec5_ftymap, symb_exec5_blftymap, symb_exec5_pblock_action_names_map) ["t"] path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond NONE n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract_conc debug_flag arch_ty (def_term ctx) (symb_exec5_ftymap, symb_exec5_blftymap, symb_exec5_pblock_action_names_map) ["t"] path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond NONE n_max postcond postcond_rewr_thms postcond_simpset; val _ = export_theory (); diff --git a/hol/symb_exec/p4_symb_exec_test6Script.sml b/hol/symb_exec/tests/table_unknownScript.sml similarity index 99% rename from hol/symb_exec/p4_symb_exec_test6Script.sml rename to hol/symb_exec/tests/table_unknownScript.sml index 025776f4..862ba593 100644 --- a/hol/symb_exec/p4_symb_exec_test6Script.sml +++ b/hol/symb_exec/tests/table_unknownScript.sml @@ -4,7 +4,7 @@ open p4Theory; open p4_symb_execLib; -val _ = new_theory "p4_symb_exec_test6"; +val _ = new_theory "table_unknown"; (* Test 6: * There are two table applications, one with two possible outcomes, @@ -265,6 +265,7 @@ val n_max = 150; val postcond = “(\s. T):v1model_ascope astate -> bool”; val fuel = 1; val postcond_rewr_thms = [] +val postcond_simpset = pure_ss (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl val init_step_thm = eval_ctxt_gen (stop_consts_rewr@stop_consts_never) stop_consts_never path_cond (mk_arch_multi_exec (ctx, init_astate, 0)) @@ -307,7 +308,7 @@ val step_thm = step_thm2; val time_start = Time.now(); (* val p4_symb_exec_fun = (p4_symb_exec 1) *) -val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms; +val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; val _ = print (String.concat ["Total time consumption: ", (LargeInt.toString $ Time.toMilliseconds ((Time.now()) - time_start)), From 9bb9ba4d091d40b016556ee08219676a1b63b67a Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Tue, 8 Oct 2024 23:42:16 +0200 Subject: [PATCH 2/3] Added the IMP stuff, some fixes --- hol/symb_exec/example_ipsec/basicScript.sml | 118 +---- .../example_ipsec/basic_altScript.sml | 46 +- hol/symb_exec/imp/Holmakefile | 52 ++ hol/symb_exec/imp/impScript.sml | 477 ++++++++++++++++++ hol/symb_exec/p4_symb_execLib.sml | 13 +- hol/symb_exec/symb_execLib.sml | 2 +- hol/symb_exec/tests/conditionalScript.sml | 28 +- .../tests/conditional_thenScript.sml | 2 +- hol/symb_exec/tests/decomposeScript.sml | 13 +- hol/symb_exec/tests/register_readScript.sml | 6 +- .../tests/register_read_writeScript.sml | 6 +- hol/symb_exec/tests/selectScript.sml | 2 +- hol/symb_exec/tests/table_knownScript.sml | 2 +- .../tests/table_known_fourScript.sml | 3 +- hol/symb_exec/tests/table_unknownScript.sml | 6 +- 15 files changed, 597 insertions(+), 179 deletions(-) create mode 100644 hol/symb_exec/imp/Holmakefile create mode 100644 hol/symb_exec/imp/impScript.sml diff --git a/hol/symb_exec/example_ipsec/basicScript.sml b/hol/symb_exec/example_ipsec/basicScript.sml index 456f4f12..bb6e06e6 100644 --- a/hol/symb_exec/example_ipsec/basicScript.sml +++ b/hol/symb_exec/example_ipsec/basicScript.sml @@ -5,6 +5,12 @@ open p4_symb_execLib; val _ = new_theory "basic"; +(* IPsec example + * Mid-size example based on https://github.com/didriklundberg/p4-ipsec + * (a fork of the code from this paper: https://arxiv.org/abs/1907.03593) + * + * Below is automatically generated by input tool: *) + val basic_blftymap = ``[("MyParser",[]); ("MyVerifyChecksum",[]); ("MyIngress", [(funn_name "drop",[],p_tau_bot); @@ -1285,7 +1291,7 @@ val basic_astate = ``((0,[],[],0,[],[("parseError",v_bit (fixwidth 32 (n2v 0),32 (********************) (* MANUAL ADDITIONS *) -(* TODO: Input has to be set up for every input packet type *) +(* Setting up the input packet. Note that this implicitly assumes the input has a certain length *) val eth_input = mk_symb_packet_prefix "eth" 112; val ipv4_input = mk_symb_packet_prefix "ip" 160; val esp_input = mk_symb_packet_prefix "esp" 64; @@ -1321,76 +1327,9 @@ Definition ctx'_def: ctx' = ^(replace_ext_impls pre_ctx [("", "update_checksum", “v1model_update_checksum'”)]) End - (* - -Extern approximation triggered if function name in top frame is in list, and any of the local -variables and extern object mapped to using "this" contain free variables or ARBs? -Better: Provide extern-specific function to decide whether to branch or not, with default behaviour being every occurrence of extern. - -val externs_to_approx = - [(("", "update_checksum"), (NONE, update_checksum_approx)); - (("register", "read"), (NONE, register_read_approx)); - (("register", "write"), (NONE, register_write_approx))] - - update_checksum: freeze eval at compute_checksum16, then add assumption for symbolic result of this. - This is easier than the below: do this first. - - register_construct: - 1. This should have an inner construct that generates the register array from a (constant) number. - The symbolic assumption becomes firstly the result of the above function in terms of - free variables, secondly a shorthand for the whole memory that is kept. These should somehow be put into the path condition as two conjuncts - would that work? - -val massive_tm = “[ARB; ARB; ARB]:bool list” - -val massive_tm_abbrev = mk_eq (massive_tm, mk_var("some_fresh_var", “:bool list”)); -val massive_thm_abbrev = prove(mk_exists (mk_var("some_fresh_var", “:bool list”), massive_tm_abbrev), gs[]); - -val test_thm = prove(“A ∧ B ⇒ (C ∧ P (^massive_tm))”, cheat); - -val hide_thm = ASSUME $ markerLib.mk_hide "some_fresh_var" (concl massive_tm_abbrev) - -val test_thm2 = ASM_REWRITE_RULE [Once CONJ_COMM, GSYM CONJ_ASSOC] $ hurdUtils.DISCH_CONJUNCTS_ALL $ UNDISCH_ALL $ ASM_REWRITE_RULE [] $ ADD_ASSUM massive_tm_abbrev test_thm; - -And when unifying: - -Note that the theorem used when unifying has en existentially quantified fresh variable: - -val test_thm3 = prove(“A ∧ B ⇒ C ∧ P [ARB:bool; ARB; ARB]”, -ASSUME_TAC (GEN_ALL test_thm2) >> -rpt disch_tac >> -ASSUME_TAC massive_thm_abbrev >> -gs[]); - -(* OLD -FULL_SIMP_TAC pure_ss [GSYM massive_thm_abbrev] ASM_REWRITE_RULE [Once CONJ_COMM, GSYM CONJ_ASSOC] $ hurdUtils.DISCH_CONJUNCTS_ALL $ UNDISCH_ALL $ SIMP_RULE (srw_ss()) [GSYM massive_thm_abbrev] $ test_thm2; -*) - -Maybe you can also separate the path condition you use for eval-in-ctxt with the one used for composition. In general, use a subset of the whole path condition for eval-in-ctxt usage. Then, you can remove the "abbreviation assumption" from the assumptions used when rewriting, yet still keep it in the path condition. -The process of doing the above can maybe be simplified by adding some kind of marker to "abbreviation assumptions". However, they abbreviation assumptions must be accumulated into the final contract, there seems to be no way around that. - -Note that in this exact case when the values of the initial register array are all ARBs, I can actually use a definition to hide all the values... But when should this be introduced? - - register_read: - 1. Define extern implementation in terms of function f1 from index and object to result. - First, the register array should be looked up (register object can't be symbolic). - 2. Approximation uses 1) the type of an entry in the array and 2) index and 3) the object - to give the result in terms of symbolic bits. - - register_write: - 1. Define extern implementation in terms of function f1 from index, object and value to result. - First, the register array should be looked up (register object can't be symbolic). - 2. Approximation uses 1) the type of an entry in the array and 2) index to give the result in - terms of a "write update" to the extern object. This - - *) - val ctx = rhs $ concl $ EVAL ``ctx'``; val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "basic_ctx" (mk_eq(mk_var("basic_ctx", type_of ctx), ctx)); -(* OLD -val ctx = basic_actx; -val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "basic_ctx" (mk_eq(mk_var("basic_ctx", type_of ctx), ctx)); -*) (* Additional parts of the context relevant only to symbolic execution *) val fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_ftymap_entries ^basic_ftymap” @@ -1399,9 +1338,12 @@ val b_fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_b val basic_ty_ctx_tm = “(^fty_map', ^b_fty_map', ^basic_pblock_action_names_map)” val symb_exec_ty_ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "ty_ctx" (mk_eq(mk_var("ty_ctx", type_of basic_ty_ctx_tm), basic_ty_ctx_tm)) +(* Abbreviating the pblock map *) val basic_pblock_map = #2 $ p4Syntax.dest_actx basic_actx; val symb_exec_pblock_map_def = hd $ Defn.eqns_of $ Defn.mk_defn "pblock_map" (mk_eq(mk_var("pblock_map", type_of basic_pblock_map), basic_pblock_map)) + +(* Well-formedness assumptions on table content for the precondition *) val basic_wf_sad_encrypt_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_exec_ty_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) ("sad_encrypt",sad_encrypt_tbl)” val basic_wf_sad_decrypt_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_exec_ty_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) ("sad_decrypt",sad_decrypt_tbl)” @@ -1410,20 +1352,8 @@ val basic_wf_forward_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_e val basic_wf_spd_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_exec_ty_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) ("spd",spd_tbl)” -fun is_finished' i_end step_thm = - let - val astate = p4_testLib.the_final_state_imp step_thm - val (aenv, _, _, _) = p4Syntax.dest_astate astate - val (i, io_list, _, _) = p4Syntax.dest_aenv aenv - in - (* Whenever the result of taking one step is at block index i, we're finished *) - if numSyntax.int_of_term i = i_end andalso null $ fst $ listSyntax.dest_list io_list - then true - else false - end -; -(* These are defined to enable easier debugging *) +(* The arguments to symbolic execution are mapped to variables here to enable easier debugging *) val (fty_map, b_fty_map, pblock_action_names_map) = (basic_ftymap, basic_blftymap, basic_pblock_action_names_map); val const_actions_tables = []; val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -1438,11 +1368,11 @@ val path_cond = ASSUME “^basic_wf_sad_encrypt_tbl_tm /\ ^basic_wf_spd_tbl_tm” val n_max = 300; val debug_flag = true; -val p4_is_finished_alt_opt = NONE (* (SOME (is_finished' 5)) *); -(* -val postcond = “(\s. (packet_dropped s \/ (?bit_list. get_packet s = SOME bit_list /\ (LENGTH bit_list = 272 \/ LENGTH bit_list = 336 \/ LENGTH bit_list = 400 \/ LENGTH bit_list = 480 \/ LENGTH bit_list = 544)))):v1model_ascope astate -> bool”; -*) -(* Pick the bits at the right positions *) +val p4_is_finished_alt_opt = NONE; + + +(* Defining the postcondition *) +(* Pick the bits at the right positions according to the input packet definition above *) val etherType = “[eth96; eth97; eth98; eth99; eth100; eth101; eth102; eth103; eth104; eth105; eth106; eth107; eth108; eth109; eth110; eth111]:bool list”; @@ -1451,7 +1381,6 @@ val protocol = “[ip72; ip73; ip74; ip75; ip76; ip77; ip78; ip79]:bool list” val IPv4 = “[F; F; F; F; T; F; F; F; F; F; F; F; F; F; F; F]” val ESP = “[F; F; T; T; F; F; T; F]” -(* Alternative version: *) val postcond = “(\s. (* Either the package is dropped, *) (packet_dropped s \/ @@ -1471,21 +1400,8 @@ val postcond = val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def, p4_symb_execTheory.get_packet_def, p4_symb_execTheory.packet_dropped_def, p4_v1modelTheory.v1model_is_drop_port_def]; val time_start = Time.now(); -(* TEST - - val (path_tree, res_list) = - p4_symb_exec 1 debug_flag arch_ty (ctx_def, ctx) (fty_map, b_fty_map, basic_pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [v1model_update_checksum'_def] path_cond p4_is_finished_alt_opt 1; - val (path_tree, res_list) = - p4_symb_exec 1 debug_flag arch_ty (ctx_def, ctx) (fty_map, b_fty_map, basic_pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [v1model_update_checksum'_def] path_cond p4_is_finished_alt_opt 46; - -val (path_tree, res_list) = - p4_symb_exec 1 debug_flag arch_ty (ctx_def, ctx) (fty_map, b_fty_map, basic_pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [v1model_update_checksum'_def] path_cond p4_is_finished_alt_opt 110; - -val (fv_index, path_cond, step_thm) = el 2 res_list - -*) -(* Commit 7daf3ad: +(* Commit 7463b72: Using all threads yield "Total time consumption: 885548 ms" (14m, 45s, 548ms) All threads minus two yield "Total time consumption: 845613 ms" (14m, 5s, 613ms) Single thread yields diff --git a/hol/symb_exec/example_ipsec/basic_altScript.sml b/hol/symb_exec/example_ipsec/basic_altScript.sml index 074b4cea..f2d2de05 100644 --- a/hol/symb_exec/example_ipsec/basic_altScript.sml +++ b/hol/symb_exec/example_ipsec/basic_altScript.sml @@ -5,6 +5,16 @@ open p4_symb_execLib; val _ = new_theory "basic_alt"; +(* IPsec example + * Mid-size example based on https://github.com/didriklundberg/p4-ipsec + * (a fork of the code from this paper: https://arxiv.org/abs/1907.03593) + * + * This version has also undergone a program transformation that moves the + * evaluation of the in-directed data argument of checksum computation + * before the method call. + * + * Below is automatically generated by input tool: *) + val basic_alt_blftymap = ``[("MyParser",[]); ("MyVerifyChecksum",[]); ("MyIngress", [(funn_name "drop",[],p_tau_bot); @@ -1312,7 +1322,7 @@ val basic_alt_astate = ``((0,[],[],0,[],[("parseError",v_bit (fixwidth 32 (n2v 0 (********************) (* MANUAL ADDITIONS *) -(* TODO: Input has to be set up for every input packet type *) +(* Setting up the input packet. Note that this implicitly assumes the input has a certain length *) val eth_input = mk_symb_packet_prefix "eth" 112; val ipv4_input = mk_symb_packet_prefix "ip" 160; val esp_input = mk_symb_packet_prefix "esp" 64; @@ -1351,11 +1361,6 @@ End val ctx = rhs $ concl $ EVAL ``ctx'``; val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "basic_alt_ctx" (mk_eq(mk_var("basic_alt_ctx", type_of ctx), ctx)); -(* OLD -val ctx = basic_alt_actx; -val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "basic_alt_ctx" (mk_eq(mk_var("basic_alt_ctx", type_of ctx), ctx)); -*) - (* Additional parts of the context relevant only to symbolic execution *) val fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_ftymap_entries ^basic_alt_ftymap” val b_fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_b_ftymap_entries ^basic_alt_blftymap” @@ -1363,9 +1368,13 @@ val b_fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_b val basic_alt_ty_ctx_tm = “(^fty_map', ^b_fty_map', ^basic_alt_pblock_action_names_map)” val symb_exec_ty_ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "ty_ctx" (mk_eq(mk_var("ty_ctx", type_of basic_alt_ty_ctx_tm), basic_alt_ty_ctx_tm)) + +(* Abbreviating the pblock map *) val basic_alt_pblock_map = #2 $ p4Syntax.dest_actx basic_alt_actx; val symb_exec_pblock_map_def = hd $ Defn.eqns_of $ Defn.mk_defn "pblock_map" (mk_eq(mk_var("pblock_map", type_of basic_alt_pblock_map), basic_alt_pblock_map)) + +(* Well-formedness assumptions on table content for the precondition *) val basic_alt_wf_sad_encrypt_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_exec_ty_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) ("sad_encrypt",sad_encrypt_tbl)” val basic_alt_wf_sad_decrypt_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_exec_ty_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) ("sad_decrypt",sad_decrypt_tbl)” @@ -1374,20 +1383,8 @@ val basic_alt_wf_forward_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl sy val basic_alt_wf_spd_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_exec_ty_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) ("spd",spd_tbl)” -fun is_finished' i_end step_thm = - let - val astate = p4_testLib.the_final_state_imp step_thm - val (aenv, _, _, _) = p4Syntax.dest_astate astate - val (i, io_list, _, _) = p4Syntax.dest_aenv aenv - in - (* Whenever the result of taking one step is at block index i, we're finished *) - if numSyntax.int_of_term i = i_end andalso null $ fst $ listSyntax.dest_list io_list - then true - else false - end -; -(* These are defined to enable easier debugging *) +(* The arguments to symbolic execution are mapped to variables here to enable easier debugging *) val (fty_map, b_fty_map, pblock_action_names_map) = (basic_alt_ftymap, basic_alt_blftymap, basic_alt_pblock_action_names_map); val const_actions_tables = []; val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -1402,11 +1399,11 @@ val path_cond = ASSUME “^basic_alt_wf_sad_encrypt_tbl_tm /\ ^basic_alt_wf_spd_tbl_tm” val n_max = 300; val debug_flag = true; -val p4_is_finished_alt_opt = NONE (* (SOME (is_finished' 5)) *); -(* -val postcond = “(\s. (packet_dropped s \/ (?bit_list. get_packet s = SOME bit_list /\ (LENGTH bit_list = 272 \/ LENGTH bit_list = 336 \/ LENGTH bit_list = 400 \/ LENGTH bit_list = 480 \/ LENGTH bit_list = 544)))):v1model_ascope astate -> bool”; -*) -(* Pick the bits at the right positions *) +val p4_is_finished_alt_opt = NONE; + + +(* Defining the postcondition *) +(* Pick the bits at the right positions according to the input packet definition above *) val etherType = “[eth96; eth97; eth98; eth99; eth100; eth101; eth102; eth103; eth104; eth105; eth106; eth107; eth108; eth109; eth110; eth111]:bool list”; @@ -1415,7 +1412,6 @@ val protocol = “[ip72; ip73; ip74; ip75; ip76; ip77; ip78; ip79]:bool list” val IPv4 = “[F; F; F; F; T; F; F; F; F; F; F; F; F; F; F; F]” val ESP = “[F; F; T; T; F; F; T; F]” -(* Alternative version: *) val postcond = “(\s. (* Either the package is dropped, *) (packet_dropped s \/ diff --git a/hol/symb_exec/imp/Holmakefile b/hol/symb_exec/imp/Holmakefile new file mode 100644 index 00000000..4cc32545 --- /dev/null +++ b/hol/symb_exec/imp/Holmakefile @@ -0,0 +1,52 @@ +# includes +# ---------------------------------- +DEPENDENCIES = .. + + +# configuration +# ---------------------------------- +HOLHEAP = +NEWHOLHEAP = + +HEAPINC_EXTRA = wordsLib + + +# included lines follow +# ---------------------------------- + +# automatic Holmake targets (all theories and non-"Script.sml" .sml files) +# automatic heap inclusion by name pattern +# ---------------------------------- +SMLFILES = $(subst *.sml,, $(patsubst %Script.sml,%Theory.sml,$(wildcard *.sml))) +TARGETS = $(patsubst %.sml,%.uo,$(SMLFILES)) + +HEAPINC = $(subst *Theory,,$(patsubst %Script.sml,%Theory ,$(wildcard *Script.sml))) \ + $(subst *Syntax,,$(patsubst %.sml,% ,$(wildcard *Syntax.sml))) \ + $(subst *Simps,, $(patsubst %.sml,% ,$(wildcard *Simps.sml ))) \ + $(subst *Lib,, $(patsubst %.sml,% ,$(wildcard *Lib.sml ))) \ + $(HEAPINC_EXTRA) + + +# general configs +# ---------------------------------- +all: $(TARGETS) $(if $(NEWHOLHEAP),$(NEWHOLHEAP),) + +INCLUDES = $(DEPENDENCIES) $(if $(HOLHEAP),$(shell dirname $(HOLHEAP)),) + +EXTRA_CLEANS = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) $(wildcard *.exe) + +OPTIONS = QUIT_ON_FAILURE + +default: all + +.PHONY: all default + + +# holheap part +# ---------------------------------- +ifdef POLY + +$(NEWHOLHEAP): $(TARGETS) $(HOLHEAP) + $(protect $(HOLDIR)/bin/buildheap) $(if $(HOLHEAP),-b $(HOLHEAP),) -o $@ $(HEAPINC) + +endif diff --git a/hol/symb_exec/imp/impScript.sml b/hol/symb_exec/imp/impScript.sml new file mode 100644 index 00000000..0fbac550 --- /dev/null +++ b/hol/symb_exec/imp/impScript.sml @@ -0,0 +1,477 @@ +open HolKernel boolLib liteLib simpLib Parse bossLib; + +val _ = new_theory "imp"; + +open listTheory alistTheory stringTheory; + +(*************************) +(* Auxiliary definitions *) + +Definition AUPDATE_def: + AUPDATE alist (k,v) = + case ALOOKUP alist k of + SOME _ => AFUPDKEY k (\old_v. v) alist + | NONE => (alist++[(k,v)]) +End + +Definition AUPDATE_LIST_def: + AUPDATE_LIST = FOLDL AUPDATE +End + +(****************) +(* IMP language *) + +Datatype: +v = (* value *) + v_bool bool (* Boolean *) + | v_num num (* natural number, possibly zero *) +End + +Datatype: +bop = (* binary operation *) + bop_mul (* multiplication *) + | bop_div (* (integer) division *) + | bop_mod (* modulo *) + | bop_add (* addition *) + | bop_sub (* (saturated) subtraction *) + | bop_lt (* less than *) + | bop_eq (* equal *) + | bop_and (* and *) + | bop_or (* or *) +End + +Datatype: +uop = (* binary operation *) + uop_neg (* negation *) +End + +Datatype: +e = (* expression *) + e_v v (* value *) + | e_var string (* variable *) + | e_uop uop e (* unary operation *) + | e_bop e bop e (* binary operation *) +End + +Datatype: +tau = (* type *) + tau_bool (* boolean *) + | tau_num (* number *) +End + +(* TODO: Should language have declare, block or only assign? *) +Datatype: +stmt = (* statement *) + stmt_empty (* empty statement *) + | stmt_ass string e (* assignment *) + | stmt_cond e stmt stmt (* conditional *) + | stmt_while e stmt (* loop *) + | stmt_seq stmt stmt (* sequence *) +End + +val _ = type_abbrev("imp_store", ``:((string, v) alist)``); + +Definition v_exec_uop_def: + (v_exec_uop uop_neg (v_bool b) = SOME (v_bool ~b)) + /\ + (v_exec_uop uop v = NONE) +End + +Definition v_exec_bop_def: + (v_exec_bop bop_mul (v_num n1) (v_num n2) = + SOME (v_num (n1 * n2))) + /\ + (v_exec_bop bop_div (v_num n1) (v_num n2) = + SOME (v_num (n1 DIV n2))) + /\ + (v_exec_bop bop_mod (v_num n1) (v_num n2) = + SOME (v_num (n1 MOD n2))) + /\ + (v_exec_bop bop_add (v_num n1) (v_num n2) = + SOME (v_num (n1 + n2))) + /\ + (v_exec_bop bop_sub (v_num n1) (v_num n2) = + SOME (v_num (n1 - n2))) + /\ + (v_exec_bop bop_lt (v_num n1) (v_num n2) = + SOME (v_bool (n1 < n2))) + /\ + (v_exec_bop bop_eq (v_num n1) (v_num n2) = + SOME (v_bool (n1 = n2))) + /\ + (v_exec_bop bop_eq (v_bool b1) (v_bool b2) = + SOME (v_bool (b1 = b2))) + /\ + (v_exec_bop bop_and (v_bool b1) (v_bool b2) = + SOME (v_bool (b1 /\ b2))) + /\ + (v_exec_bop bop_or (v_bool b1) (v_bool b2) = + SOME (v_bool (b1 \/ b2))) + /\ + (v_exec_bop bop v1 v2 = NONE) +End + +Definition e_exec_def: + (e_exec (st:imp_store) (e_var x) = + case ALOOKUP st x of + SOME v => SOME (e_v v) + | NONE => NONE) + /\ + (e_exec st (e_uop uop e) = + case e of + e_v v => + (case v_exec_uop uop v of + SOME v' => SOME (e_v v') + | NONE => NONE) + | _ => + (case e_exec st e of + SOME e' => SOME (e_uop uop e') + | NONE => NONE)) + /\ + (e_exec st (e_bop e1 bop e2) = + (case e1 of + (e_v v1) => + (case e2 of + (e_v v2) => + (case v_exec_bop bop v1 v2 of + SOME v' => SOME (e_v v') + | NONE => NONE) + | _ => + (case e_exec st e2 of + SOME e2' => SOME (e_bop e1 bop e2') + | NONE => NONE)) + | _ => + (case e_exec st e1 of + SOME e1' => SOME (e_bop e1' bop e2) + | NONE => NONE))) + /\ + (e_exec _ _ = NONE) +End + +Definition get_v_def: + get_v e = + case e of + e_v v => SOME v + | _ => NONE +End + +Definition get_v_bool_def: + get_v_bool e = + case get_v e of + SOME v => + (case v of + v_bool b => SOME b + | _ => NONE) + | NONE => NONE +End + +Definition stmt_exec_ass_def: + stmt_exec_ass varname v st = + AUPDATE st (varname, v) +End + +Definition stmt_exec_def: + (* Assignment *) + (stmt_exec st (stmt_ass varname e) = + case get_v e of + SOME v => + SOME (stmt_exec_ass varname v st, stmt_empty) + | NONE => + (case e_exec st e of + SOME e' => + SOME (st, stmt_ass varname e') + | _ => NONE)) + /\ + (* Conditional *) + (stmt_exec st (stmt_cond e stmt1 stmt2) = + case get_v_bool e of + SOME b => + (if b + then SOME (st, stmt1) + else SOME (st, stmt2)) + | NONE => + (case e_exec st e of + SOME e' => + SOME (st, stmt_cond e' stmt1 stmt2) + | NONE => NONE)) + /\ + (* While *) + (stmt_exec st (stmt_while e stmt) = + SOME (st, stmt_cond e (stmt_seq stmt (stmt_while e stmt)) stmt_empty)) + /\ + (* Sequence *) + (stmt_exec st (stmt_seq stmt1 stmt2) = + case stmt1 of + stmt_empty => + SOME (st, stmt2) + | _ => + (case stmt_exec st stmt1 of + SOME (st', stmt1') => + SOME (st', stmt_seq stmt1' stmt2) + | _ => NONE)) + /\ + (stmt_exec _ _ = NONE) +End + +Definition stmt_multi_exec_def: + (stmt_multi_exec (st, stmt) 0 = + SOME (st, stmt)) + /\ + (stmt_multi_exec (st, stmt) (SUC fuel) = + case stmt_exec st stmt of + SOME (st', stmt') => + stmt_multi_exec (st', stmt') fuel + | NONE => NONE) +End + +(******************************************) +(* Symbolic execution function parameters *) + +open symb_execTheory; + +(** imp_is_finished **) + +val stmt_empty_tm = prim_mk_const {Name="stmt_empty", Thy="imp"}; +fun is_stmt_empty tm = term_eq tm stmt_empty_tm; + +(* From p4_testLib.sml, should be moved to symbexec library? *) +fun the_final_state_imp step_thm = + optionSyntax.dest_some $ snd $ dest_eq $ snd $ dest_imp $ concl step_thm; + +fun imp_is_finished step_thm = + let + val state = the_final_state_imp step_thm + val (store, statement) = pairSyntax.dest_pair state + in + is_stmt_empty statement + end +; + + +(** imp_regular_step **) + +val (stmt_multi_exec_tm, _, dest_stmt_multi_exec, is_stmt_multi_exec) = + syntax_fns2 "imp" "stmt_multi_exec"; +val mk_stmt_multi_exec = + (fn (state, fuel) => (#2 (syntax_fns2 "imp" "stmt_multi_exec")) (state, numSyntax.term_of_int fuel)); + +(* From p4_testLib.sml, should be moved to symbexec library? *) +fun the_final_state_hyp_imp step_thm = + let + val (hyp, step_tm) = dest_imp $ concl step_thm + in + (hyp, optionSyntax.dest_some $ snd $ dest_eq step_tm) + end +; + +fun mk_exec n = (fn state => mk_stmt_multi_exec (state, n)); + +(* TODO: Test freezing compset *) +fun imp_norewr_eval_ctxt st = EVAL (mk_exec 1 st); + +open evalwrapLib; + +fun imp_eval_ctxt path_cond state = + eval_ctxt_gen [] [] (ASSUME path_cond) (mk_exec 1 state) +; + +(* TODO: Put in generic symb_execLib? *) +val simple_arith_ss = pure_ss++numSimps.REDUCE_ss; + +Theorem stmt_multi_exec_add: +!st stmt m n. +stmt_multi_exec (st, stmt) (m+n) = + case stmt_multi_exec (st, stmt) n of + | SOME (st', stmt') => + stmt_multi_exec (st', stmt') m + | NONE => NONE +Proof +Induct_on `n` >- ( + fs [stmt_multi_exec_def] +) >> +rpt strip_tac >> +fs [stmt_multi_exec_def, arithmeticTheory.ADD_CLAUSES] >> +Cases_on `stmt_exec st stmt` >> ( + fs [] +) >> +PairCases_on `x` >> +fs [] +QED + +Theorem stmt_multi_exec_comp_n_tl_assl: +!n m assl st stmt st' stmt' st'' stmt''. +(assl ==> stmt_multi_exec (st, stmt) n = SOME (st', stmt')) ==> +(assl ==> stmt_multi_exec (st', stmt') m = SOME (st'', stmt'')) ==> +(assl ==> stmt_multi_exec (st, stmt) (n+m) = SOME (st'', stmt'')) +Proof +rpt strip_tac >> +gs [] >> +fs [stmt_multi_exec_add] +QED + +Theorem stmt_multi_exec_comp_n_tl_assl_conj: +!n m assl st stmt st' stmt' st'' stmt''. +((assl ==> stmt_multi_exec (st, stmt) n = SOME (st', stmt')) /\ + (assl ==> stmt_multi_exec (st', stmt') m = SOME (st'', stmt''))) ==> +(assl ==> stmt_multi_exec (st, stmt) (n+m) = SOME (st'', stmt'')) +Proof +metis_tac[stmt_multi_exec_comp_n_tl_assl] +QED + +Theorem stmt_multi_exec_comp_n_tl_assl_conj_nomidassl: +!n m assl st stmt st' stmt' st'' stmt''. +((assl ==> stmt_multi_exec (st, stmt) n = SOME (st', stmt')) /\ + (stmt_multi_exec (st', stmt') m = SOME (st'', stmt''))) ==> +(assl ==> stmt_multi_exec (st, stmt) (n+m) = SOME (st'', stmt'')) +Proof +metis_tac[stmt_multi_exec_comp_n_tl_assl_conj] +QED + +fun imp_regular_step branch_just_happened step_thm = + let + val (ante, st) = the_final_state_hyp_imp step_thm + val step_thm2 = + if branch_just_happened + then imp_eval_ctxt ante st + else imp_norewr_eval_ctxt st + in + let + val res = + SIMP_RULE simple_arith_ss [] + (if branch_just_happened + then + (MATCH_MP stmt_multi_exec_comp_n_tl_assl_conj (CONJ step_thm step_thm2)) + else + (MATCH_MP stmt_multi_exec_comp_n_tl_assl_conj_nomidassl (CONJ step_thm step_thm2))) + in + res + end + end +; + + +(** imp_should_branch **) + +val (stmt_cond_tm, mk_stmt_cond, dest_stmt_cond, is_stmt_cond) = + syntax_fns3 "imp" "stmt_cond"; +val (stmt_seq_tm, mk_stmt_seq, dest_stmt_seq, is_stmt_seq) = + syntax_fns2 "imp" "stmt_seq"; +val (e_v_tm, mk_e_v, dest_e_v, is_e_v) = + syntax_fns1 "imp" "e_v"; +val (v_bool_tm, mk_v_bool, dest_v_bool, is_v_bool) = + syntax_fns1 "imp" "v_bool"; + +fun stmt_get_next stmt = + if is_stmt_seq stmt + then stmt_get_next $ fst $ dest_stmt_seq stmt + else stmt +; + +datatype branch_data = + no_branch + | conditional of term; + +fun state_get_branch_data state = + let + val (store, stmt) = pairSyntax.dest_pair state + val stmt' = stmt_get_next stmt + in + if is_stmt_cond stmt' + then conditional $ #1 $ dest_stmt_cond stmt' + else no_branch + end +; + +fun imp_should_branch (fv_index:int, step_thm) = + let + val (_, state) = the_final_state_hyp_imp step_thm + val res = + (* + val conditional branch_cond = it + *) + (case state_get_branch_data state of + conditional branch_cond => + if is_e_v branch_cond andalso not $ null $ free_vars branch_cond + then + let + val branch_cond' = dest_v_bool $ dest_e_v branch_cond + in + SOME (SPEC branch_cond' disj_list_EXCLUDED_MIDDLE, [fv_index, fv_index]) + end + else NONE + | no_branch => NONE) + in + res + end +; + + +fun get_init_step_thm path_cond init_st init_stmt = + (eval_ctxt_gen [] [] (ASSUME path_cond) (mk_exec 0 “(^init_st, ^init_stmt)”)) +; + +(*************************************************************) +(* AbsMinus (toy example adapted from Gordon and Collavizza) + * https://hal.science/hal-03015714/document *) + +val toy_program = “stmt_seq (stmt_ass "k" (e_v $ v_num 0)) + (stmt_seq (stmt_cond (e_uop uop_neg (e_bop (e_var "j") bop_lt (e_var "i"))) (stmt_ass "k" (e_bop (e_var "k") bop_add (e_v $ v_num 1))) stmt_empty) + (stmt_cond (e_bop (e_bop (e_var "k") bop_eq (e_v $ v_num 1)) bop_and (e_uop uop_neg $ e_bop (e_var "i") bop_eq (e_var "j"))) + (stmt_ass "result" (e_bop (e_var "j") bop_sub (e_var "i"))) + (stmt_ass "result" (e_bop (e_var "i") bop_sub (e_var "j")))))” +val toy_init_state = “[("i", v_num i); ("j", v_num j); ("Result", v_num Result); ("result", v_num result)]” + +val toy_loop = “stmt_while (e_bop (e_var "a") bop_lt (e_var "b")) + (stmt_ass "a" (e_bop (e_var "a") bop_add (e_v $ v_num 1)))” + +(*****************) +(* Performing symbolic execution *) +val init_step_thm = get_init_step_thm T toy_init_state toy_program +val debug_flag = true +val path_cond = ASSUME T +val fuel = 50 + +open symb_execLib; + +val (res_path_tree, path_cond_step_list) = symb_exec (debug_flag, imp_regular_step, init_step_thm, imp_should_branch, imp_is_finished) path_cond fuel + + +(* Proving the postcondition *) +val postcond = + “\s:(string # imp$v) list # imp$stmt. (i < j ==> ALOOKUP (FST s) "result" = SOME (v_num (j - i))) /\ + (i >= j ==> ALOOKUP (FST s) "result" = SOME (v_num (i - j)))” + +fun prove_postcond postcond step_thm = + let + val prel_res_thm = HO_MATCH_MP symb_exec_add_postcond step_thm + val (hypo, step_tm) = dest_imp $ concl step_thm + val res_state_tm = optionSyntax.dest_some $ snd $ dest_eq step_tm + val postcond_thm = EQT_ELIM $ (computeLib.EVAL_CONV THENC (SIMP_CONV (srw_ss()) []) THENC numLib.ARITH_CONV) $ mk_imp (hypo, mk_comb (postcond, res_state_tm)) + in + MATCH_MP prel_res_thm postcond_thm + end +; + +fun prove_postconds_debug' postcond [] _ = [] + | prove_postconds_debug' postcond (h::t) n = + let + val res = prove_postcond postcond h + handle exc => (print (("Error when proving postcondition for n-step theorem at 0-index "^(Int.toString n))^"\n"); raise exc) + in + (res::(prove_postconds_debug' postcond t (n + 1))) + end +; +fun prove_postconds debug_flag postcond path_cond_step_list = + if debug_flag + then + let + val (l', l'') = unzip $ map (fn (a,b,c) => (a, c)) path_cond_step_list + in + zip l' (prove_postconds_debug' postcond l'' 0) + end + else map (fn (a,b,c) => (a, prove_postcond postcond c)) path_cond_step_list +; + +prove_postconds debug_flag postcond path_cond_step_list; + +val _ = export_theory(); diff --git a/hol/symb_exec/p4_symb_execLib.sml b/hol/symb_exec/p4_symb_execLib.sml index f0f7bad6..59943987 100644 --- a/hol/symb_exec/p4_symb_execLib.sml +++ b/hol/symb_exec/p4_symb_execLib.sml @@ -2238,17 +2238,18 @@ SUBST_MATCH (GSYM (ASSUME eq_tm)) test_thm (******************) (* p4_is_finished *) (* Function that decides whether a HOL4P4 program is finished or not: - * here, when processing of all symbolic input packets are finished. + * here, when block n is reached. 0 signifies that processing of all + * symbolic input packets are finished. * Used as a default when no other function is specified. *) -fun p4_is_finished step_thm = +fun p4_is_finished n step_thm = let val astate = the_final_state_imp step_thm val (aenv, _, _, _) = dest_astate astate val (i, io_list, _, _) = dest_aenv aenv in - (* Whenever the result of taking one step is at block index 0 with no further input - * in the input queue, we're finished *) - if int_of_term i = 0 andalso null $ fst $ dest_list io_list + (* Whenever the result of taking one step is at block index n with no + * further input in the input queue, we're finished *) + if int_of_term i = n andalso null $ fst $ dest_list io_list then true else false end @@ -2301,7 +2302,7 @@ fun p4_symb_exec nthreads_max debug_flag arch_ty (ctx_def, ctx) (fty_map, b_fty_ val is_finished = if isSome p4_is_finished_alt_opt then valOf p4_is_finished_alt_opt - else p4_is_finished + else (p4_is_finished 0) in (* DEBUG: val lang_regular_step = p4_regular_step (debug_flag, ctx_def, ctx, norewr_eval_ctxt, eval_ctxt) comp_thm; diff --git a/hol/symb_exec/symb_execLib.sml b/hol/symb_exec/symb_execLib.sml index 96aeac19..459041ab 100644 --- a/hol/symb_exec/symb_execLib.sml +++ b/hol/symb_exec/symb_execLib.sml @@ -495,7 +495,7 @@ val rewr_thms = rewr_thms@[lookup_v_def, lookup_map_def, topmost_map_def, find_t open p4Theory; *) -(* TODO: This should take a HOL4P4_CONV *) +(* TODO: This should take a custom CONV *) fun prove_postcond rewr_thms simpset postcond step_thm = let val prel_res_thm = HO_MATCH_MP symb_exec_add_postcond step_thm diff --git a/hol/symb_exec/tests/conditionalScript.sml b/hol/symb_exec/tests/conditionalScript.sml index 31ab17bf..0a6d2d67 100644 --- a/hol/symb_exec/tests/conditionalScript.sml +++ b/hol/symb_exec/tests/conditionalScript.sml @@ -134,7 +134,7 @@ val symb_exec1_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [([e1; e ("action_run",v_bit (REPLICATE 32 ARB,32))],NONE)]], arch_frame_list_empty,status_running):v1model_ascope astate”; -(* symb_exec: *) + (* Parameter assignment for debugging: *) val debug_flag = false; val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -152,6 +152,7 @@ val n_max = 50; val postcond = “(\s. packet_has_port s 1 \/ packet_has_port s 2):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] val postcond_simpset = pure_ss + (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl @@ -168,7 +169,7 @@ val (path_tree, [(path_id, path_cond, step_thm)]) = (* For debugging, branch happens here: val (path_tree, [(path_id, path_cond, step_thm)]) = - p4_symb_exec 1 true arch_ty (ctx_def, ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables init_astate stop_consts_rewr stop_consts_never [] path_cond NONE 24; + p4_symb_exec 1 true arch_ty (ctx_def, ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond NONE 19; val (path_tree, [(path_id, path_cond, step_thm), (path_id2, path_cond2, step_thm2)]) = p4_symb_exec 1 true arch_ty (ctx_def, ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables init_astate stop_consts_rewr stop_consts_never [] path_cond NONE 25; @@ -187,27 +188,4 @@ val (res_id1, res_cond1, res_thm1) = res_elem1 * (higher numbers as arguments will work, but do no extra computations) *) val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; -(* - -val path_cond = (ASSUME T); -val n_max = 50; -val postcond = “(\s. packet_has_port s 1 \/ packet_has_port s 2):v1model_ascope astate -> bool”; -val nthreads_max = 1; -val debug_flag = false; -val fuel = 100 - - val ctx_name = "ctx" - val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn ctx_name (mk_eq(mk_var(ctx_name, type_of ctx), ctx)) - - val table_stop_consts = [match_all_tm] - val eval_ctxt = p4_eval_ctxt_gen ((stop_consts_rewr@stop_consts_never@p4_stop_eval_consts@table_stop_consts), (stop_consts_never@p4_stop_eval_consts), (fn astate => mk_arch_multi_exec (ctx, astate, 1))) - -val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl - - val p4_init_step_thm = eval_ctxt_gen (stop_consts_rewr@stop_consts_never) stop_consts_never path_cond (mk_arch_multi_exec (ctx, init_astate, 0)) - -symb_exec_conc (p4_regular_step (debug_flag, ctx_def, ctx, eval_ctxt) comp_thm, p4_init_step_thm, p4_should_branch, p4_is_finished) path_cond fuel 4 - -*) - val _ = export_theory (); diff --git a/hol/symb_exec/tests/conditional_thenScript.sml b/hol/symb_exec/tests/conditional_thenScript.sml index e39e6202..59d1575b 100644 --- a/hol/symb_exec/tests/conditional_thenScript.sml +++ b/hol/symb_exec/tests/conditional_thenScript.sml @@ -136,7 +136,6 @@ val symb_exec2_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [([e1; e arch_frame_list_empty,status_running):v1model_ascope astate”; -(* symb_exec: *) (* Parameter assignment for debugging: *) val debug_flag = false val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -155,6 +154,7 @@ val n_max = 50; val postcond = “(\s. packet_has_port s 1):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] val postcond_simpset = pure_ss + (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl *) diff --git a/hol/symb_exec/tests/decomposeScript.sml b/hol/symb_exec/tests/decomposeScript.sml index 79479c58..2d8ecdf9 100644 --- a/hol/symb_exec/tests/decomposeScript.sml +++ b/hol/symb_exec/tests/decomposeScript.sml @@ -135,7 +135,7 @@ val symb_exec1_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [([e1; e ("action_run",v_bit (REPLICATE 32 ARB,32))],NONE)]], arch_frame_list_empty,status_running):v1model_ascope astate”; -(* symb_exec: *) + (* Parameter assignment for debugging: *) val debug_flag = false; val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -159,8 +159,6 @@ val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] val block_index_stop = “2:num” val p4_is_finished_alt_opt1 = SOME (fn step_thm => Teq $ rhs $ concl $ EVAL “p4_block_next ^(optionSyntax.dest_some $ rhs $ snd $ dest_imp $ concl step_thm) ^block_index_stop”); - -(* TODO: Why does the initial state not have anything mapped to by ext reference 1? *) (* Get well-formedness property after parser block just finished *) val p4_v1model_parser_wellformed_def = (fn defn => let val _ = Defn.save_defn defn in Defn.fetch_eqns defn end) $ get_v1model_wellformed_defs ctx init_astate block_index_stop; val postcond_simpset = (pure_ss++(p4_wellformed_ss p4_v1model_parser_wellformed_def)) @@ -183,7 +181,6 @@ val postcond1 = “(\s. p4_v1model_parser_wellformed s /\ p4_v1model_lookup_avar_validity (lval_field (lval_varname (varn_name "hdr")) "h") s = SOME T *) ):v1model_ascope astate -> bool”; (* (* If block_index_stop is 5 or later *) -(* TODO: Problems when using disjunctions: "egress_spec is either 1 or 2" *) val postcond1 = “(\s. p4_v1model_parser_wellformed s /\ p4_v1model_lookup_avar (lval_field (lval_field (lval_field (lval_varname (varn_name "parsedHdr")) "h") "row") "e") s = SOME $ v_bit ([e1; e2; e3; e4; e5; e6; e7; e8],8) /\ (p4_v1model_lookup_avar (lval_field (lval_varname (varn_name "standard_meta")) "egress_spec") s = SOME $ v_bit ([F; F; F; F; F; F; F; F; T],9) \/ @@ -208,17 +205,15 @@ val contract_thm1 = p4_symb_exec_prove_contract debug_flag arch_ty (def_thm ctx_ val init_astate2 = get_intermediate_state postcond1 p4_v1model_parser_wellformed_def; (* 3. Prove a contract from the intermediate to final state *) -(* TODO: Contact unification fails when disjunctions in the path condition are involved. - * Use simpset for p4_v1model_lookup_avar and similar? - * Also, the initial path condition should maybe be the initial path condition combined with - * the postcondition? *) val contract_thm2 = p4_symb_exec_prove_contract debug_flag arch_ty (def_thm ctx_def) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate2 stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; (* 4. Combine the contracts *) -(* +(* DEBUG + val contract1 = contract_thm1 val contract2 = contract_thm2 val wellformed_def = p4_v1model_parser_wellformed_def + *) val combined_contract = p4_combine_contracts contract_thm1 contract_thm2 p4_v1model_parser_wellformed_def; diff --git a/hol/symb_exec/tests/register_readScript.sml b/hol/symb_exec/tests/register_readScript.sml index b3e0a9c8..986e9f95 100644 --- a/hol/symb_exec/tests/register_readScript.sml +++ b/hol/symb_exec/tests/register_readScript.sml @@ -270,11 +270,10 @@ val b_fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_b val symb_exec7_ctx_tm = “(^fty_map', ^b_fty_map', ^symb_exec7_pblock_action_names_map)” val symb_exec_ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "symb_exec_ctx" (mk_eq(mk_var("symb_exec_ctx", type_of symb_exec7_ctx_tm), symb_exec7_ctx_tm)) -(* TODO: Not needed? *) val symb_exec7_pblock_map = #2 $ p4Syntax.dest_actx symb_exec7_actx; val symb_exec_pblock_map_def = hd $ Defn.eqns_of $ Defn.mk_defn "pblock_map" (mk_eq(mk_var("pblock_map", type_of symb_exec7_pblock_map), symb_exec7_pblock_map)) -(* symb_exec: *) + (* Parameter assignment for debugging: *) val debug_flag = false; val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -294,7 +293,8 @@ val fuel = 1; val postcond_rewr_thms = [] val postcond_simpset = pure_ss -val time_start = Time.now(); (* +val time_start = Time.now(); +(* val p4_symb_exec_fun = (p4_symb_exec 1) *) val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; diff --git a/hol/symb_exec/tests/register_read_writeScript.sml b/hol/symb_exec/tests/register_read_writeScript.sml index 5638dbad..fe37d652 100644 --- a/hol/symb_exec/tests/register_read_writeScript.sml +++ b/hol/symb_exec/tests/register_read_writeScript.sml @@ -289,11 +289,10 @@ val b_fty_map' = optionSyntax.dest_some $ rhs $ concl $ EVAL “deparameterise_b val symb_exec8_ctx_tm = “(^fty_map', ^b_fty_map', ^symb_exec8_pblock_action_names_map)” val symb_exec_ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "symb_exec_ctx" (mk_eq(mk_var("symb_exec_ctx", type_of symb_exec8_ctx_tm), symb_exec8_ctx_tm)) -(* TODO: Not needed? *) val symb_exec8_pblock_map = #2 $ p4Syntax.dest_actx symb_exec8_actx; val symb_exec_pblock_map_def = hd $ Defn.eqns_of $ Defn.mk_defn "pblock_map" (mk_eq(mk_var("pblock_map", type_of symb_exec8_pblock_map), symb_exec8_pblock_map)) -(* symb_exec: *) + (* Parameter assignment for debugging: *) val debug_flag = true; val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -313,7 +312,8 @@ val fuel = 1; val postcond_rewr_thms = [] val postcond_simpset = pure_ss -val time_start = Time.now(); (* +val time_start = Time.now(); +(* val p4_symb_exec_fun = (p4_symb_exec 1) *) val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; diff --git a/hol/symb_exec/tests/selectScript.sml b/hol/symb_exec/tests/selectScript.sml index 2e3e372d..8f4d6137 100644 --- a/hol/symb_exec/tests/selectScript.sml +++ b/hol/symb_exec/tests/selectScript.sml @@ -144,7 +144,6 @@ val symb_exec3_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [([e1; e arch_frame_list_empty,status_running):v1model_ascope astate”; -(* symb_exec: *) (* Parameter assignment for debugging: *) val debug_flag = false val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -161,6 +160,7 @@ val n_max = 50; val postcond = “(\s. packet_has_port s 1):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] val postcond_simpset = pure_ss + (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl *) diff --git a/hol/symb_exec/tests/table_knownScript.sml b/hol/symb_exec/tests/table_knownScript.sml index d6c4dc16..1cae5786 100644 --- a/hol/symb_exec/tests/table_knownScript.sml +++ b/hol/symb_exec/tests/table_knownScript.sml @@ -175,7 +175,6 @@ val symb_exec4_astate_symb = rhs $ concl $ EVAL ``p4_append_input_list [([e1; e2 arch_frame_list_empty,status_running):v1model_ascope astate``; -(* symb_exec: *) (* Parameter assignment for debugging: *) val arch_ty = p4_v1modelLib.v1model_arch_ty val ctx = symb_exec4_actx @@ -188,6 +187,7 @@ val n_max = 50; val postcond = “(\s. packet_has_port s 42 \/ packet_has_port s 101):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] val postcond_simpset = pure_ss + (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl val init_step_thm = eval_ctxt_gen (stop_consts_rewr@stop_consts_never) stop_consts_never path_cond (mk_arch_multi_exec (ctx, init_astate, 0)) diff --git a/hol/symb_exec/tests/table_known_fourScript.sml b/hol/symb_exec/tests/table_known_fourScript.sml index f165c8c2..9266a171 100644 --- a/hol/symb_exec/tests/table_known_fourScript.sml +++ b/hol/symb_exec/tests/table_known_fourScript.sml @@ -190,7 +190,7 @@ val symb_exec5_astate_symb = rhs $ concl $ EVAL ``p4_append_input_list [([e1; e2 ("action_run",v_bit (REPLICATE 32 ARB,32))],NONE)]], arch_frame_list_empty,status_running):v1model_ascope astate``; -(* symb_exec: *) + (* Parameter assignment for debugging: *) val debug_flag = false val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -207,6 +207,7 @@ val postcond = “(\s. packet_has_port s 42 \/ packet_has_port s 101):v1model_ascope astate -> bool”; val postcond_rewr_thms = [p4_symb_execTheory.packet_has_port_def] val postcond_simpset = pure_ss + (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl val init_step_thm = eval_ctxt_gen (stop_consts_rewr@stop_consts_never) stop_consts_never path_cond (mk_arch_multi_exec (ctx, init_astate, 0)) diff --git a/hol/symb_exec/tests/table_unknownScript.sml b/hol/symb_exec/tests/table_unknownScript.sml index 862ba593..4f97c191 100644 --- a/hol/symb_exec/tests/table_unknownScript.sml +++ b/hol/symb_exec/tests/table_unknownScript.sml @@ -247,7 +247,7 @@ val symb_exec6_ctrl = #4 $ p4_v1modelLib.dest_v1model_ascope $ #4 $ p4Syntax.des val symb_exec6_wf_tm = “v1model_ctrl_is_well_formed ^(lhs $ concl symb_exec_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) (^symb_exec6_ctrl)” val symb_exec6_wf_tbl_tm = “v1model_tbl_is_well_formed ^(lhs $ concl symb_exec_ctx_def) ^(lhs $ concl symb_exec_pblock_map_def) ("t2",t2_ctrl)” -(* symb_exec: *) + (* Parameter assignment for debugging: *) val debug_flag = false; val arch_ty = p4_v1modelLib.v1model_arch_ty @@ -266,6 +266,7 @@ val postcond = “(\s. T):v1model_ascope astate -> bool”; val fuel = 1; val postcond_rewr_thms = [] val postcond_simpset = pure_ss + (* For debugging: val comp_thm = INST_TYPE [Type.alpha |-> arch_ty] p4_exec_semTheory.arch_multi_exec_comp_n_tl_assl val init_step_thm = eval_ctxt_gen (stop_consts_rewr@stop_consts_never) stop_consts_never path_cond (mk_arch_multi_exec (ctx, init_astate, 0)) @@ -305,7 +306,8 @@ val step_thm = step_thm2; *) -val time_start = Time.now(); (* +val time_start = Time.now(); +(* val p4_symb_exec_fun = (p4_symb_exec 1) *) val contract_thm = p4_symb_exec_prove_contract debug_flag arch_ty (def_term ctx) (fty_map, b_fty_map, pblock_action_names_map) const_actions_tables path_cond_defs init_astate stop_consts_rewr stop_consts_never [] path_cond p4_is_finished_alt_opt n_max postcond postcond_rewr_thms postcond_simpset; From c606a07a99435149a4b812c070741fb6e8c2d417 Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Thu, 10 Oct 2024 17:00:59 +0200 Subject: [PATCH 3/3] More things from dev_select_tna6 --- hol/p4_coreScript.sml | 20 ++++ hol/p4_v1modelLib.sig | 5 + hol/p4_v1modelLib.sml | 3 + hol/p4_v1modelScript.sml | 18 ++-- hol/symb_exec/README.md | 2 + hol/symb_exec/example_ipsec/basicScript.sml | 34 +----- .../example_ipsec/basic_altScript.sml | 34 +----- hol/symb_exec/p4_symb_execLib.sml | 102 +----------------- hol/symb_exec/p4_symb_execScript.sml | 7 ++ hol/symb_exec/p4_symb_exec_v1modelLib.sig | 2 + hol/symb_exec/p4_symb_exec_v1modelLib.sml | 23 ++++ hol/symb_exec/symb_execLib.sig | 2 +- hol/symb_exec/symb_execLib.sml | 23 ++-- 13 files changed, 95 insertions(+), 180 deletions(-) diff --git a/hol/p4_coreScript.sml b/hol/p4_coreScript.sml index 6052a2e0..0accd15f 100644 --- a/hol/p4_coreScript.sml +++ b/hol/p4_coreScript.sml @@ -425,6 +425,26 @@ Definition get_checksum_incr_def: ) End +(* Alternative version tailored for symbolic execution *) +Definition get_checksum_incr'_def: + (get_checksum_incr' scope_list ext_data_name = + (case lookup_lval scope_list ext_data_name of + | SOME (v_bit (bl, n)) => + if n MOD 16 = 0 then SOME bl else NONE + | SOME (v_header vbit f_list) => + (case header_entries2v f_list of + | SOME bl => + if (LENGTH bl) MOD 16 = 0 then SOME bl else NONE + | NONE => NONE) + | SOME (v_struct f_list) => + (case header_entries2v f_list of + | SOME bl => + if (LENGTH bl) MOD 16 = 0 then SOME bl else NONE + | NONE => NONE) + | _ => NONE) + ) +End + Definition add_ones_complement_def: add_ones_complement (x, y) = let diff --git a/hol/p4_v1modelLib.sig b/hol/p4_v1modelLib.sig index c3e4d62b..4b82005b 100644 --- a/hol/p4_v1modelLib.sig +++ b/hol/p4_v1modelLib.sig @@ -42,4 +42,9 @@ val is_v1model_register_write_inner : term -> bool val mk_v1model_register_write_inner : term * term * term -> term val v1model_register_write_inner_tm : term +val dest_v1model_update_checksum_inner : term -> term +val is_v1model_update_checksum_inner : term -> bool +val mk_v1model_update_checksum_inner : term -> term +val v1model_update_checksum_inner_tm : term + end diff --git a/hol/p4_v1modelLib.sml b/hol/p4_v1modelLib.sml index 0c065cc4..3e0c434b 100644 --- a/hol/p4_v1modelLib.sml +++ b/hol/p4_v1modelLib.sml @@ -103,4 +103,7 @@ val (v1model_register_read_inner_tm, mk_v1model_register_read_inner, dest_v1mod val (v1model_register_write_inner_tm, mk_v1model_register_write_inner, dest_v1model_register_write_inner, is_v1model_register_write_inner) = syntax_fns3 "p4_v1model" "v1model_register_write_inner"; +val (v1model_update_checksum_inner_tm, mk_v1model_update_checksum_inner, dest_v1model_update_checksum_inner, is_v1model_update_checksum_inner) = + syntax_fns1 "p4_v1model" "v1model_update_checksum_inner"; + end diff --git a/hol/p4_v1modelScript.sml b/hol/p4_v1modelScript.sml index cf1c2886..5914897e 100644 --- a/hol/p4_v1modelScript.sml +++ b/hol/p4_v1modelScript.sml @@ -237,6 +237,11 @@ End (*************************) (* update_checksum *) +Definition v1model_update_checksum_inner_def: + v1model_update_checksum_inner bitlist = + v_bit $ w16 $ compute_checksum16 $ v2w16s' bitlist +End + Definition v1model_update_checksum_def: (v1model_update_checksum ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) = (case lookup_lval scope_list (lval_varname (varn_name "condition")) of @@ -247,13 +252,14 @@ Definition v1model_update_checksum_def: | SOME $ v_bit (bl, n) => if v2n bl = 6 then - (case get_checksum_incr scope_list (lval_varname (varn_name "data")) of + (case get_checksum_incr' scope_list (lval_varname (varn_name "data")) of | SOME checksum_incr => (case lookup_lval scope_list (lval_varname (varn_name "checksum")) of | SOME $ v_bit (bl', n') => if n' = 16 then - (case assign scope_list (v_bit $ w16 $ compute_checksum16 checksum_incr) (lval_varname (varn_name "checksum")) of + (* TODO: This can be made total, since we just looked up the checksum *) + (case assign scope_list (v1model_update_checksum_inner checksum_incr) (lval_varname (varn_name "checksum")) of | SOME scope_list' => SOME ((counter, ext_obj_map, v_map, ctrl), scope_list', status_returnv v_bot) | NONE => NONE) else NONE @@ -412,8 +418,6 @@ Termination METIS_TAC [v1_size_mem] End -(* TODO: This is currently a placeholder implementation. - * For symbolic execution. This should be rewritten by adding an assumption that introduces fresh free variables *) Definition ipsec_crypt_decrypt_aes_ctr_def: (ipsec_crypt_decrypt_aes_ctr ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) = case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of @@ -438,8 +442,6 @@ Definition ipsec_crypt_decrypt_aes_ctr_def: ) End -(* TODO: This is currently a placeholder implementation. - * For symbolic execution. This should be rewritten by adding an assumption that introduces fresh free variables *) Definition ipsec_crypt_encrypt_aes_ctr_def: (ipsec_crypt_encrypt_aes_ctr ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) = case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of @@ -458,8 +460,6 @@ Definition ipsec_crypt_encrypt_aes_ctr_def: ) End -(* TODO: This is currently a placeholder implementation. - * For symbolic execution. This should be rewritten by adding an assumption that introduces fresh free variables *) Definition ipsec_crypt_encrypt_null_def: (ipsec_crypt_encrypt_null ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) = case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of @@ -478,8 +478,6 @@ Definition ipsec_crypt_encrypt_null_def: ) End -(* TODO: This is currently a placeholder implementation. - * For symbolic execution. This should be rewritten by adding an assumption that introduces fresh free variables *) Definition ipsec_crypt_decrypt_null_def: (ipsec_crypt_decrypt_null ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) = case lookup_lval scope_list (lval_varname (varn_name "ipv4")) of diff --git a/hol/symb_exec/README.md b/hol/symb_exec/README.md index 56e8e3d7..b5f1d4e8 100644 --- a/hol/symb_exec/README.md +++ b/hol/symb_exec/README.md @@ -85,3 +85,5 @@ and send everything to the REPL to observe debug output of what's going on. A mid-size example can be found in `example_ipsec` subdirectory. The Python script `count_reds.py` can be used on the debug output to generate statistics about the symbolic execution. + +The `imp` subdirectory contains an instantiation of the symbolic executor for a simple imperative language with loops. diff --git a/hol/symb_exec/example_ipsec/basicScript.sml b/hol/symb_exec/example_ipsec/basicScript.sml index bb6e06e6..58293548 100644 --- a/hol/symb_exec/example_ipsec/basicScript.sml +++ b/hol/symb_exec/example_ipsec/basicScript.sml @@ -1299,35 +1299,7 @@ val input = rhs $ concl $ EVAL “^eth_input ++ (^ipv4_input ++ ^esp_input)”; val basic_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [(^input,0)] ^basic_astate”; - -(* RE-DEFINITIONS OF TROUBLESOME EXTERNS *) - -Definition v1model_update_checksum'_def: - (v1model_update_checksum' ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) = - case assign scope_list (v_bit $ ((REPLICATE 16 (ARB:bool)), 16)) (lval_varname (varn_name "checksum")) of - | SOME scope_list' => - SOME ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, scope_list', status_returnv v_bot) - | NONE => NONE - ) -End - -val pre_ctx = basic_actx; - -(* TODO: Move *) -fun replace_ext_impls ctx_tm [] = ctx_tm - | replace_ext_impls ctx_tm ((ext_name, method_name, method_tm)::t) = - let - val ctx_tm' = replace_ext_impl ctx_tm ext_name method_name method_tm - in - replace_ext_impls ctx_tm' t - end -; - -Definition ctx'_def: - ctx' = ^(replace_ext_impls pre_ctx [("", "update_checksum", “v1model_update_checksum'”)]) -End - -val ctx = rhs $ concl $ EVAL ``ctx'``; +val ctx = basic_actx; val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "basic_ctx" (mk_eq(mk_var("basic_ctx", type_of ctx), ctx)); @@ -1359,9 +1331,9 @@ val const_actions_tables = []; val arch_ty = p4_v1modelLib.v1model_arch_ty val path_cond_defs = [symb_exec_ty_ctx_def, symb_exec_pblock_map_def] val init_astate = basic_astate_symb -val stop_consts_rewr = [“v1model_is_drop_port”, “v1model_register_construct_inner”, “v1model_register_read_inner”, “v1model_register_write_inner”] +val stop_consts_rewr = [“v1model_is_drop_port”, “v1model_register_construct_inner”, “v1model_register_read_inner”, “v1model_register_write_inner”, “v1model_update_checksum_inner”] val stop_consts_never = [] -val thms_to_add = [v1model_update_checksum'_def] +val thms_to_add = [] val path_cond = ASSUME “^basic_wf_sad_encrypt_tbl_tm /\ ^basic_wf_sad_decrypt_tbl_tm /\ ^basic_wf_forward_tbl_tm /\ diff --git a/hol/symb_exec/example_ipsec/basic_altScript.sml b/hol/symb_exec/example_ipsec/basic_altScript.sml index f2d2de05..8c2a07ba 100644 --- a/hol/symb_exec/example_ipsec/basic_altScript.sml +++ b/hol/symb_exec/example_ipsec/basic_altScript.sml @@ -1330,35 +1330,7 @@ val input = rhs $ concl $ EVAL “^eth_input ++ (^ipv4_input ++ ^esp_input)”; val basic_alt_astate_symb = rhs $ concl $ EVAL “p4_append_input_list [(^input,0)] ^basic_alt_astate”; - -(* RE-DEFINITIONS OF TROUBLESOME EXTERNS *) - -Definition v1model_update_checksum'_def: - (v1model_update_checksum' ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, g_scope_list:g_scope_list, scope_list) = - case assign scope_list (v_bit $ ((REPLICATE 16 (ARB:bool)), 16)) (lval_varname (varn_name "checksum")) of - | SOME scope_list' => - SOME ((counter, ext_obj_map, v_map, ctrl):v1model_ascope, scope_list', status_returnv v_bot) - | NONE => NONE - ) -End - -val pre_ctx = basic_alt_actx; - -(* TODO: Move *) -fun replace_ext_impls ctx_tm [] = ctx_tm - | replace_ext_impls ctx_tm ((ext_name, method_name, method_tm)::t) = - let - val ctx_tm' = replace_ext_impl ctx_tm ext_name method_name method_tm - in - replace_ext_impls ctx_tm' t - end -; - -Definition ctx'_def: - ctx' = ^(replace_ext_impls pre_ctx [("", "update_checksum", “v1model_update_checksum'”)]) -End - -val ctx = rhs $ concl $ EVAL ``ctx'``; +val ctx = basic_alt_actx; val ctx_def = hd $ Defn.eqns_of $ Defn.mk_defn "basic_alt_ctx" (mk_eq(mk_var("basic_alt_ctx", type_of ctx), ctx)); (* Additional parts of the context relevant only to symbolic execution *) @@ -1390,9 +1362,9 @@ val const_actions_tables = []; val arch_ty = p4_v1modelLib.v1model_arch_ty val path_cond_defs = [symb_exec_ty_ctx_def, symb_exec_pblock_map_def] val init_astate = basic_alt_astate_symb -val stop_consts_rewr = [“v1model_is_drop_port”, “v1model_register_construct_inner”, “v1model_register_read_inner”, “v1model_register_write_inner”] +val stop_consts_rewr = [“v1model_is_drop_port”, “v1model_register_construct_inner”, “v1model_register_read_inner”, “v1model_register_write_inner”, “v1model_update_checksum_inner”] val stop_consts_never = [] -val thms_to_add = [v1model_update_checksum'_def] +val thms_to_add = [] val path_cond = ASSUME “^basic_alt_wf_sad_encrypt_tbl_tm /\ ^basic_alt_wf_sad_decrypt_tbl_tm /\ ^basic_alt_wf_forward_tbl_tm /\ diff --git a/hol/symb_exec/p4_symb_execLib.sml b/hol/symb_exec/p4_symb_execLib.sml index 59943987..5f07fa37 100644 --- a/hol/symb_exec/p4_symb_execLib.sml +++ b/hol/symb_exec/p4_symb_execLib.sml @@ -753,7 +753,7 @@ val apply (tbl_name, e) = apply if (hurdUtils.forall is_e_v) (fst $ dest_list e) andalso (* Perform a symbolic branch if the apply expression (list) contains * free variables or ARBs (hack) *) - (not $ null $ free_vars e orelse HOLset.member (all_atoms e, “ARB:bool”)) + (not $ null $ free_vars e orelse HOLset.member (all_atoms e, mk_arb bool)) then let (* 1. Extract ctrl from ascope *) @@ -1080,7 +1080,6 @@ val array = “[([ARB:bool; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; AR end else if is_funn_ext funn then - (* TODO: What is going on here? Print debug output... *) let val (ext_obj_tm, ext_method_tm) = dest_funn_ext funn val ext_obj = stringSyntax.fromHOLstring ext_obj_tm @@ -1089,106 +1088,15 @@ val array = “[([ARB:bool; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; AR in if (ext_obj = "register") andalso (ext_method = "read") then approx_v1model_register_read p4_symb_arg_prefix fv_index scope_list ascope -(* - let - (* 1. Get first entry of register array (for entry width) *) - val array_index = fst $ dest_pair $ dest_v_bit $ dest_some $ rhs $ concl $ HOL4P4_CONV “lookup_lval ^scope_list (lval_varname (varn_name "index"))” - val ext_ref = dest_v_ext_ref $ dest_some $ rhs $ concl $ HOL4P4_CONV “lookup_lval ^scope_list (lval_varname (varn_name "this"))” - - val ascope = #4 $ dest_aenv aenv - (* TODO: V1Model *) - val ext_obj_map = #2 $ p4_v1modelLib.dest_v1model_ascope ascope - val array = snd $ dest_comb $ fst $ sumSyntax.dest_inr $ dest_some $ rhs $ concl $ HOL4P4_CONV “ALOOKUP ^ext_obj_map ^ext_ref” - (* TODO: Double-check this works *) - val entry_width = snd $ dest_pair $ dest_v_bit $ dest_some $ rhs $ concl $ HOL4P4_CONV “lookup_lval ^scope_list (lval_varname (varn_name "result"))” -(* - val entry_width = snd $ dest_pair $ rhs $ concl $ HOL4P4_CONV “EL 0 ^array” -*) - - (* 2. Prove approximation theorem *) - val tm1 = “v1model_register_read_inner ^entry_width ^array_index ^array” - (* TODO: Hack, make function that returns list *) - val approx_vars = fixedwidth_freevars_fromindex (p4_symb_arg_prefix, fv_index, int_of_term entry_width) - val rhs_tm = mk_pair (approx_vars, entry_width) - val goal_tm = mk_disj_list [list_mk_exists (fst $ dest_list approx_vars, mk_eq (tm1, rhs_tm))] - -(* Unless you cache, these have to be proved every single time *) -val list_var = mk_var("list", “:bool list”) -val list_hyp = mk_eq(mk_length list_var, entry_width) -val list_exists_thm = prove(mk_forall (list_var, mk_imp (list_hyp, list_mk_exists(fst $ dest_list approx_vars, mk_eq (list_var, approx_vars)))), -rpt strip_tac >> -rpt (goal_term (fn tm => tmCases_on (fst $ dest_eq $ snd $ strip_exists tm) []) >> FULL_SIMP_TAC list_ss []) -); - -(* -val old_array = array - -val array = “[([ARB:bool; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB],32); - ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB],32); - ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB],32)]” - -val array2 = “[([ARB:bool; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB],32); - ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB],32); - ([ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; ARB; - ARB; ARB; ARB; ARB; ARB; ARB],32)]” -*) - - val approx_thm = - (* “^goal_tm” *) - prove(mk_imp (“wellformed_register_array ^entry_width ^array”, goal_tm), - (* As soon as possible, hide the array, which may be big *) - markerLib.ABBREV_TAC “(array:(bool list # num) list) = ^array” >> - qpat_x_assum ‘Abbrev (array = _)’ (fn thm => markerLib.hide_tac "big_array" thm) >> - (* TODO: V1Model hack *) - SIMP_TAC std_ss [disj_list_def, p4_v1modelTheory.v1model_register_read_inner_def] >> -(* - subgoal ‘wellformed_register_array ^entry_width array’ >- ( - markerLib.unhide_tac "big_array" >> - markerLib.UNABBREV_TAC "array" >> - (* TODO: May want to use path cond here if you abbreviate array using assumptions *) - EVAL_TAC - ) >> -*) - disch_tac >> - CASE_TAC >- ( - EVAL_TAC >> - ntac (int_of_term entry_width) (exists_tac (mk_arb bool)) >> - REWRITE_TAC [] - ) >> - Cases_on ‘x’ >> - imp_res_tac p4_symb_execTheory.wellformed_register_array_oEL >> - imp_res_tac list_exists_thm >> - RW_TAC std_ss [] - ); - (* TODO: The antecedent may be computable. Either check this before or compute it here *) - val wf_ante_eval = EVAL “wellformed_register_array ^entry_width ^array” - - val approx_thm' = - if Teq $ snd $ dest_eq $ concl wf_ante_eval - then MATCH_MP approx_thm (EQT_ELIM wf_ante_eval) - else approx_thm - in - SOME (approx_thm', [fv_index+(int_of_term entry_width)]) - end -*) + else if (ext_obj = "") andalso (ext_method = "update_checksum") + then approx_v1model_update_checksum p4_symb_arg_prefix fv_index scope_list else NONE end else NONE end (* Branch point: emission of packet in final block *) | output port_bl => - if (not $ null $ free_vars port_bl orelse HOLset.member (all_atoms port_bl, “ARB:bool”)) + if (not $ null $ free_vars port_bl orelse HOLset.member (all_atoms port_bl, mk_arb bool)) then (* TODO: Fix hack... *) SOME (SPEC “v1model_is_drop_port ^port_bl” disj_list_EXCLUDED_MIDDLE, [fv_index, fv_index]) @@ -3050,7 +2958,7 @@ fun p4_symb_exec_prove_contract_gen p4_symb_exec_fun debug_flag arch_ty ctx_data (* Prove postcondition holds for all resulting states in n-step theorems *) val id_step_post_thm_list = - prove_postconds debug_flag postcond_rewr_thms postcond_simpset postcond path_cond_step_list + prove_postconds debug_flag postcond_rewr_thms stop_consts_rewr postcond_simpset postcond path_cond_step_list (* if debug_flag then diff --git a/hol/symb_exec/p4_symb_execScript.sml b/hol/symb_exec/p4_symb_execScript.sml index 03c45b33..4ddbd65e 100644 --- a/hol/symb_exec/p4_symb_execScript.sml +++ b/hol/symb_exec/p4_symb_execScript.sml @@ -504,4 +504,11 @@ p4_v1model_lookup_avar_validity varn (((i, in_out_list, in_out_list', (counter, | _ => NONE End +Theorem w2v_exists: +!w. ?b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15. w2v (w:word16) = [b0; b1; b2; b3; b4; b5; b6; b7; b8; b9; b10; b11; b12; b13; b14; b15] +Proof +rpt strip_tac >> +fs[bitstringTheory.w2v_def] +QED + val _ = export_theory (); diff --git a/hol/symb_exec/p4_symb_exec_v1modelLib.sig b/hol/symb_exec/p4_symb_exec_v1modelLib.sig index ac650681..1abf6875 100644 --- a/hol/symb_exec/p4_symb_exec_v1modelLib.sig +++ b/hol/symb_exec/p4_symb_exec_v1modelLib.sig @@ -6,5 +6,7 @@ val approx_v1model_register_construct : string -> int -> term -> (thm * int list) option val approx_v1model_register_read : string -> int -> term -> term -> (thm * int list) option +val approx_v1model_update_checksum : + string -> int -> term -> (thm * int list) option end diff --git a/hol/symb_exec/p4_symb_exec_v1modelLib.sml b/hol/symb_exec/p4_symb_exec_v1modelLib.sml index daa6b76a..6ec30386 100644 --- a/hol/symb_exec/p4_symb_exec_v1modelLib.sml +++ b/hol/symb_exec/p4_symb_exec_v1modelLib.sml @@ -110,4 +110,27 @@ fun approx_v1model_register_read p4_symb_arg_prefix fv_index scope_list ascope = end ; +(* TODO: Fix this. Similar to register construction *) +fun approx_v1model_update_checksum p4_symb_arg_prefix fv_index scope_list = + let + (* TODO: HOL4P4_CONV? *) + val data_bitlist = dest_some $ rhs $ concl $ EVAL “get_checksum_incr' ^scope_list (lval_varname (varn_name "data"))” + + val tm1 = mk_v1model_update_checksum_inner data_bitlist + + val approx_vars = fixedwidth_freevars_fromindex (p4_symb_arg_prefix, fv_index, 16) + + val rhs_tm = mk_v_bit $ mk_pair (approx_vars, term_of_int 16) + val goal_tm = mk_disj_list [boolSyntax.list_mk_exists (fst $ dest_list approx_vars, mk_eq (tm1, rhs_tm))] + + val approx_thm = + (* “^goal_tm” *) + prove(goal_tm, + SIMP_TAC std_ss [disj_list_def, v1model_update_checksum_inner_def, p4Theory.v_11, p4Theory.w16_def, w2v_exists] + ); + in + SOME (approx_thm, [fv_index+16]) + end +; + end diff --git a/hol/symb_exec/symb_execLib.sig b/hol/symb_exec/symb_execLib.sig index ae295728..7bd7aebc 100644 --- a/hol/symb_exec/symb_execLib.sig +++ b/hol/symb_exec/symb_execLib.sig @@ -18,6 +18,6 @@ val symb_exec_conc: (thm -> bool) -> thm -> int -> int -> path_tree * (int * thm * thm) list -val prove_postconds: bool -> thm list -> simpLib.simpset -> term -> (int * thm * thm) list -> (int * thm) list +val prove_postconds: bool -> thm list -> term list -> simpLib.simpset -> term -> (int * thm * thm) list -> (int * thm) list end diff --git a/hol/symb_exec/symb_execLib.sml b/hol/symb_exec/symb_execLib.sml index 459041ab..024da609 100644 --- a/hol/symb_exec/symb_execLib.sml +++ b/hol/symb_exec/symb_execLib.sml @@ -491,12 +491,13 @@ val rewr_thms = postcond_rewr_thms val simpset = postcond_simpset val rewr_thms = rewr_thms@[lookup_v_def, lookup_map_def, topmost_map_def, find_topmost_map_def] +val restr_tms = stop_consts_rewr open p4Theory; *) (* TODO: This should take a custom CONV *) -fun prove_postcond rewr_thms simpset postcond step_thm = +fun prove_postcond rewr_thms restr_tms simpset postcond step_thm = let val prel_res_thm = HO_MATCH_MP symb_exec_add_postcond step_thm val (hypo, step_tm) = dest_imp $ concl step_thm @@ -504,8 +505,10 @@ fun prove_postcond rewr_thms simpset postcond step_thm = (* TODO: OPTIMIZE: srw_ss??? EVAL_CONV? *) (* val postcond_thm = EQT_ELIM $ (computeLib.EVAL_CONV THENC (SIMP_CONV ((srw_ss())++bitstringLib.BITSTRING_GROUND_ss++boolSimps.LET_ss) rewr_thms)) $ mk_imp (hypo, mk_comb (postcond, res_state_tm)) + + val postcond_thm = EQT_ELIM $ (SIMP_CONV bool_ss rewr_thms THENC SIMP_CONV simpset [] THENC computeLib.RESTR_EVAL_CONV restr_tms THENC (SIMP_CONV ((srw_ss())++bitstringLib.BITSTRING_GROUND_ss++boolSimps.LET_ss) rewr_thms)) $ mk_imp (hypo, mk_comb (postcond, res_state_tm)) *) - val postcond_thm = EQT_ELIM $ (SIMP_CONV bool_ss [] THENC SIMP_CONV simpset [] THENC computeLib.EVAL_CONV THENC (SIMP_CONV ((srw_ss())++bitstringLib.BITSTRING_GROUND_ss++boolSimps.LET_ss) rewr_thms)) $ mk_imp (hypo, mk_comb (postcond, res_state_tm)) + val postcond_thm = EQT_ELIM $ (SIMP_CONV bool_ss rewr_thms THENC SIMP_CONV simpset [] THENC computeLib.RESTR_EVAL_CONV restr_tms THENC (SIMP_CONV ((srw_ss())++bitstringLib.BITSTRING_GROUND_ss++boolSimps.LET_ss) rewr_thms)) $ mk_imp (hypo, mk_comb (postcond, res_state_tm)) in MATCH_MP prel_res_thm postcond_thm end @@ -513,7 +516,7 @@ fun prove_postcond rewr_thms simpset postcond step_thm = (* DEBUG val step_thms = map #3 path_cond_step_list; -val step_thm = hd step_thms +val step_thm = el 5 step_thms (* basic: Index 24, 32, 52, 67 are interesting *) val h = el 24 step_thms @@ -523,24 +526,24 @@ val h = el 67 step_thms val rewr_thms = postcond_rewr_thms *) -fun prove_postconds_debug' rewr_thms _ postcond [] _ = [] - | prove_postconds_debug' rewr_thms simpset postcond (h::t) n = +fun prove_postconds_debug' rewr_thms restr_tms _ postcond [] _ = [] + | prove_postconds_debug' rewr_thms restr_tms simpset postcond (h::t) n = let - val res = prove_postcond rewr_thms simpset postcond h + val res = prove_postcond rewr_thms restr_tms simpset postcond h handle exc => (print (("Error when proving postcondition for n-step theorem at 0-index "^(Int.toString n))^"\n"); raise exc) in - (res::(prove_postconds_debug' rewr_thms simpset postcond t (n + 1))) + (res::(prove_postconds_debug' rewr_thms restr_tms simpset postcond t (n + 1))) end ; -fun prove_postconds debug_flag rewr_thms simpset postcond path_cond_step_list = +fun prove_postconds debug_flag rewr_thms restr_tms simpset postcond path_cond_step_list = if debug_flag then let val (l', l'') = unzip $ map (fn (a,b,c) => (a, c)) path_cond_step_list in - zip l' (prove_postconds_debug' rewr_thms simpset postcond l'' 0) + zip l' (prove_postconds_debug' rewr_thms restr_tms simpset postcond l'' 0) end - else map (fn (a,b,c) => (a, prove_postcond rewr_thms simpset postcond c)) path_cond_step_list + else map (fn (a,b,c) => (a, prove_postcond rewr_thms restr_tms simpset postcond c)) path_cond_step_list ; end