From ba4ceac31282284d37d9988454414b13c1d35cfa Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Tue, 19 Nov 2024 14:43:44 +0000 Subject: [PATCH 01/28] start loop plumbing --- backend/cn/lib/cn_internal_to_ail.ml | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 57559e26c..562746d5a 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -613,10 +613,11 @@ type ail_bindings_and_statements = type ail_executable_spec = { pre : ail_bindings_and_statements; post : ail_bindings_and_statements; - in_stmt : (Locations.t * ail_bindings_and_statements) list - } + in_stmt : (Locations.t * ail_bindings_and_statements) list; + loops: (Locations.t * ail_bindings_and_statements) list; + } -let empty_ail_executable_spec = { pre = ([], []); post = ([], []); in_stmt = [] } +let empty_ail_executable_spec = { pre = ([], []); post = ([], []); in_stmt = []; loops = [] } type 'a dest = | Assert : Cerb_location.t -> ail_bindings_and_statements dest @@ -3277,6 +3278,16 @@ let cn_to_ail_statements dts globals (loc, cn_progs) = (loc, (List.concat bs, upd_s @ List.concat ss @ pop_s)) + +let cn_to_ail_loop dts globals (loc, at) = match at with + | AT.Computational (_, _, _ ) -> (loc, []) + | L stats -> + (* let ail_statements = + List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats + in *) + (loc, []) + + let prepend_to_precondition ail_executable_spec (b1, s1) = let b2, s2 = ail_executable_spec.pre in { ail_executable_spec with pre = (b1 @ b2, s1 @ s2) } @@ -3344,7 +3355,7 @@ let rec cn_to_ail_lat_internal_2 in prepend_to_precondition ail_executable_spec (b1, ss) (* Postcondition *) - | LAT.I (post, (stats, _loop)) -> + | LAT.I (post, (stats, loop)) -> (*TODO: handle loops *) let rec remove_duplicates locs stats = match stats with @@ -3390,6 +3401,7 @@ let rec cn_to_ail_lat_internal_2 let ail_statements = List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats in + let ail_loop_invariants = List.map (cn_to_ail_loop dts globals) loop in let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in let ownership_stat_ = if without_ownership_checking then @@ -3406,7 +3418,7 @@ let rec cn_to_ail_lat_internal_2 A.( AilSblock (return_cn_binding @ post_bs, return_cn_decl @ post_ss @ ownership_stat_)) in - { pre = ([], []); post = ([], [ block ]); in_stmt = ail_statements } + { pre = ([], []); post = ([], [ block ]); in_stmt = ail_statements; loops = [] } let rec cn_to_ail_pre_post_aux_internal From 9020534730786801f5b497a18f68fec63c097b9b Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Tue, 19 Nov 2024 16:51:16 +0000 Subject: [PATCH 02/28] Add functions for separating variable declarations for loop purposes, and add plumbing through to executable spec for whole loop location --- backend/cn/lib/cn_internal_to_ail.ml | 100 ++++++++++++++++++--- backend/cn/lib/cn_internal_to_ail.mli | 6 +- backend/cn/lib/executable_spec_extract.ml | 11 ++- backend/cn/lib/executable_spec_extract.mli | 4 +- backend/cn/lib/executable_spec_records.ml | 2 +- backend/cn/lib/executable_spec_utils.ml | 33 +++++++ backend/cn/lib/ownership_exec.ml | 36 -------- 7 files changed, 132 insertions(+), 60 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 562746d5a..269b1f7d0 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -614,10 +614,15 @@ type ail_executable_spec = { pre : ail_bindings_and_statements; post : ail_bindings_and_statements; in_stmt : (Locations.t * ail_bindings_and_statements) list; - loops: (Locations.t * ail_bindings_and_statements) list; - } + loops : + ((Locations.t * ail_bindings_and_statements) + * (Locations.t * ail_bindings_and_statements)) + list + } + +let empty_ail_executable_spec = + { pre = ([], []); post = ([], []); in_stmt = []; loops = [] } -let empty_ail_executable_spec = { pre = ([], []); post = ([], []); in_stmt = []; loops = [] } type 'a dest = | Assert : Cerb_location.t -> ail_bindings_and_statements dest @@ -3278,14 +3283,78 @@ let cn_to_ail_statements dts globals (loc, cn_progs) = (loc, (List.concat bs, upd_s @ List.concat ss @ pop_s)) - -let cn_to_ail_loop dts globals (loc, at) = match at with - | AT.Computational (_, _, _ ) -> (loc, []) - | L stats -> - (* let ail_statements = - List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats - in *) - (loc, []) +let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = function + | LAT.Define ((name, it), _info, lat) -> + let ctype = bt_to_ail_ctype (IT.bt it) in + let binding = create_binding name ctype in + let decl = A.(AilSdeclaration [ (name, None) ]) in + let b1, s1 = cn_to_ail_expr_internal dts globals it (AssignVar name) in + let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in + (b1 @ b2 @ [ binding ], (decl :: s1) @ s2) + | LAT.Resource ((name, (ret, _bt)), (loc, _str_opt), lat) -> + let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in + let pop_s = generate_cn_pop_msg_info in + let b1, s1 = + cn_to_ail_resource_internal ~is_pre:true ~is_toplevel name dts globals preds loc ret + in + let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in + (b1 @ b2, upd_s @ s1 @ pop_s @ s2) + | LAT.Constraint (lc, (loc, _str_opt), lat) -> + let b1, s, e = cn_to_ail_logical_constraint_internal dts globals PassBack lc in + let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in + let pop_s = generate_cn_pop_msg_info in + let ss = upd_s @ s @ generate_cn_assert (*~cn_source_loc_opt:(Some loc)*) e @ pop_s in + let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in + (b1 @ b2, ss @ s2) + | LAT.I ss -> + let ail_statements = + List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) ss + in + let _, bs_and_ss = List.split ail_statements in + let bs, ss = List.split bs_and_ss in + (List.concat bs, List.concat ss) + + +let cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at) = + match at with + | AT.Computational (_, _, _) -> + (* TODO: Loop computational args *) + ((cond_loc, ([], [])), (loop_loc, ([], []))) + | L lat -> + let rec modify_decls_for_loop decls modified_stats = + let rec collect_initialised_syms_and_exprs = function + | [] -> [] + | (sym, Some expr) :: xs -> (sym, expr) :: collect_initialised_syms_and_exprs xs + | (_, None) :: xs -> collect_initialised_syms_and_exprs xs + in + function + | [] -> (decls, modified_stats) + | s :: ss -> + (match s with + (* + Separate initialised variable declarations into declaration and initialisation (assignment). + Needed so that CN invariant ghost variables are in scope for assertions in the loop body. + *) + | A.(AilSdeclaration syms_and_exprs) -> + let sym_some_expr_pairs = collect_initialised_syms_and_exprs syms_and_exprs in + let none_pairs = List.map (fun (sym, _) -> (sym, None)) syms_and_exprs in + let none_decl = A.(AilSdeclaration none_pairs) in + let assign_stats = + List.map + (fun (sym, rhs_expr) -> + let ident = mk_expr A.(AilEident sym) in + A.(AilSexpr (mk_expr (AilEassign (ident, rhs_expr))))) + sym_some_expr_pairs + in + modify_decls_for_loop + (decls @ [ none_decl ]) + (modified_stats @ assign_stats) + ss + | _ -> modify_decls_for_loop decls (modified_stats @ [ s ]) ss) + in + let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in + let decls, modified_stats = modify_decls_for_loop [] [] ss in + ((cond_loc, ([], modified_stats)), (loop_loc, (bs, decls))) let prepend_to_precondition ail_executable_spec (b1, s1) = @@ -3356,7 +3425,6 @@ let rec cn_to_ail_lat_internal_2 prepend_to_precondition ail_executable_spec (b1, ss) (* Postcondition *) | LAT.I (post, (stats, loop)) -> - (*TODO: handle loops *) let rec remove_duplicates locs stats = match stats with | [] -> [] @@ -3401,7 +3469,7 @@ let rec cn_to_ail_lat_internal_2 let ail_statements = List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats in - let ail_loop_invariants = List.map (cn_to_ail_loop dts globals) loop in + let ail_loop_invariants = List.map (cn_to_ail_loop dts globals preds) loop in let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in let ownership_stat_ = if without_ownership_checking then @@ -3418,7 +3486,11 @@ let rec cn_to_ail_lat_internal_2 A.( AilSblock (return_cn_binding @ post_bs, return_cn_decl @ post_ss @ ownership_stat_)) in - { pre = ([], []); post = ([], [ block ]); in_stmt = ail_statements; loops = [] } + { pre = ([], []); + post = ([], [ block ]); + in_stmt = ail_statements; + loops = ail_loop_invariants + } let rec cn_to_ail_pre_post_aux_internal diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli index 0eab96128..a0d1e2aba 100644 --- a/backend/cn/lib/cn_internal_to_ail.mli +++ b/backend/cn/lib/cn_internal_to_ail.mli @@ -54,7 +54,11 @@ type ail_bindings_and_statements = type ail_executable_spec = { pre : ail_bindings_and_statements; post : ail_bindings_and_statements; - in_stmt : (Locations.t * ail_bindings_and_statements) list + in_stmt : (Locations.t * ail_bindings_and_statements) list; + loops : + ((Locations.t * ail_bindings_and_statements) + * (Locations.t * ail_bindings_and_statements)) + list } val generate_get_or_put_ownership_function diff --git a/backend/cn/lib/executable_spec_extract.ml b/backend/cn/lib/executable_spec_extract.ml index 2f904b3be..4c878ddc6 100644 --- a/backend/cn/lib/executable_spec_extract.ml +++ b/backend/cn/lib/executable_spec_extract.ml @@ -10,10 +10,10 @@ type statements = statement list let statements_subst subst = List.map (statement_subst subst) -type loop = Locations.t * statements ArgumentTypes.t +type loop = Locations.t * Locations.t * statements ArgumentTypes.t -let loop_subst subst ((loc, at) : loop) = - (loc, ArgumentTypes.subst statements_subst subst at) +let loop_subst subst ((cond_loc, loop_loc, at) : loop) = + (cond_loc, loop_loc, ArgumentTypes.subst statements_subst subst at) type loops = loop list @@ -106,11 +106,10 @@ let rec stmts_in_expr (Mucore.Expr (loc, _, _, e_)) = let from_loop ((_label_sym : Sym.t), (label_def : _ label_def)) : loop option = match label_def with | Return _ -> None - | Label (_loc, label_args_and_body, _annots, _, `Loop (loop_condition_loc, _loop_loc)) - -> + | Label (_loc, label_args_and_body, _annots, _, `Loop (loop_condition_loc, loop_loc)) -> let label_args_and_body = Core_to_mucore.at_of_arguments Fun.id label_args_and_body in let label_args_and_statements = ArgumentTypes.map stmts_in_expr label_args_and_body in - Some (loop_condition_loc, label_args_and_statements) + Some (loop_condition_loc, loop_loc, label_args_and_statements) let from_fn (fn, decl) = diff --git a/backend/cn/lib/executable_spec_extract.mli b/backend/cn/lib/executable_spec_extract.mli index 9844565f1..8f964d5fe 100644 --- a/backend/cn/lib/executable_spec_extract.mli +++ b/backend/cn/lib/executable_spec_extract.mli @@ -2,8 +2,8 @@ type statement = Locations.t * Cnprog.t list type statements = statement list -type loop = - Locations.t * statements ArgumentTypes.t (* location is for the loop condition *) +type loop = Locations.t * Locations.t * statements ArgumentTypes.t +(* first location is for the loop condition; second is for the entire loop *) type loops = loop list diff --git a/backend/cn/lib/executable_spec_records.ml b/backend/cn/lib/executable_spec_records.ml index 56a317561..574ab3e20 100644 --- a/backend/cn/lib/executable_spec_records.ml +++ b/backend/cn/lib/executable_spec_records.ml @@ -122,7 +122,7 @@ let add_records_to_map_from_instrumentation (i : Executable_spec_extract.instrum aux_rt rt; List.iter add_records_to_map_from_cnprogs stmts; List.iter - (fun (_loc, loop_at) -> + (fun (_loc1, _loc2, loop_at) -> let loop_stmts = aux_at loop_at in List.iter add_records_to_map_from_cnprogs loop_stmts) loops diff --git a/backend/cn/lib/executable_spec_utils.ml b/backend/cn/lib/executable_spec_utils.ml index 48d61af85..a1619638d 100644 --- a/backend/cn/lib/executable_spec_utils.ml +++ b/backend/cn/lib/executable_spec_utils.ml @@ -155,3 +155,36 @@ let create_decl_object ctype = (* declarations: list (ail_identifier * (Loc.t * Annot.attributes * declaration)) *) let create_declaration sym decl = (sym, (Cerb_location.unknown, CF.Annot.Attrs [], decl)) + +let get_start_loc ?(offset = 0) = function + | Cerb_location.Loc_region (start_pos, _, _) -> + let new_start_pos = { start_pos with pos_cnum = start_pos.pos_cnum + offset } in + Cerb_location.point new_start_pos + | Loc_regions (pos_list, _) -> + (match List.last pos_list with + | Some (_, start_pos) -> + let new_start_pos = { start_pos with pos_cnum = start_pos.pos_cnum + offset } in + Cerb_location.point new_start_pos + | None -> + failwith + "get_start_loc: Loc_regions has empty list of positions (should be non-empty)") + | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } + | Loc_unknown | Loc_other _ -> + failwith "get_start_loc: Location should be Loc_region, Loc_regions or Loc_point" + + +let get_end_loc ?(offset = 0) = function + | Cerb_location.Loc_region (_, end_pos, _) -> + let new_end_pos = { end_pos with pos_cnum = end_pos.pos_cnum + offset } in + Cerb_location.point new_end_pos + | Loc_regions (pos_list, _) -> + (match List.last pos_list with + | Some (_, end_pos) -> + let new_end_pos = { end_pos with pos_cnum = end_pos.pos_cnum + offset } in + Cerb_location.point new_end_pos + | None -> + failwith + "get_end_loc: Loc_regions has empty list of positions (should be non-empty)") + | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } + | Loc_unknown | Loc_other _ -> + failwith "get_end_loc: Location should be Loc_region, Loc_regions or Loc_point" diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index c4eb7583f..5545e55b7 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -27,42 +27,6 @@ let c_declare_and_map_local_sym = Sym.fresh_pretty "c_declare_and_map_local" let c_declare_init_and_map_local_sym = Sym.fresh_pretty "c_declare_init_and_map_local" -let get_start_loc ?(offset = 0) = function - | Cerb_location.Loc_region (start_pos, _, _) -> - let new_start_pos = { start_pos with pos_cnum = start_pos.pos_cnum + offset } in - Cerb_location.point new_start_pos - | Loc_regions (pos_list, _) -> - (match List.last pos_list with - | Some (_, start_pos) -> - let new_start_pos = { start_pos with pos_cnum = start_pos.pos_cnum + offset } in - Cerb_location.point new_start_pos - | None -> - failwith - "get_start_loc: Loc_regions has empty list of positions (should be non-empty)") - | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } - | Loc_unknown | Loc_other _ -> - failwith - "get_start_loc: Location of AilSdeclaration should be Loc_region or Loc_regions" - - -let get_end_loc ?(offset = 0) = function - | Cerb_location.Loc_region (_, end_pos, _) -> - let new_end_pos = { end_pos with pos_cnum = end_pos.pos_cnum + offset } in - Cerb_location.point new_end_pos - | Loc_regions (pos_list, _) -> - (match List.last pos_list with - | Some (_, end_pos) -> - let new_end_pos = { end_pos with pos_cnum = end_pos.pos_cnum + offset } in - Cerb_location.point new_end_pos - | None -> - failwith - "get_end_loc: Loc_regions has empty list of positions (should be non-empty)") - | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } - | Loc_unknown | Loc_other _ -> - failwith - "get_end_loc: Location of AilSdeclaration should be Loc_region or Loc_regions" - - let get_ownership_global_init_stats () = let cn_ghost_state_init_fcall = mk_expr From aa64e070e153ad9f5a133cc06163e4a32afe3755 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 20 Nov 2024 13:43:42 +0000 Subject: [PATCH 03/28] Complete loop invariant plumbing + disable internal VIP allocations in executable spec mode --- backend/cn/lib/cn_internal_to_ail.ml | 10 ++++++---- backend/cn/lib/core_to_mucore.ml | 14 ++++++++------ backend/cn/lib/executable_spec_internal.ml | 15 ++++++++++++++- runtime/libcn/libexec/cn-runtime-single-file.sh | 2 +- 4 files changed, 29 insertions(+), 12 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 269b1f7d0..44db93bb6 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -2605,6 +2605,7 @@ let cn_to_ail_resource_internal let matching_preds = List.filter (fun (pred_sym', _def) -> Sym.equal pname pred_sym') preds in + Printf.printf "Pred sym: %s\n" (Sym.pp_string pname); let pred_sym', pred_def' = match matching_preds with | [] -> @@ -3285,7 +3286,7 @@ let cn_to_ail_statements dts globals (loc, cn_progs) = let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = function | LAT.Define ((name, it), _info, lat) -> - let ctype = bt_to_ail_ctype (IT.bt it) in + let ctype = bt_to_ail_ctype (IT.get_bt it) in let binding = create_binding name ctype in let decl = A.(AilSdeclaration [ (name, None) ]) in let b1, s1 = cn_to_ail_expr_internal dts globals it (AssignVar name) in @@ -3315,11 +3316,12 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu (List.concat bs, List.concat ss) -let cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at) = +let rec cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at) = match at with - | AT.Computational (_, _, _) -> + | AT.Computational (_, _, at') -> (* TODO: Loop computational args *) - ((cond_loc, ([], [])), (loop_loc, ([], []))) + (* ((cond_loc, ([], [])), (loop_loc, ([], []))) *) + cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at') | L lat -> let rec modify_decls_for_loop decls modified_stats = let rec collect_initialised_syms_and_exprs = function diff --git a/backend/cn/lib/core_to_mucore.ml b/backend/cn/lib/core_to_mucore.ml index 312d644f9..78d2b0cb5 100644 --- a/backend/cn/lib/core_to_mucore.ml +++ b/backend/cn/lib/core_to_mucore.ml @@ -951,13 +951,15 @@ let make_label_args f_i loc env st args (accesses, inv) = let env = C.add_logical oa_name oa_bt env in let st = C.LocalState.add_c_variable_state s (CVS_Pointer_pointing_to value) st in let owned_res = ((oa_name, (pt_ret, SBT.proj oa_bt)), (loc, None)) in - let alloc_res = C.allocation_token loc s in + let resources' = + if !Sym.executable_spec_enabled then + [ owned_res ] + else ( + let alloc_res = C.allocation_token loc s in + [ alloc_res; owned_res ]) + in let@ at = - aux - (resources @ [ alloc_res; owned_res ], good_lcs @ (* good_pointer_lc :: *) lcs) - env - st - rest + aux (resources @ resources', good_lcs @ (* good_pointer_lc :: *) lcs) env st rest in return (Mu.mComputational ((s, Loc ()), (loc, None)) at) | [] -> diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index d1cb0a530..cd3c5961f 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -145,8 +145,21 @@ let generate_c_pres_and_posts_internal (fun (loc, e_opt, strs) -> (loc, e_opt, [ String.concat "\n" strs ])) return_ownership_stmts in + let ail_loop_invariants = ail_executable_spec.loops in + let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in + let ail_cond_injs = + List.map + (fun (loc, bs_and_ss) -> + (get_start_loc loc, generate_ail_stat_strs bs_and_ss @ [ ", " ])) + ail_cond_stats + in + let ail_loop_decl_injs = + List.map + (fun (loc, bs_and_ss) -> (get_start_loc loc, generate_ail_stat_strs bs_and_ss)) + ail_loop_decls + in ( [ (instrumentation.fn, (pre_str, post_str)) ], - in_stmt @ block_ownership_stmts, + in_stmt @ block_ownership_stmts @ ail_cond_injs @ ail_loop_decl_injs, return_ownership_stmts ) diff --git a/runtime/libcn/libexec/cn-runtime-single-file.sh b/runtime/libcn/libexec/cn-runtime-single-file.sh index 371d349fb..7a0e0c663 100755 --- a/runtime/libcn/libexec/cn-runtime-single-file.sh +++ b/runtime/libcn/libexec/cn-runtime-single-file.sh @@ -65,7 +65,7 @@ if cn instrument "${INPUT_FN}" \ ${NO_CHECK_OWNERSHIP}; then [ "${QUIET}" ] || echo "Generating C files from CN-annotated source." else - echo_and_err "Failed to generate C files from CN-annotatated source." + echo_and_err "Failed to generate C files from CN-annotated source." fi # Compile From 6ddd7ba5b0aa837462faa86da0b44d5b40febd36 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 20 Nov 2024 15:47:26 +0000 Subject: [PATCH 04/28] Runtime loop invariants compiling and running --- backend/cn/lib/cn_internal_to_ail.ml | 12 +++++++++++- backend/cn/lib/executable_spec_internal.ml | 19 ++++++++++++++++++- 2 files changed, 29 insertions(+), 2 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 44db93bb6..cb83a331c 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3356,7 +3356,17 @@ let rec cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at) = in let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in let decls, modified_stats = modify_decls_for_loop [] [] ss in - ((cond_loc, ([], modified_stats)), (loop_loc, (bs, decls))) + let dummy_expr_as_stat = + A.( + AilSexpr + (mk_expr (AilEconst (ConstantInteger (IConstant (Z.of_int 0, Decimal, None)))))) + in + let ail_gcc_stat_as_expr = + A.( + AilEgcc_statement (bs, List.map mk_stmt (modified_stats @ [ dummy_expr_as_stat ]))) + in + let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in + ((cond_loc, ([], [ ail_stat_as_expr_stat ])), (loop_loc, (bs, decls))) let prepend_to_precondition ail_executable_spec (b1, s1) = diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index cd3c5961f..4399f4a28 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -147,10 +147,27 @@ let generate_c_pres_and_posts_internal in let ail_loop_invariants = ail_executable_spec.loops in let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in + (* A bit of a hack *) + let rec remove_last = function + | [] -> [] + | [ _ ] -> [] + | x :: xs -> x :: remove_last xs + in + let rec remove_last_semicolon = function + | [] -> [] + | [ x ] -> + let split_x = String.split_on_char ';' x in + let without_whitespace_x = remove_last split_x in + let res = String.concat ";" without_whitespace_x in + Printf.printf "res: %s\n" res; + [ res ] + | x :: xs -> x :: remove_last_semicolon xs + in let ail_cond_injs = List.map (fun (loc, bs_and_ss) -> - (get_start_loc loc, generate_ail_stat_strs bs_and_ss @ [ ", " ])) + ( get_start_loc loc, + remove_last_semicolon (generate_ail_stat_strs bs_and_ss) @ [ ", " ] )) ail_cond_stats in let ail_loop_decl_injs = From 1df691e4953224783cde598b6ae805e56ce30eb6 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 20 Nov 2024 17:07:56 +0000 Subject: [PATCH 05/28] Separate stack depth decr and postcondition leak check --- backend/cn/lib/cn_internal_to_ail.ml | 17 ++++++++--------- backend/cn/lib/ownership_exec.ml | 2 ++ 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index cb83a331c..5e78b58c3 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3483,20 +3483,19 @@ let rec cn_to_ail_lat_internal_2 in let ail_loop_invariants = List.map (cn_to_ail_loop dts globals preds) loop in let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in - let ownership_stat_ = + let ownership_stats_ = if without_ownership_checking then [] - else ( - let cn_stack_depth_decr_stat_ = - mk_stmt - (A.AilSexpr - (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_decr_sym), [])))) - in - [ cn_stack_depth_decr_stat_ ]) + else + List.map + (fun fn_sym -> + mk_stmt (A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident fn_sym), []))))) + OE.[ cn_stack_depth_decr_sym; cn_postcondition_leak_check_sym ] in let block = A.( - AilSblock (return_cn_binding @ post_bs, return_cn_decl @ post_ss @ ownership_stat_)) + AilSblock + (return_cn_binding @ post_bs, return_cn_decl @ post_ss @ ownership_stats_)) in { pre = ([], []); post = ([], [ block ]); diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index 5545e55b7..50f2282e0 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -17,6 +17,8 @@ let cn_stack_depth_incr_sym = Sym.fresh_pretty "ghost_stack_depth_incr" let cn_stack_depth_decr_sym = Sym.fresh_pretty "ghost_stack_depth_decr" +let cn_postcondition_leak_check_sym = Sym.fresh_pretty "cn_postcondition_leak_check" + let c_add_ownership_fn_sym = Sym.fresh_pretty "c_add_to_ghost_state" let c_remove_ownership_fn_sym = Sym.fresh_pretty "c_remove_from_ghost_state" From a7cf6d39d5d7272281107fd8e276f73c52720bb1 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 20 Nov 2024 17:08:17 +0000 Subject: [PATCH 06/28] runtime lib separation of decr and leak check --- runtime/libcn/include/cn-executable/utils.h | 1 + runtime/libcn/src/cn-executable/utils.c | 34 ++++++++++++--------- 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index a6c93b6cf..adf735a45 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -145,6 +145,7 @@ void initialise_ghost_stack_depth(void); signed long get_cn_stack_depth(void); void ghost_stack_depth_incr(void); void ghost_stack_depth_decr(void); +void cn_postcondition_leak_check(void); /* malloc, free */ diff --git a/runtime/libcn/src/cn-executable/utils.c b/runtime/libcn/src/cn-executable/utils.c index d3737c978..167b55c4d 100644 --- a/runtime/libcn/src/cn-executable/utils.c +++ b/runtime/libcn/src/cn-executable/utils.c @@ -202,28 +202,32 @@ void ghost_stack_depth_incr(void) { #define FMT_PTR_2 "\x1B[35m%#lx\x1B[0m" void ghost_stack_depth_decr(void) { - cn_stack_depth--; - // update_error_message_info(0); - // print_error_msg_info(); + cn_stack_depth--; + // update_error_message_info(0); + // print_error_msg_info(); + + // cn_printf(CN_LOGGING_INFO, "\n"); +} + +void cn_postcondition_leak_check(void) { // leak checking hash_table_iterator it = ht_iterator(cn_ownership_global_ghost_state); // cn_printf(CN_LOGGING_INFO, "CN pointers leaked at (%ld) stack-depth: ", cn_stack_depth); while (ht_next(&it)) { - uintptr_t* key = (uintptr_t*)it.key; - int* depth = it.value; - if (*depth > cn_stack_depth) { - print_error_msg_info(error_msg_info); - cn_printf(CN_LOGGING_ERROR, "Leak check failed, ownership leaked for pointer "FMT_PTR"\n", *key); - cn_failure(CN_FAILURE_OWNERSHIP_LEAK); - // cn_printf(CN_LOGGING_INFO, FMT_PTR_2 " (%d),", *key, *depth); - } + uintptr_t *key = (uintptr_t *) it.key; + int *depth = it.value; + if (*depth > cn_stack_depth) { + print_error_msg_info(error_msg_info); + cn_printf(CN_LOGGING_ERROR, "Leak check failed, ownership leaked for pointer "FMT_PTR"\n", *key); + cn_failure(CN_FAILURE_OWNERSHIP_LEAK); + // cn_printf(CN_LOGGING_INFO, FMT_PTR_2 " (%d),", *key, *depth); + } } - // cn_printf(CN_LOGGING_INFO, "\n"); } -int ownership_ghost_state_get(signed long* address_key) { - int* curr_depth_maybe = (int*)ht_get(cn_ownership_global_ghost_state, address_key); - return curr_depth_maybe ? *curr_depth_maybe : -1; +int ownership_ghost_state_get(signed long *address_key) { + int *curr_depth_maybe = (int *) ht_get(cn_ownership_global_ghost_state, address_key); + return curr_depth_maybe ? *curr_depth_maybe : -1; } void ownership_ghost_state_set(signed long* address_key, int stack_depth_val) { From 83b58fcf6fc4b6644c7dd76e44fc774d771e06ee Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 20 Nov 2024 17:35:10 +0000 Subject: [PATCH 07/28] Add translation for computational arguments --- backend/cn/lib/cn_internal_to_ail.ml | 51 +++++++++++++++------- backend/cn/lib/executable_spec_extract.mli | 2 + 2 files changed, 37 insertions(+), 16 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 5e78b58c3..b8816f136 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3316,12 +3316,25 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu (List.concat bs, List.concat ss) -let rec cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at) = +let rec cn_to_ail_loop_aux dts globals preds (cond_loc, loop_loc, at) = match at with - | AT.Computational (_, _, at') -> - (* TODO: Loop computational args *) - (* ((cond_loc, ([], [])), (loop_loc, ([], []))) *) - cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at') + | AT.Computational ((sym, bt), _, at') -> + let cn_sym = generate_sym_with_suffix ~suffix:"_cn" sym in + let cn_ctype = bt_to_ail_ctype bt in + let binding = create_binding cn_sym cn_ctype in + let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in + let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in + let assign = + A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) + in + let subst_loop = + ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') + in + let (_, (_, cond_ss)), (_, (loop_bs, loop_ss)) = + cn_to_ail_loop_aux dts globals preds subst_loop + in + ( (cond_loc, ([], assign :: cond_ss)), + (loop_loc, (binding :: loop_bs, decl :: loop_ss)) ) | L lat -> let rec modify_decls_for_loop decls modified_stats = let rec collect_initialised_syms_and_exprs = function @@ -3356,17 +3369,23 @@ let rec cn_to_ail_loop dts globals preds (cond_loc, loop_loc, at) = in let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in let decls, modified_stats = modify_decls_for_loop [] [] ss in - let dummy_expr_as_stat = - A.( - AilSexpr - (mk_expr (AilEconst (ConstantInteger (IConstant (Z.of_int 0, Decimal, None)))))) - in - let ail_gcc_stat_as_expr = - A.( - AilEgcc_statement (bs, List.map mk_stmt (modified_stats @ [ dummy_expr_as_stat ]))) - in - let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in - ((cond_loc, ([], [ ail_stat_as_expr_stat ])), (loop_loc, (bs, decls))) + ((cond_loc, ([], modified_stats)), (loop_loc, (bs, decls))) + + +let cn_to_ail_loop dts globals preds ((cond_loc, loop_loc, _) as loop) = + let (_, (_, cond_ss)), (_, loop_bs_and_ss) = + cn_to_ail_loop_aux dts globals preds loop + in + let dummy_expr_as_stat = + A.( + AilSexpr + (mk_expr (AilEconst (ConstantInteger (IConstant (Z.of_int 0, Decimal, None)))))) + in + let ail_gcc_stat_as_expr = + A.(AilEgcc_statement ([], List.map mk_stmt (cond_ss @ [ dummy_expr_as_stat ]))) + in + let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in + ((cond_loc, ([], [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss)) let prepend_to_precondition ail_executable_spec (b1, s1) = diff --git a/backend/cn/lib/executable_spec_extract.mli b/backend/cn/lib/executable_spec_extract.mli index 8f964d5fe..cc039f3b3 100644 --- a/backend/cn/lib/executable_spec_extract.mli +++ b/backend/cn/lib/executable_spec_extract.mli @@ -20,6 +20,8 @@ val sym_subst : Sym.t * BaseTypes.t * Sym.t -> [ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t +val loop_subst : [ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t -> loop -> loop + val fn_args_and_body_subst : [ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t -> fn_args_and_body -> From 01b29fd8fdc414d4077f139967905a17c6a6630c Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 20 Nov 2024 18:16:42 +0000 Subject: [PATCH 08/28] End to end runtime loop invariants working for small example --- backend/cn/lib/cn_internal_to_ail.ml | 49 +++++++++------- backend/cn/lib/ownership_exec.ml | 13 +++++ runtime/libcn/include/cn-executable/utils.h | 6 +- runtime/libcn/src/cn-executable/utils.c | 63 +++++++++++++++------ 4 files changed, 92 insertions(+), 39 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index b8816f136..c9d2359ac 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -2578,12 +2578,12 @@ let get_while_bounds_and_cond (i_sym, i_bt) it = (* is_pre used for ownership checking, to see if ownership needs to be taken or put back *) let cn_to_ail_resource_internal - ?(is_pre = true) ?(is_toplevel = true) sym dts globals (preds : (Sym.t * Def.Predicate.t) list) + ownership_mode loc = let calculate_return_type = function @@ -2637,7 +2637,7 @@ let cn_to_ail_resource_internal | Request.P p -> let ctype, bt = calculate_return_type p.name in let b, s, e = cn_to_ail_expr_internal dts globals p.pointer PassBack in - let enum_str = if is_pre then "GET" else "PUT" in + let enum_str = OE.get_enum_str_from_ownership_mode ownership_mode in let enum_str = if not is_toplevel then "owned_enum" else enum_str in let enum_sym = Sym.fresh_pretty enum_str in let rhs, bs, ss, _owned_ctype = @@ -2734,7 +2734,7 @@ let cn_to_ail_resource_internal let cn_pointer_return_type = bt_to_ail_ctype BT.(Loc ()) in let ptr_add_binding = create_binding ptr_add_sym cn_pointer_return_type in let ptr_add_stat = A.(AilSdeclaration [ (ptr_add_sym, Some e4) ]) in - let enum_str = if is_pre then "GET" else "PUT" in + let enum_str = OE.get_enum_str_from_ownership_mode ownership_mode in let enum_str = if not is_toplevel then "owned_enum" else enum_str in let enum_sym = Sym.fresh_pretty enum_str in let rhs, bs, ss, _owned_ctype = @@ -3031,7 +3031,7 @@ let rec cn_to_ail_lat_internal ?(is_toplevel = true) dts pred_sym_opt globals pr let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in let b1, s1 = - cn_to_ail_resource_internal ~is_pre:true ~is_toplevel name dts globals preds loc ret + cn_to_ail_resource_internal ~is_toplevel name dts globals preds OE.Pre loc ret in let b2, s2 = cn_to_ail_lat_internal ~is_toplevel dts pred_sym_opt globals preds lat in (b1 @ b2, upd_s @ s1 @ pop_s @ s2) @@ -3174,9 +3174,7 @@ let rec cn_to_ail_post_aux_internal dts globals preds = function let new_name = generate_sym_with_suffix ~suffix:"_cn" name in let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in - let b1, s1 = - cn_to_ail_resource_internal ~is_pre:false new_name dts globals preds loc re - in + let b1, s1 = cn_to_ail_resource_internal new_name dts globals preds OE.Post loc re in let new_lrt = LogicalReturnTypes.subst (ESE.sym_subst (name, bt, new_name)) t in let b2, s2 = cn_to_ail_post_aux_internal dts globals preds new_lrt in (b1 @ b2, upd_s @ s1 @ pop_s @ s2) @@ -3296,7 +3294,7 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in let b1, s1 = - cn_to_ail_resource_internal ~is_pre:true ~is_toplevel name dts globals preds loc ret + cn_to_ail_resource_internal ~is_toplevel name dts globals preds OE.Loop loc ret in let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in (b1 @ b2, upd_s @ s1 @ pop_s @ s2) @@ -3316,12 +3314,13 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu (List.concat bs, List.concat ss) -let rec cn_to_ail_loop_aux dts globals preds (cond_loc, loop_loc, at) = +let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = match at with | AT.Computational ((sym, bt), _, at') -> - let cn_sym = generate_sym_with_suffix ~suffix:"_cn" sym in - let cn_ctype = bt_to_ail_ctype bt in + let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in + let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in let binding = create_binding cn_sym cn_ctype in + (* TODO: Check this should always translate to the address of the given sym in the loop invariant case *) let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in let assign = @@ -3331,7 +3330,7 @@ let rec cn_to_ail_loop_aux dts globals preds (cond_loc, loop_loc, at) = ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') in let (_, (_, cond_ss)), (_, (loop_bs, loop_ss)) = - cn_to_ail_loop_aux dts globals preds subst_loop + cn_to_ail_loop_inv_aux dts globals preds subst_loop in ( (cond_loc, ([], assign :: cond_ss)), (loop_loc, (binding :: loop_bs, decl :: loop_ss)) ) @@ -3372,18 +3371,30 @@ let rec cn_to_ail_loop_aux dts globals preds (cond_loc, loop_loc, at) = ((cond_loc, ([], modified_stats)), (loop_loc, (bs, decls))) -let cn_to_ail_loop dts globals preds ((cond_loc, loop_loc, _) as loop) = +let cn_to_ail_loop_inv dts globals preds ((cond_loc, loop_loc, _) as loop) = let (_, (_, cond_ss)), (_, loop_bs_and_ss) = - cn_to_ail_loop_aux dts globals preds loop + cn_to_ail_loop_inv_aux dts globals preds loop + in + let cn_stack_depth_incr_call = + A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_incr_sym), []))) + in + let cn_loop_leak_check_and_decr_call = + A.AilSexpr + (mk_expr (AilEcall (mk_expr (AilEident OE.cn_loop_leak_check_and_decr_sym), []))) + in + let cn_stack_depth_decr_call = + A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_decr_sym), []))) in let dummy_expr_as_stat = A.( AilSexpr (mk_expr (AilEconst (ConstantInteger (IConstant (Z.of_int 0, Decimal, None)))))) in - let ail_gcc_stat_as_expr = - A.(AilEgcc_statement ([], List.map mk_stmt (cond_ss @ [ dummy_expr_as_stat ]))) + let stats = + (cn_stack_depth_incr_call :: cond_ss) + @ [ cn_loop_leak_check_and_decr_call; cn_stack_depth_decr_call; dummy_expr_as_stat ] in + let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in ((cond_loc, ([], [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss)) @@ -3425,9 +3436,7 @@ let rec cn_to_ail_lat_internal_2 let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in let new_name = generate_sym_with_suffix ~suffix:"_cn" name in - let b1, s1 = - cn_to_ail_resource_internal ~is_pre:true new_name dts globals preds loc ret - in + let b1, s1 = cn_to_ail_resource_internal new_name dts globals preds OE.Pre loc ret in let new_lat = ESE.fn_largs_and_body_subst (ESE.sym_subst (name, bt, new_name)) lat in let ail_executable_spec = cn_to_ail_lat_internal_2 @@ -3500,7 +3509,7 @@ let rec cn_to_ail_lat_internal_2 let ail_statements = List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats in - let ail_loop_invariants = List.map (cn_to_ail_loop dts globals preds) loop in + let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds) loop in let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in let ownership_stats_ = if without_ownership_checking then diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index 50f2282e0..cbabceaff 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -3,6 +3,17 @@ open Executable_spec_utils module A = CF.AilSyntax module C = CF.Ctype +type ownership_mode = + | Pre + | Post + | Loop + +let get_enum_str_from_ownership_mode = function + | Pre -> "GET" + | Post -> "PUT" + | Loop -> "LOOP" + + let cn_ghost_state_sym = Sym.fresh_pretty "cn_ownership_global_ghost_state" let cn_ghost_state_struct_type = @@ -19,6 +30,8 @@ let cn_stack_depth_decr_sym = Sym.fresh_pretty "ghost_stack_depth_decr" let cn_postcondition_leak_check_sym = Sym.fresh_pretty "cn_postcondition_leak_check" +let cn_loop_leak_check_and_decr_sym = Sym.fresh_pretty "cn_loop_leak_check_and_decr" + let c_add_ownership_fn_sym = Sym.fresh_pretty "c_add_to_ghost_state" let c_remove_ownership_fn_sym = Sym.fresh_pretty "c_remove_from_ghost_state" diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index adf735a45..e62683207 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -146,6 +146,7 @@ signed long get_cn_stack_depth(void); void ghost_stack_depth_incr(void); void ghost_stack_depth_decr(void); void cn_postcondition_leak_check(void); +void cn_loop_leak_check_and_decr(void); /* malloc, free */ @@ -541,7 +542,8 @@ CN_GEN_MAP_GET(cn_map) enum OWNERSHIP { GET, - PUT + PUT, + LOOP }; int ownership_ghost_state_get(signed long *address_key); @@ -549,7 +551,7 @@ void ownership_ghost_state_set(signed long* address_key, int stack_depth_val); void ownership_ghost_state_remove(signed long* address_key); /* CN ownership checking */ -void cn_get_ownership(uintptr_t generic_c_ptr, size_t size); +void cn_get_ownership(uintptr_t generic_c_ptr, size_t size, char *check_msg); void cn_put_ownership(uintptr_t generic_c_ptr, size_t size); void cn_assume_ownership(void *generic_c_ptr, unsigned long size, char *fun); void cn_get_or_put_ownership(enum OWNERSHIP owned_enum, uintptr_t generic_c_ptr, size_t size); diff --git a/runtime/libcn/src/cn-executable/utils.c b/runtime/libcn/src/cn-executable/utils.c index 167b55c4d..255a6ccfb 100644 --- a/runtime/libcn/src/cn-executable/utils.c +++ b/runtime/libcn/src/cn-executable/utils.c @@ -218,13 +218,40 @@ void cn_postcondition_leak_check(void) { int *depth = it.value; if (*depth > cn_stack_depth) { print_error_msg_info(error_msg_info); - cn_printf(CN_LOGGING_ERROR, "Leak check failed, ownership leaked for pointer "FMT_PTR"\n", *key); + cn_printf(CN_LOGGING_ERROR, "Postcondition leak check failed, ownership leaked for pointer "FMT_PTR"\n", *key); cn_failure(CN_FAILURE_OWNERSHIP_LEAK); // cn_printf(CN_LOGGING_INFO, FMT_PTR_2 " (%d),", *key, *depth); } } } +void cn_loop_leak_check_and_decr(void) { + hash_table_iterator it1 = ht_iterator(cn_ownership_global_ghost_state); + + while (ht_next(&it1)) { + uintptr_t *key = (uintptr_t *) it1.key; + int *depth = it1.value; + /* Everything mapped to the function stack depth should have been bumped up by calls to Owned in invariant */ + if (*depth == cn_stack_depth - 1) { + print_error_msg_info(error_msg_info); + cn_printf(CN_LOGGING_ERROR, "Loop invariant leak check failed, ownership leaked for pointer "FMT_PTR"\n", *key); + cn_failure(CN_FAILURE_OWNERSHIP_LEAK); + // cn_printf(CN_LOGGING_INFO, FMT_PTR_2 " (%d),", *key, *depth); + } + } + + hash_table_iterator it2 = ht_iterator(cn_ownership_global_ghost_state); + + while (ht_next(&it2)) { + uintptr_t *key = (uintptr_t *) it2.key; + int *depth = it2.value; + /* Bump down everything that was bumped up in loop invariant */ + if (*depth == cn_stack_depth) { + ownership_ghost_state_set((signed long *) key, cn_stack_depth - 1); + } + } +} + int ownership_ghost_state_get(signed long *address_key) { int *curr_depth_maybe = (int *) ht_get(cn_ownership_global_ghost_state, address_key); return curr_depth_maybe ? *curr_depth_maybe : -1; @@ -253,10 +280,9 @@ void dump_ownership_state() } -void cn_get_ownership(uintptr_t generic_c_ptr, size_t size) { - // cn_printf(CN_LOGGING_INFO, "[CN: getting ownership] " FMT_PTR_2 ", size: %lu\n", generic_c_ptr, size); - //// print_error_msg_info(); - c_ownership_check("Precondition ownership check", generic_c_ptr, (int)size, cn_stack_depth - 1); +void cn_get_ownership(uintptr_t generic_c_ptr, size_t size, char *check_msg) { + /* Used for precondition and loop invariant taking/getting of ownership */ + c_ownership_check(check_msg, generic_c_ptr, (int) size, cn_stack_depth - 1); c_add_to_ghost_state(generic_c_ptr, size, cn_stack_depth); } @@ -283,18 +309,21 @@ void cn_assume_ownership(void* generic_c_ptr, unsigned long size, char* fun) { void cn_get_or_put_ownership(enum OWNERSHIP owned_enum, uintptr_t generic_c_ptr, size_t size) { nr_owned_predicates++; switch (owned_enum) - { - case GET: - { - cn_get_ownership(generic_c_ptr, size); - break; - } - case PUT: - { - cn_put_ownership(generic_c_ptr, size); - break; - } - } + { + case GET: + { + cn_get_ownership(generic_c_ptr, size, "Precondition ownership check"); + break; + } + case PUT: + { + cn_put_ownership(generic_c_ptr, size); + break; + } + case LOOP: { + cn_get_ownership(generic_c_ptr, size, "Loop invariant ownership check"); + } + } } From 4690478a5e97590f209e6b0d4fec1602539d13fa Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 20 Nov 2024 18:42:47 +0000 Subject: [PATCH 09/28] Fix binding issue so runtime memcpy loop invariant working --- backend/cn/lib/cn_internal_to_ail.ml | 16 ++++++++++------ backend/cn/lib/executable_spec_internal.ml | 1 - 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index c9d2359ac..4ef73df39 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -2814,6 +2814,7 @@ let cn_to_ail_resource_internal let cn_map_type = mk_ctype ~annots:[ CF.Annot.Atypedef (Sym.fresh_pretty "cn_map") ] C.Void in + Printf.printf "HERE IN MAP CREATE\n"; let sym_binding = create_binding sym (mk_ctype C.(Pointer (empty_qualifiers, cn_map_type))) in @@ -2863,7 +2864,7 @@ let cn_to_ail_resource_internal 0 )) in let ail_block = - A.(AilSblock ([], List.map mk_stmt [ start_assign; while_loop ])) + A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ])) in ([ sym_binding ], [ sym_decl; ail_block ]) in @@ -3329,10 +3330,10 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = let subst_loop = ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') in - let (_, (_, cond_ss)), (_, (loop_bs, loop_ss)) = + let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)) = cn_to_ail_loop_inv_aux dts globals preds subst_loop in - ( (cond_loc, ([], assign :: cond_ss)), + ( (cond_loc, (cond_bs, assign :: cond_ss)), (loop_loc, (binding :: loop_bs, decl :: loop_ss)) ) | L lat -> let rec modify_decls_for_loop decls modified_stats = @@ -3364,15 +3365,18 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = (decls @ [ none_decl ]) (modified_stats @ assign_stats) ss + (* | A.(AilSblock (bs, block_ss)) -> + let decls', modified_stats' = modify_decls_for_loop decls [] (List.map rm_stmt block_ss) in + modify_decls_for_loop (decls' @ decls) (modified_stats @ [A.(AilSblock (bs, (List.map mk_stmt modified_stats')))]) ss *) | _ -> modify_decls_for_loop decls (modified_stats @ [ s ]) ss) in let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in let decls, modified_stats = modify_decls_for_loop [] [] ss in - ((cond_loc, ([], modified_stats)), (loop_loc, (bs, decls))) + ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls))) let cn_to_ail_loop_inv dts globals preds ((cond_loc, loop_loc, _) as loop) = - let (_, (_, cond_ss)), (_, loop_bs_and_ss) = + let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss) = cn_to_ail_loop_inv_aux dts globals preds loop in let cn_stack_depth_incr_call = @@ -3396,7 +3400,7 @@ let cn_to_ail_loop_inv dts globals preds ((cond_loc, loop_loc, _) as loop) = in let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in - ((cond_loc, ([], [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss)) + ((cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss)) let prepend_to_precondition ail_executable_spec (b1, s1) = diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index 4399f4a28..dad4ca365 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -159,7 +159,6 @@ let generate_c_pres_and_posts_internal let split_x = String.split_on_char ';' x in let without_whitespace_x = remove_last split_x in let res = String.concat ";" without_whitespace_x in - Printf.printf "res: %s\n" res; [ res ] | x :: xs -> x :: remove_last_semicolon xs in From d85b1fcd2df229611a8ed2e74146a85e4eb564f7 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Thu, 21 Nov 2024 12:19:55 +0000 Subject: [PATCH 10/28] review changes --- backend/cn/lib/cn_internal_to_ail.ml | 5 ++--- backend/cn/lib/ownership_exec.ml | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 4ef73df39..cb153cc58 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -2637,7 +2637,7 @@ let cn_to_ail_resource_internal | Request.P p -> let ctype, bt = calculate_return_type p.name in let b, s, e = cn_to_ail_expr_internal dts globals p.pointer PassBack in - let enum_str = OE.get_enum_str_from_ownership_mode ownership_mode in + let enum_str = OE.ownership_mode_to_enum_str ownership_mode in let enum_str = if not is_toplevel then "owned_enum" else enum_str in let enum_sym = Sym.fresh_pretty enum_str in let rhs, bs, ss, _owned_ctype = @@ -2734,7 +2734,7 @@ let cn_to_ail_resource_internal let cn_pointer_return_type = bt_to_ail_ctype BT.(Loc ()) in let ptr_add_binding = create_binding ptr_add_sym cn_pointer_return_type in let ptr_add_stat = A.(AilSdeclaration [ (ptr_add_sym, Some e4) ]) in - let enum_str = OE.get_enum_str_from_ownership_mode ownership_mode in + let enum_str = OE.ownership_mode_to_enum_str ownership_mode in let enum_str = if not is_toplevel then "owned_enum" else enum_str in let enum_sym = Sym.fresh_pretty enum_str in let rhs, bs, ss, _owned_ctype = @@ -2814,7 +2814,6 @@ let cn_to_ail_resource_internal let cn_map_type = mk_ctype ~annots:[ CF.Annot.Atypedef (Sym.fresh_pretty "cn_map") ] C.Void in - Printf.printf "HERE IN MAP CREATE\n"; let sym_binding = create_binding sym (mk_ctype C.(Pointer (empty_qualifiers, cn_map_type))) in diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index cbabceaff..d7b740dc8 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -8,7 +8,7 @@ type ownership_mode = | Post | Loop -let get_enum_str_from_ownership_mode = function +let ownership_mode_to_enum_str = function | Pre -> "GET" | Post -> "PUT" | Loop -> "LOOP" From 4844e5ebb996c4d3533135cb8402420981442c14 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Thu, 21 Nov 2024 15:10:24 +0000 Subject: [PATCH 11/28] minor fixes --- backend/cn/lib/cn_internal_to_ail.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index cb153cc58..3222af754 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -557,7 +557,7 @@ let gen_bool_while_loop sym bt start_expr while_cond ?(if_cond_opt = None) (bs, [ A.( AilSif ( wrap_with_convert_from_cn_bool if_cond_expr, - mk_stmt (AilSblock ([], List.map mk_stmt (ss @ [ b_assign; incr_stat ]))), + mk_stmt (AilSblock ([], List.map mk_stmt (ss @ [ b_assign ]))), mk_stmt (AilSblock ([], [ mk_stmt AilSskip ])) )); incr_stat ] @@ -2806,7 +2806,7 @@ let cn_to_ail_resource_internal 0 )) in let ail_block = - A.(AilSblock ([], List.map mk_stmt [ start_assign; while_loop ])) + A.(AilSblock ([start_binding], List.map mk_stmt [ start_assign; while_loop ])) in ([], [ ail_block ]) | _ -> @@ -2867,7 +2867,7 @@ let cn_to_ail_resource_internal in ([ sym_binding ], [ sym_decl; ail_block ]) in - (b1 @ b2 @ b3 @ [ start_binding ] @ bs' @ bs, s1 @ s2 @ s3 @ ss @ ss') + (b1 @ b2 @ b3 @ bs' @ bs, s1 @ s2 @ s3 @ ss @ ss') let cn_to_ail_logical_constraint_internal @@ -3908,7 +3908,7 @@ let cn_to_ail_assume_resource_internal 0 )) in let ail_block = - A.(AilSblock ([], List.map mk_stmt [ start_assign; while_loop ])) + A.(AilSblock ([start_binding], List.map mk_stmt [ start_assign; while_loop ])) in ([], [ ail_block ]) | _ -> @@ -3965,11 +3965,11 @@ let cn_to_ail_assume_resource_internal 0 )) in let ail_block = - A.(AilSblock ([], List.map mk_stmt [ start_assign; while_loop ])) + A.(AilSblock ([start_binding], List.map mk_stmt [ start_assign; while_loop ])) in ([ sym_binding ], [ sym_decl; ail_block ]) in - (b1 @ b2 @ b3 @ [ start_binding ] @ bs' @ bs, s1 @ s2 @ s3 @ ss @ ss') + (b1 @ b2 @ b3 @ bs' @ bs, s1 @ s2 @ s3 @ ss @ ss') let rec cn_to_ail_assume_lat_internal dts pred_sym_opt globals preds = function From 1f5587ae2b6393fa3c76bc07575eca5f8ad71a8f Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Thu, 21 Nov 2024 16:17:14 +0000 Subject: [PATCH 12/28] Propagate executable spec Ctype printing in GCC statement as expression --- ocaml_frontend/pprinters/pp_ail.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ocaml_frontend/pprinters/pp_ail.ml b/ocaml_frontend/pprinters/pp_ail.ml index 2ac3dc067..ef37b4449 100644 --- a/ocaml_frontend/pprinters/pp_ail.ml +++ b/ocaml_frontend/pprinters/pp_ail.ml @@ -622,7 +622,7 @@ let rec pp_expression_aux ?(executable_spec=false) mk_pp_annot a_expr = | AilEprint_type e -> pp_ail_keyword "__cerb_printtype" ^^ P.parens (pp e) | AilEgcc_statement (bs, ss) -> - P.parens (pp_statement_aux mk_pp_annot ~bs:[] (AnnotatedStatement (Cerb_location.unknown, Annot.no_attributes, AilSblock (bs, ss)))) + P.parens (pp_statement_aux ~executable_spec mk_pp_annot ~bs:[] (AnnotatedStatement (Cerb_location.unknown, Annot.no_attributes, AilSblock (bs, ss)))) )) in pp None a_expr From 2a093fbdd58312c50bf7f4da66ae08eed7580293 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Thu, 21 Nov 2024 16:18:57 +0000 Subject: [PATCH 13/28] format --- backend/cn/lib/cn_internal_to_ail.ml | 6 +++--- backend/cn/lib/ownership_exec.ml | 6 +----- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 3222af754..ab629ebee 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -2806,7 +2806,7 @@ let cn_to_ail_resource_internal 0 )) in let ail_block = - A.(AilSblock ([start_binding], List.map mk_stmt [ start_assign; while_loop ])) + A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ])) in ([], [ ail_block ]) | _ -> @@ -3908,7 +3908,7 @@ let cn_to_ail_assume_resource_internal 0 )) in let ail_block = - A.(AilSblock ([start_binding], List.map mk_stmt [ start_assign; while_loop ])) + A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ])) in ([], [ ail_block ]) | _ -> @@ -3965,7 +3965,7 @@ let cn_to_ail_assume_resource_internal 0 )) in let ail_block = - A.(AilSblock ([start_binding], List.map mk_stmt [ start_assign; while_loop ])) + A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ])) in ([ sym_binding ], [ sym_decl; ail_block ]) in diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index d7b740dc8..0d464a8ba 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -8,11 +8,7 @@ type ownership_mode = | Post | Loop -let ownership_mode_to_enum_str = function - | Pre -> "GET" - | Post -> "PUT" - | Loop -> "LOOP" - +let ownership_mode_to_enum_str = function Pre -> "GET" | Post -> "PUT" | Loop -> "LOOP" let cn_ghost_state_sym = Sym.fresh_pretty "cn_ownership_global_ghost_state" From 317df4db5025d0f115fedcd48aeb9a9b54d76d7a Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 22 Nov 2024 01:10:30 +0000 Subject: [PATCH 14/28] experiments for not repeating bindings across loops --- backend/cn/lib/cn_internal_to_ail.ml | 95 ++++++++++++++-------- backend/cn/lib/cn_internal_to_ail.mli | 7 +- backend/cn/lib/executable_spec_internal.ml | 6 +- backend/cn/lib/executable_spec_utils.ml | 4 +- 4 files changed, 69 insertions(+), 43 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index ab629ebee..8af276b52 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -615,13 +615,12 @@ type ail_executable_spec = post : ail_bindings_and_statements; in_stmt : (Locations.t * ail_bindings_and_statements) list; loops : - ((Locations.t * ail_bindings_and_statements) - * (Locations.t * ail_bindings_and_statements)) - list + (Locations.t * ail_bindings_and_statements) list + * (Locations.t * ail_bindings_and_statements) list } let empty_ail_executable_spec = - { pre = ([], []); post = ([], []); in_stmt = []; loops = [] } + { pre = ([], []); post = ([], []); in_stmt = []; loops = ([], []) } type 'a dest = @@ -3314,26 +3313,32 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu (List.concat bs, List.concat ss) -let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = +let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (cond_loc, loop_loc, at) = match at with | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in - let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in - let binding = create_binding cn_sym cn_ctype in - (* TODO: Check this should always translate to the address of the given sym in the loop invariant case *) - let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in - let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in - let assign = - A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) - in let subst_loop = ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') in - let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)) = - cn_to_ail_loop_inv_aux dts globals preds subst_loop + let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)), _ = + cn_to_ail_loop_inv_aux dts globals preds (sym :: decl_syms) subst_loop + in + let ret_loop_bs, ret_loop_ss = + if List.mem Sym.equal sym decl_syms then + (loop_bs, loop_ss) + else ( + let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in + let binding = create_binding cn_sym cn_ctype in + let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in + (binding :: loop_bs, decl :: loop_ss)) + in + let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in + let assign = + A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) in ( (cond_loc, (cond_bs, assign :: cond_ss)), - (loop_loc, (binding :: loop_bs, decl :: loop_ss)) ) + (loop_loc, (ret_loop_bs, ret_loop_ss)), + sym :: decl_syms ) | L lat -> let rec modify_decls_for_loop decls modified_stats = let rec collect_initialised_syms_and_exprs = function @@ -3371,12 +3376,12 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = in let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in let decls, modified_stats = modify_decls_for_loop [] [] ss in - ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls))) + ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls)), decl_syms) -let cn_to_ail_loop_inv dts globals preds ((cond_loc, loop_loc, _) as loop) = - let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss) = - cn_to_ail_loop_inv_aux dts globals preds loop +let cn_to_ail_loop_inv dts globals preds decl_syms ((cond_loc, loop_loc, _) as loop) = + let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss), new_decl_syms = + cn_to_ail_loop_inv_aux dts globals preds decl_syms loop in let cn_stack_depth_incr_call = A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_incr_sym), []))) @@ -3399,7 +3404,9 @@ let cn_to_ail_loop_inv dts globals preds ((cond_loc, loop_loc, _) as loop) = in let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in - ((cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss)) + ( (cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), + (loop_loc, loop_bs_and_ss), + new_decl_syms ) let prepend_to_precondition ail_executable_spec (b1, s1) = @@ -3466,8 +3473,8 @@ let rec cn_to_ail_lat_internal_2 lat in prepend_to_precondition ail_executable_spec (b1, ss) - (* Postcondition *) - | LAT.I (post, (stats, loop)) -> + (* Postcondition, statements and loop invariants *) + | LAT.I (post, (stats, loops)) -> let rec remove_duplicates locs stats = match stats with | [] -> [] @@ -3512,7 +3519,32 @@ let rec cn_to_ail_lat_internal_2 let ail_statements = List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats in - let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds) loop in + let rec _get_ail_loop_invariants dts globals preds decl_syms = function + | [] -> ([], []) + | l :: ls -> + let cond_ail, loop_decl_ail, new_decl_syms = + cn_to_ail_loop_inv dts globals preds decl_syms l + in + let cond_ails, loop_decl_ails = + _get_ail_loop_invariants dts globals preds new_decl_syms ls + in + (cond_ail :: cond_ails, loop_decl_ail :: loop_decl_ails) + in + (* let ail_loop_invariants = get_ail_loop_invariants dts globals preds [] loops in *) + let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds []) loops in + let cond_stats, loop_decls, _ = + Executable_spec_utils.list_split_three ail_loop_invariants + in + (* let (cond_stats, loop_decls) = List.split ail_loop_invariants in *) + (* let rec shift_loop_decls = function + | [] -> [] + | [(_, (bs, ss))] -> [(Cerb_location.unknown, (bs, ss))] + | (loc, (decl_bs, decl_ss)) :: ds -> + let ds_bs_and_ss = shift_loop_decls ds in + let (ds_bs, ds_ss) = List.split (List.map snd ds_bs_and_ss) in + [loc, (decl_bs @ (List.concat ds_bs), decl_ss @ (List.concat ds_ss))] + in *) + (* let modified_ail_loop_invariants = (cond_stats, (loop_decls)) in *) let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in let ownership_stats_ = if without_ownership_checking then @@ -3531,11 +3563,11 @@ let rec cn_to_ail_lat_internal_2 { pre = ([], []); post = ([], [ block ]); in_stmt = ail_statements; - loops = ail_loop_invariants + loops = (cond_stats, loop_decls) } -let rec cn_to_ail_pre_post_aux_internal +let rec cn_to_ail_executable_spec_aux without_ownership_checking dts preds @@ -3550,7 +3582,7 @@ let rec cn_to_ail_pre_post_aux_internal let decl = A.(AilSdeclaration [ (cn_sym, Some (mk_expr rhs)) ]) in let subst_at = ESE.fn_args_and_body_subst (ESE.sym_subst (sym, bt, cn_sym)) at in let ail_executable_spec = - cn_to_ail_pre_post_aux_internal + cn_to_ail_executable_spec_aux without_ownership_checking dts preds @@ -3569,16 +3601,11 @@ let rec cn_to_ail_pre_post_aux_internal lat -let cn_to_ail_pre_post_internal - ~without_ownership_checking - dts - preds - globals - c_return_type +let cn_to_ail_executable_spec ~without_ownership_checking dts preds globals c_return_type = function | Some internal -> let ail_executable_spec = - cn_to_ail_pre_post_aux_internal + cn_to_ail_executable_spec_aux without_ownership_checking dts preds diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli index a0d1e2aba..61afa19b3 100644 --- a/backend/cn/lib/cn_internal_to_ail.mli +++ b/backend/cn/lib/cn_internal_to_ail.mli @@ -56,9 +56,8 @@ type ail_executable_spec = post : ail_bindings_and_statements; in_stmt : (Locations.t * ail_bindings_and_statements) list; loops : - ((Locations.t * ail_bindings_and_statements) - * (Locations.t * ail_bindings_and_statements)) - list + (Locations.t * ail_bindings_and_statements) list + * (Locations.t * ail_bindings_and_statements) list } val generate_get_or_put_ownership_function @@ -170,7 +169,7 @@ val cn_to_ail_predicates_internal list * A.sigma_tag_definition option list -val cn_to_ail_pre_post_internal +val cn_to_ail_executable_spec : without_ownership_checking:bool -> A.sigma_cn_datatype list -> (Sym.t * Definition.Predicate.t) list -> diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index dad4ca365..d55156943 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -70,7 +70,7 @@ let generate_c_pres_and_posts_internal in let globals = extract_global_variables prog5.globs in let ail_executable_spec = - Cn_internal_to_ail.cn_to_ail_pre_post_internal + Cn_internal_to_ail.cn_to_ail_executable_spec ~without_ownership_checking dts preds @@ -145,8 +145,8 @@ let generate_c_pres_and_posts_internal (fun (loc, e_opt, strs) -> (loc, e_opt, [ String.concat "\n" strs ])) return_ownership_stmts in - let ail_loop_invariants = ail_executable_spec.loops in - let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in + let ail_cond_stats, ail_loop_decls = ail_executable_spec.loops in + (* let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in *) (* A bit of a hack *) let rec remove_last = function | [] -> [] diff --git a/backend/cn/lib/executable_spec_utils.ml b/backend/cn/lib/executable_spec_utils.ml index a1619638d..d4774e1c7 100644 --- a/backend/cn/lib/executable_spec_utils.ml +++ b/backend/cn/lib/executable_spec_utils.ml @@ -167,7 +167,7 @@ let get_start_loc ?(offset = 0) = function Cerb_location.point new_start_pos | None -> failwith - "get_start_loc: Loc_regions has empty list of positions (should be non-empty)") + (__FUNCTION__ ^ ": Loc_regions has empty list of positions (should be non-empty)")) | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } | Loc_unknown | Loc_other _ -> failwith "get_start_loc: Location should be Loc_region, Loc_regions or Loc_point" @@ -184,7 +184,7 @@ let get_end_loc ?(offset = 0) = function Cerb_location.point new_end_pos | None -> failwith - "get_end_loc: Loc_regions has empty list of positions (should be non-empty)") + (__FUNCTION__ ^ ": Loc_regions has empty list of positions (should be non-empty)")) | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } | Loc_unknown | Loc_other _ -> failwith "get_end_loc: Location should be Loc_region, Loc_regions or Loc_point" From 42ed2f66a84f1d08adc6e6a109359d5dbbe13fe0 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Mon, 30 Dec 2024 14:34:19 +0000 Subject: [PATCH 15/28] Pre-deadline loop invariant changes --- backend/cn/lib/cn_internal_to_ail.ml | 99 ++++++++++++++-------- backend/cn/lib/cn_internal_to_ail.mli | 2 + backend/cn/lib/executable_spec_extract.ml | 10 +-- backend/cn/lib/executable_spec_extract.mli | 2 +- backend/cn/lib/executable_spec_internal.ml | 20 +++-- backend/cn/lib/executable_spec_records.ml | 2 +- backend/cn/lib/ownership_exec.ml | 21 +++-- 7 files changed, 98 insertions(+), 58 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 8af276b52..5ca32c6b2 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3287,57 +3287,49 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu let binding = create_binding name ctype in let decl = A.(AilSdeclaration [ (name, None) ]) in let b1, s1 = cn_to_ail_expr_internal dts globals it (AssignVar name) in - let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in - (b1 @ b2 @ [ binding ], (decl :: s1) @ s2) + let (b2, s2), cn_stat_locs_bs_and_ss = + cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat + in + ((b1 @ b2 @ [ binding ], (decl :: s1) @ s2), cn_stat_locs_bs_and_ss) | LAT.Resource ((name, (ret, _bt)), (loc, _str_opt), lat) -> let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in let b1, s1 = cn_to_ail_resource_internal ~is_toplevel name dts globals preds OE.Loop loc ret in - let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in - (b1 @ b2, upd_s @ s1 @ pop_s @ s2) + let (b2, s2), cn_stat_locs_bs_and_ss = + cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat + in + ((b1 @ b2, upd_s @ s1 @ pop_s @ s2), cn_stat_locs_bs_and_ss) | LAT.Constraint (lc, (loc, _str_opt), lat) -> let b1, s, e = cn_to_ail_logical_constraint_internal dts globals PassBack lc in let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in let ss = upd_s @ s @ generate_cn_assert (*~cn_source_loc_opt:(Some loc)*) e @ pop_s in - let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in - (b1 @ b2, ss @ s2) + let (b2, s2), cn_stat_locs_bs_and_ss = + cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat + in + ((b1 @ b2, ss @ s2), cn_stat_locs_bs_and_ss) | LAT.I ss -> let ail_statements = List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) ss in - let _, bs_and_ss = List.split ail_statements in - let bs, ss = List.split bs_and_ss in - (List.concat bs, List.concat ss) + (([], []), ail_statements) -let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (cond_loc, loop_loc, at) = +let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (s, (cond_loc, loop_loc, at)) = match at with | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in let subst_loop = - ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') + ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (s, (cond_loc, loop_loc, at')) in - let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)), _ = + let ((_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)), cn_stat_loc_bs_and_ss), _ = cn_to_ail_loop_inv_aux dts globals preds (sym :: decl_syms) subst_loop in - let ret_loop_bs, ret_loop_ss = - if List.mem Sym.equal sym decl_syms then - (loop_bs, loop_ss) - else ( - let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in - let binding = create_binding cn_sym cn_ctype in - let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in - (binding :: loop_bs, decl :: loop_ss)) - in - let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in - let assign = - A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) - in - ( (cond_loc, (cond_bs, assign :: cond_ss)), - (loop_loc, (ret_loop_bs, ret_loop_ss)), + ( ( (cond_loc, (cond_bs, cond_ss)), + (loop_loc, (loop_bs, loop_ss)), + cn_stat_loc_bs_and_ss ), sym :: decl_syms ) | L lat -> let rec modify_decls_for_loop decls modified_stats = @@ -3374,13 +3366,29 @@ let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (cond_loc, loop_loc, modify_decls_for_loop (decls' @ decls) (modified_stats @ [A.(AilSblock (bs, (List.map mk_stmt modified_stats')))]) ss *) | _ -> modify_decls_for_loop decls (modified_stats @ [ s ]) ss) in - let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in + let (bs, ss), cn_stat_loc_bs_and_ss = + cn_to_ail_lat_internal_loop dts globals preds lat + in let decls, modified_stats = modify_decls_for_loop [] [] ss in - ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls)), decl_syms) + ( ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls)), cn_stat_loc_bs_and_ss), + decl_syms ) -let cn_to_ail_loop_inv dts globals preds decl_syms ((cond_loc, loop_loc, _) as loop) = - let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss), new_decl_syms = +let cn_to_ail_loop_inv dts globals preds decl_syms ((s, (cond_loc, loop_loc, at)) as loop) + = + Printf.printf "Loop sym: %s\n" (Sym.pp_string s); + Printf.printf + "Loop invariant argument types: %s\n" + (CF.Pp_utils.to_plain_pretty_string + (AT.pp + (fun statements -> + Pp.separate_map + Pp.comma + (fun (loc, _statement) -> Locations.pp loc) + statements) + at)); + let ((_, (cond_bs, cond_ss)), (_, loop_bs_and_ss), cn_stat_loc_bs_and_ss), new_decl_syms + = cn_to_ail_loop_inv_aux dts globals preds decl_syms loop in let cn_stack_depth_incr_call = @@ -3404,11 +3412,23 @@ let cn_to_ail_loop_inv dts globals preds decl_syms ((cond_loc, loop_loc, _) as l in let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in - ( (cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), - (loop_loc, loop_bs_and_ss), + ( ( (cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), + (loop_loc, loop_bs_and_ss), + cn_stat_loc_bs_and_ss ), new_decl_syms ) +let generate_cn_addr_var_bs_and_ss sym = + let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in + let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in + let binding = create_binding cn_sym cn_ctype in + let rhs = + wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) (BT.Loc ()) + in + let decl = A.(AilSdeclaration [ (cn_sym, Some (mk_expr rhs)) ]) in + ([ binding ], [ decl ]) + + let prepend_to_precondition ail_executable_spec (b1, s1) = let b2, s2 = ail_executable_spec.pre in { ail_executable_spec with pre = (b1 @ b2, s1 @ s2) } @@ -3522,7 +3542,7 @@ let rec cn_to_ail_lat_internal_2 let rec _get_ail_loop_invariants dts globals preds decl_syms = function | [] -> ([], []) | l :: ls -> - let cond_ail, loop_decl_ail, new_decl_syms = + let (cond_ail, loop_decl_ail, _), new_decl_syms = cn_to_ail_loop_inv dts globals preds decl_syms l in let cond_ails, loop_decl_ails = @@ -3532,8 +3552,12 @@ let rec cn_to_ail_lat_internal_2 in (* let ail_loop_invariants = get_ail_loop_invariants dts globals preds [] loops in *) let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds []) loops in - let cond_stats, loop_decls, _ = - Executable_spec_utils.list_split_three ail_loop_invariants + let stats, _ = List.split ail_loop_invariants in + let cond_stats, loop_decls, cn_stat_locs_bs_and_ss = + Executable_spec_utils.list_split_three stats + in + let all_ail_statements = + remove_duplicates [] (ail_statements @ List.concat cn_stat_locs_bs_and_ss) in (* let (cond_stats, loop_decls) = List.split ail_loop_invariants in *) (* let rec shift_loop_decls = function @@ -3562,7 +3586,8 @@ let rec cn_to_ail_lat_internal_2 in { pre = ([], []); post = ([], [ block ]); - in_stmt = ail_statements; + in_stmt = all_ail_statements; + (* @ (List.concat cn_stat_locs_bs_and_ss); *) loops = (cond_stats, loop_decls) } diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli index 61afa19b3..1cf15ce93 100644 --- a/backend/cn/lib/cn_internal_to_ail.mli +++ b/backend/cn/lib/cn_internal_to_ail.mli @@ -60,6 +60,8 @@ type ail_executable_spec = * (Locations.t * ail_bindings_and_statements) list } +val generate_cn_addr_var_bs_and_ss : Sym.t -> ail_bindings_and_statements + val generate_get_or_put_ownership_function : without_ownership_checking:bool -> C.ctype -> diff --git a/backend/cn/lib/executable_spec_extract.ml b/backend/cn/lib/executable_spec_extract.ml index 4c878ddc6..cbf5f165e 100644 --- a/backend/cn/lib/executable_spec_extract.ml +++ b/backend/cn/lib/executable_spec_extract.ml @@ -10,10 +10,10 @@ type statements = statement list let statements_subst subst = List.map (statement_subst subst) -type loop = Locations.t * Locations.t * statements ArgumentTypes.t +type loop = Sym.t * (Locations.t * Locations.t * statements ArgumentTypes.t) -let loop_subst subst ((cond_loc, loop_loc, at) : loop) = - (cond_loc, loop_loc, ArgumentTypes.subst statements_subst subst at) +let loop_subst subst ((s, (cond_loc, loop_loc, at)) : loop) = + (s, (cond_loc, loop_loc, ArgumentTypes.subst statements_subst subst at)) type loops = loop list @@ -103,13 +103,13 @@ let rec stmts_in_expr (Mucore.Expr (loc, _, _, e_)) = | CN_progs (_stmts_s, stmts_i) -> [ (loc, stmts_i) ] -let from_loop ((_label_sym : Sym.t), (label_def : _ label_def)) : loop option = +let from_loop ((label_sym : Sym.t), (label_def : _ label_def)) : loop option = match label_def with | Return _ -> None | Label (_loc, label_args_and_body, _annots, _, `Loop (loop_condition_loc, loop_loc)) -> let label_args_and_body = Core_to_mucore.at_of_arguments Fun.id label_args_and_body in let label_args_and_statements = ArgumentTypes.map stmts_in_expr label_args_and_body in - Some (loop_condition_loc, loop_loc, label_args_and_statements) + Some (label_sym, (loop_condition_loc, loop_loc, label_args_and_statements)) let from_fn (fn, decl) = diff --git a/backend/cn/lib/executable_spec_extract.mli b/backend/cn/lib/executable_spec_extract.mli index cc039f3b3..ad60433d5 100644 --- a/backend/cn/lib/executable_spec_extract.mli +++ b/backend/cn/lib/executable_spec_extract.mli @@ -2,7 +2,7 @@ type statement = Locations.t * Cnprog.t list type statements = statement list -type loop = Locations.t * Locations.t * statements ArgumentTypes.t +type loop = Sym.t * (Locations.t * Locations.t * statements ArgumentTypes.t) (* first location is for the loop condition; second is for the entire loop *) type loops = loop list diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index d55156943..f41de873f 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -89,8 +89,17 @@ let generate_c_pres_and_posts_internal Ownership_exec.get_c_fn_local_ownership_checking_injs instrumentation.fn sigm in match fn_ownership_stats_opt with - | Some (entry_ownership_stats, exit_ownership_stats) -> - let entry_ownership_str = generate_ail_stat_strs ([], entry_ownership_stats) in + | Some ((entry_ownership_stats, exit_ownership_stats), params) -> + let cn_addr_bs_and_ss = + List.map + (fun (sym, _) -> Cn_internal_to_ail.generate_cn_addr_var_bs_and_ss sym) + params + in + let cn_addr_bs, cn_addr_decls = List.split cn_addr_bs_and_ss in + let entry_ownership_str = + generate_ail_stat_strs + (List.concat cn_addr_bs, entry_ownership_stats @ List.concat cn_addr_decls) + in let exit_ownership_str = generate_ail_stat_strs ([], exit_ownership_stats) in let pre_post_pair = ( pre_str @ ("\n\t/* C OWNERSHIP */\n\n" :: entry_ownership_str), @@ -119,16 +128,17 @@ let generate_c_pres_and_posts_internal in let return_injs = List.filter_map - (fun (loc, e_opt, bs, ss) -> + (fun ((loc, e_opt, bs, ss), _) -> match e_opt with Some e_opt' -> Some (loc, e_opt', bs, ss) | None -> None) block_ownership_injs in let non_return_injs = - List.filter (fun (_, e_opt, _, _) -> Option.is_none e_opt) block_ownership_injs + List.filter (fun ((_, e_opt, _, _), _) -> Option.is_none e_opt) block_ownership_injs in let block_ownership_stmts = List.map - (fun (loc, _, bs, ss) -> (loc, generate_ail_stat_strs ~with_newline:true (bs, ss))) + (fun ((loc, _, bs, ss), _) -> + (loc, generate_ail_stat_strs ~with_newline:true (bs, ss))) non_return_injs in let block_ownership_stmts = diff --git a/backend/cn/lib/executable_spec_records.ml b/backend/cn/lib/executable_spec_records.ml index 574ab3e20..544313e05 100644 --- a/backend/cn/lib/executable_spec_records.ml +++ b/backend/cn/lib/executable_spec_records.ml @@ -122,7 +122,7 @@ let add_records_to_map_from_instrumentation (i : Executable_spec_extract.instrum aux_rt rt; List.iter add_records_to_map_from_cnprogs stmts; List.iter - (fun (_loc1, _loc2, loop_at) -> + (fun (_, (_loc1, _loc2, loop_at)) -> let loop_stmts = aux_at loop_at in List.iter add_records_to_map_from_cnprogs loop_stmts) loops diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index 0d464a8ba..f68c18da4 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -97,7 +97,7 @@ let rec gen_loop_ownership_entry_decls bindings = function let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = if dest_is_loop then ( let new_bindings, new_decls = gen_loop_ownership_entry_decls bindings decls in - [ (loc, new_bindings, [ A.AilSdeclaration new_decls ]) ]) + [ ((loc, new_bindings, [ A.AilSdeclaration new_decls ]), List.map fst new_decls) ]) else ( let stats_ = List.map @@ -107,7 +107,7 @@ let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = A.(AilSexpr entry_fcall)) decls in - [ (get_end_loc loc, [], stats_) ]) + [ ((get_end_loc loc, [], stats_), List.map fst decls) ]) (* c_remove_local_footprint((uintptr_t) &xs, cn_ownership_global_ghost_state, @@ -248,7 +248,7 @@ let rec get_c_block_entry_exit_injs_aux bindings A.(AnnotatedStatement (loc, _, [ generate_c_local_ownership_exit (b_sym, b_ctype) ] )) bs in - let exit_injs' = List.map (fun (loc, stats) -> (loc, [], stats)) exit_injs in + let exit_injs' = List.map (fun (loc, stats) -> ((loc, [], stats), [])) exit_injs in let stat_injs = List.map (fun s -> get_c_block_entry_exit_injs_aux bs s) ss in List.concat stat_injs @ exit_injs' | AilSif (_, s1, s2) -> @@ -270,19 +270,19 @@ let rec get_c_block_entry_exit_injs_aux bindings A.(AnnotatedStatement (loc, _, let get_c_block_entry_exit_injs stat = let injs = get_c_block_entry_exit_injs_aux [] stat in - List.map (fun (loc, bs, ss) -> (loc, None, bs, ss)) injs + List.map (fun ((loc, bs, ss), syms) -> ((loc, None, bs, ss), syms)) injs let rec combine_injs_over_location loc = function | [] -> [] - | (loc', expr_opt, bs, inj_stmt) :: injs' -> + | ((loc', expr_opt, bs, inj_stmt), syms) :: injs' -> let stmt = if String.equal (Cerb_location.location_to_string loc) (Cerb_location.location_to_string loc') then - [ (expr_opt, bs, inj_stmt) ] + [ ((expr_opt, bs, inj_stmt), syms) ] else [] in @@ -317,18 +317,21 @@ let get_c_block_local_ownership_checking_injs | A.(AilSblock _) -> let injs = get_c_block_entry_exit_injs statement in let injs' = get_c_control_flow_block_unmaps statement in + let injs' = List.map (fun (l, r, s, b) -> ((l, r, s, b), [])) injs' in let injs = injs @ injs' in - let locs = List.map (fun (l, _, _, _) -> l) injs in + let locs = List.map (fun ((l, _, _, _), _) -> l) injs in let locs = remove_duplicates [] locs in let combined_injs = List.map (fun l -> let injs' = combine_injs_over_location l injs in + let injs', syms = List.split injs' in let expr_opt_list, bs_list, stats_list = Executable_spec_utils.list_split_three injs' in let return_expr_opt = get_return_expr_opt expr_opt_list in - (l, return_expr_opt, List.concat bs_list, List.concat stats_list)) + ( (l, return_expr_opt, List.concat bs_list, List.concat stats_list), + List.concat syms )) locs in combined_injs @@ -353,5 +356,5 @@ let get_c_fn_local_ownership_checking_injs let ownership_stats_pair = get_c_local_ownership_checking params in (* TODO: Separate return injections here since they are now done differently *) let block_ownership_injs = get_c_block_local_ownership_checking_injs fn_body in - (Some ownership_stats_pair, block_ownership_injs) + (Some (ownership_stats_pair, params), block_ownership_injs) | _, _ -> (None, []) From 3ab224016fa174bbd68575e4c903d5396325eebc Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 3 Jan 2025 12:04:42 +0000 Subject: [PATCH 16/28] Revert "Pre-deadline loop invariant changes" This reverts commit 20a763c99bd2b3490d907ebed6dbc39d7bdaf520. --- backend/cn/lib/cn_internal_to_ail.ml | 99 ++++++++-------------- backend/cn/lib/cn_internal_to_ail.mli | 2 - backend/cn/lib/executable_spec_extract.ml | 10 +-- backend/cn/lib/executable_spec_extract.mli | 2 +- backend/cn/lib/executable_spec_internal.ml | 20 ++--- backend/cn/lib/executable_spec_records.ml | 2 +- backend/cn/lib/ownership_exec.ml | 21 ++--- 7 files changed, 58 insertions(+), 98 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 5ca32c6b2..8af276b52 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3287,49 +3287,57 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu let binding = create_binding name ctype in let decl = A.(AilSdeclaration [ (name, None) ]) in let b1, s1 = cn_to_ail_expr_internal dts globals it (AssignVar name) in - let (b2, s2), cn_stat_locs_bs_and_ss = - cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat - in - ((b1 @ b2 @ [ binding ], (decl :: s1) @ s2), cn_stat_locs_bs_and_ss) + let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in + (b1 @ b2 @ [ binding ], (decl :: s1) @ s2) | LAT.Resource ((name, (ret, _bt)), (loc, _str_opt), lat) -> let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in let b1, s1 = cn_to_ail_resource_internal ~is_toplevel name dts globals preds OE.Loop loc ret in - let (b2, s2), cn_stat_locs_bs_and_ss = - cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat - in - ((b1 @ b2, upd_s @ s1 @ pop_s @ s2), cn_stat_locs_bs_and_ss) + let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in + (b1 @ b2, upd_s @ s1 @ pop_s @ s2) | LAT.Constraint (lc, (loc, _str_opt), lat) -> let b1, s, e = cn_to_ail_logical_constraint_internal dts globals PassBack lc in let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) () in let pop_s = generate_cn_pop_msg_info in let ss = upd_s @ s @ generate_cn_assert (*~cn_source_loc_opt:(Some loc)*) e @ pop_s in - let (b2, s2), cn_stat_locs_bs_and_ss = - cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat - in - ((b1 @ b2, ss @ s2), cn_stat_locs_bs_and_ss) + let b2, s2 = cn_to_ail_lat_internal_loop ~is_toplevel dts globals preds lat in + (b1 @ b2, ss @ s2) | LAT.I ss -> let ail_statements = List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) ss in - (([], []), ail_statements) + let _, bs_and_ss = List.split ail_statements in + let bs, ss = List.split bs_and_ss in + (List.concat bs, List.concat ss) -let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (s, (cond_loc, loop_loc, at)) = +let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (cond_loc, loop_loc, at) = match at with | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in let subst_loop = - ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (s, (cond_loc, loop_loc, at')) + ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') in - let ((_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)), cn_stat_loc_bs_and_ss), _ = + let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)), _ = cn_to_ail_loop_inv_aux dts globals preds (sym :: decl_syms) subst_loop in - ( ( (cond_loc, (cond_bs, cond_ss)), - (loop_loc, (loop_bs, loop_ss)), - cn_stat_loc_bs_and_ss ), + let ret_loop_bs, ret_loop_ss = + if List.mem Sym.equal sym decl_syms then + (loop_bs, loop_ss) + else ( + let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in + let binding = create_binding cn_sym cn_ctype in + let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in + (binding :: loop_bs, decl :: loop_ss)) + in + let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in + let assign = + A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) + in + ( (cond_loc, (cond_bs, assign :: cond_ss)), + (loop_loc, (ret_loop_bs, ret_loop_ss)), sym :: decl_syms ) | L lat -> let rec modify_decls_for_loop decls modified_stats = @@ -3366,29 +3374,13 @@ let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (s, (cond_loc, loop_l modify_decls_for_loop (decls' @ decls) (modified_stats @ [A.(AilSblock (bs, (List.map mk_stmt modified_stats')))]) ss *) | _ -> modify_decls_for_loop decls (modified_stats @ [ s ]) ss) in - let (bs, ss), cn_stat_loc_bs_and_ss = - cn_to_ail_lat_internal_loop dts globals preds lat - in + let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in let decls, modified_stats = modify_decls_for_loop [] [] ss in - ( ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls)), cn_stat_loc_bs_and_ss), - decl_syms ) + ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls)), decl_syms) -let cn_to_ail_loop_inv dts globals preds decl_syms ((s, (cond_loc, loop_loc, at)) as loop) - = - Printf.printf "Loop sym: %s\n" (Sym.pp_string s); - Printf.printf - "Loop invariant argument types: %s\n" - (CF.Pp_utils.to_plain_pretty_string - (AT.pp - (fun statements -> - Pp.separate_map - Pp.comma - (fun (loc, _statement) -> Locations.pp loc) - statements) - at)); - let ((_, (cond_bs, cond_ss)), (_, loop_bs_and_ss), cn_stat_loc_bs_and_ss), new_decl_syms - = +let cn_to_ail_loop_inv dts globals preds decl_syms ((cond_loc, loop_loc, _) as loop) = + let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss), new_decl_syms = cn_to_ail_loop_inv_aux dts globals preds decl_syms loop in let cn_stack_depth_incr_call = @@ -3412,23 +3404,11 @@ let cn_to_ail_loop_inv dts globals preds decl_syms ((s, (cond_loc, loop_loc, at) in let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in - ( ( (cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), - (loop_loc, loop_bs_and_ss), - cn_stat_loc_bs_and_ss ), + ( (cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), + (loop_loc, loop_bs_and_ss), new_decl_syms ) -let generate_cn_addr_var_bs_and_ss sym = - let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in - let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in - let binding = create_binding cn_sym cn_ctype in - let rhs = - wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) (BT.Loc ()) - in - let decl = A.(AilSdeclaration [ (cn_sym, Some (mk_expr rhs)) ]) in - ([ binding ], [ decl ]) - - let prepend_to_precondition ail_executable_spec (b1, s1) = let b2, s2 = ail_executable_spec.pre in { ail_executable_spec with pre = (b1 @ b2, s1 @ s2) } @@ -3542,7 +3522,7 @@ let rec cn_to_ail_lat_internal_2 let rec _get_ail_loop_invariants dts globals preds decl_syms = function | [] -> ([], []) | l :: ls -> - let (cond_ail, loop_decl_ail, _), new_decl_syms = + let cond_ail, loop_decl_ail, new_decl_syms = cn_to_ail_loop_inv dts globals preds decl_syms l in let cond_ails, loop_decl_ails = @@ -3552,12 +3532,8 @@ let rec cn_to_ail_lat_internal_2 in (* let ail_loop_invariants = get_ail_loop_invariants dts globals preds [] loops in *) let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds []) loops in - let stats, _ = List.split ail_loop_invariants in - let cond_stats, loop_decls, cn_stat_locs_bs_and_ss = - Executable_spec_utils.list_split_three stats - in - let all_ail_statements = - remove_duplicates [] (ail_statements @ List.concat cn_stat_locs_bs_and_ss) + let cond_stats, loop_decls, _ = + Executable_spec_utils.list_split_three ail_loop_invariants in (* let (cond_stats, loop_decls) = List.split ail_loop_invariants in *) (* let rec shift_loop_decls = function @@ -3586,8 +3562,7 @@ let rec cn_to_ail_lat_internal_2 in { pre = ([], []); post = ([], [ block ]); - in_stmt = all_ail_statements; - (* @ (List.concat cn_stat_locs_bs_and_ss); *) + in_stmt = ail_statements; loops = (cond_stats, loop_decls) } diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli index 1cf15ce93..61afa19b3 100644 --- a/backend/cn/lib/cn_internal_to_ail.mli +++ b/backend/cn/lib/cn_internal_to_ail.mli @@ -60,8 +60,6 @@ type ail_executable_spec = * (Locations.t * ail_bindings_and_statements) list } -val generate_cn_addr_var_bs_and_ss : Sym.t -> ail_bindings_and_statements - val generate_get_or_put_ownership_function : without_ownership_checking:bool -> C.ctype -> diff --git a/backend/cn/lib/executable_spec_extract.ml b/backend/cn/lib/executable_spec_extract.ml index cbf5f165e..4c878ddc6 100644 --- a/backend/cn/lib/executable_spec_extract.ml +++ b/backend/cn/lib/executable_spec_extract.ml @@ -10,10 +10,10 @@ type statements = statement list let statements_subst subst = List.map (statement_subst subst) -type loop = Sym.t * (Locations.t * Locations.t * statements ArgumentTypes.t) +type loop = Locations.t * Locations.t * statements ArgumentTypes.t -let loop_subst subst ((s, (cond_loc, loop_loc, at)) : loop) = - (s, (cond_loc, loop_loc, ArgumentTypes.subst statements_subst subst at)) +let loop_subst subst ((cond_loc, loop_loc, at) : loop) = + (cond_loc, loop_loc, ArgumentTypes.subst statements_subst subst at) type loops = loop list @@ -103,13 +103,13 @@ let rec stmts_in_expr (Mucore.Expr (loc, _, _, e_)) = | CN_progs (_stmts_s, stmts_i) -> [ (loc, stmts_i) ] -let from_loop ((label_sym : Sym.t), (label_def : _ label_def)) : loop option = +let from_loop ((_label_sym : Sym.t), (label_def : _ label_def)) : loop option = match label_def with | Return _ -> None | Label (_loc, label_args_and_body, _annots, _, `Loop (loop_condition_loc, loop_loc)) -> let label_args_and_body = Core_to_mucore.at_of_arguments Fun.id label_args_and_body in let label_args_and_statements = ArgumentTypes.map stmts_in_expr label_args_and_body in - Some (label_sym, (loop_condition_loc, loop_loc, label_args_and_statements)) + Some (loop_condition_loc, loop_loc, label_args_and_statements) let from_fn (fn, decl) = diff --git a/backend/cn/lib/executable_spec_extract.mli b/backend/cn/lib/executable_spec_extract.mli index ad60433d5..cc039f3b3 100644 --- a/backend/cn/lib/executable_spec_extract.mli +++ b/backend/cn/lib/executable_spec_extract.mli @@ -2,7 +2,7 @@ type statement = Locations.t * Cnprog.t list type statements = statement list -type loop = Sym.t * (Locations.t * Locations.t * statements ArgumentTypes.t) +type loop = Locations.t * Locations.t * statements ArgumentTypes.t (* first location is for the loop condition; second is for the entire loop *) type loops = loop list diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index f41de873f..d55156943 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -89,17 +89,8 @@ let generate_c_pres_and_posts_internal Ownership_exec.get_c_fn_local_ownership_checking_injs instrumentation.fn sigm in match fn_ownership_stats_opt with - | Some ((entry_ownership_stats, exit_ownership_stats), params) -> - let cn_addr_bs_and_ss = - List.map - (fun (sym, _) -> Cn_internal_to_ail.generate_cn_addr_var_bs_and_ss sym) - params - in - let cn_addr_bs, cn_addr_decls = List.split cn_addr_bs_and_ss in - let entry_ownership_str = - generate_ail_stat_strs - (List.concat cn_addr_bs, entry_ownership_stats @ List.concat cn_addr_decls) - in + | Some (entry_ownership_stats, exit_ownership_stats) -> + let entry_ownership_str = generate_ail_stat_strs ([], entry_ownership_stats) in let exit_ownership_str = generate_ail_stat_strs ([], exit_ownership_stats) in let pre_post_pair = ( pre_str @ ("\n\t/* C OWNERSHIP */\n\n" :: entry_ownership_str), @@ -128,17 +119,16 @@ let generate_c_pres_and_posts_internal in let return_injs = List.filter_map - (fun ((loc, e_opt, bs, ss), _) -> + (fun (loc, e_opt, bs, ss) -> match e_opt with Some e_opt' -> Some (loc, e_opt', bs, ss) | None -> None) block_ownership_injs in let non_return_injs = - List.filter (fun ((_, e_opt, _, _), _) -> Option.is_none e_opt) block_ownership_injs + List.filter (fun (_, e_opt, _, _) -> Option.is_none e_opt) block_ownership_injs in let block_ownership_stmts = List.map - (fun ((loc, _, bs, ss), _) -> - (loc, generate_ail_stat_strs ~with_newline:true (bs, ss))) + (fun (loc, _, bs, ss) -> (loc, generate_ail_stat_strs ~with_newline:true (bs, ss))) non_return_injs in let block_ownership_stmts = diff --git a/backend/cn/lib/executable_spec_records.ml b/backend/cn/lib/executable_spec_records.ml index 544313e05..574ab3e20 100644 --- a/backend/cn/lib/executable_spec_records.ml +++ b/backend/cn/lib/executable_spec_records.ml @@ -122,7 +122,7 @@ let add_records_to_map_from_instrumentation (i : Executable_spec_extract.instrum aux_rt rt; List.iter add_records_to_map_from_cnprogs stmts; List.iter - (fun (_, (_loc1, _loc2, loop_at)) -> + (fun (_loc1, _loc2, loop_at) -> let loop_stmts = aux_at loop_at in List.iter add_records_to_map_from_cnprogs loop_stmts) loops diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index f68c18da4..0d464a8ba 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -97,7 +97,7 @@ let rec gen_loop_ownership_entry_decls bindings = function let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = if dest_is_loop then ( let new_bindings, new_decls = gen_loop_ownership_entry_decls bindings decls in - [ ((loc, new_bindings, [ A.AilSdeclaration new_decls ]), List.map fst new_decls) ]) + [ (loc, new_bindings, [ A.AilSdeclaration new_decls ]) ]) else ( let stats_ = List.map @@ -107,7 +107,7 @@ let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = A.(AilSexpr entry_fcall)) decls in - [ ((get_end_loc loc, [], stats_), List.map fst decls) ]) + [ (get_end_loc loc, [], stats_) ]) (* c_remove_local_footprint((uintptr_t) &xs, cn_ownership_global_ghost_state, @@ -248,7 +248,7 @@ let rec get_c_block_entry_exit_injs_aux bindings A.(AnnotatedStatement (loc, _, [ generate_c_local_ownership_exit (b_sym, b_ctype) ] )) bs in - let exit_injs' = List.map (fun (loc, stats) -> ((loc, [], stats), [])) exit_injs in + let exit_injs' = List.map (fun (loc, stats) -> (loc, [], stats)) exit_injs in let stat_injs = List.map (fun s -> get_c_block_entry_exit_injs_aux bs s) ss in List.concat stat_injs @ exit_injs' | AilSif (_, s1, s2) -> @@ -270,19 +270,19 @@ let rec get_c_block_entry_exit_injs_aux bindings A.(AnnotatedStatement (loc, _, let get_c_block_entry_exit_injs stat = let injs = get_c_block_entry_exit_injs_aux [] stat in - List.map (fun ((loc, bs, ss), syms) -> ((loc, None, bs, ss), syms)) injs + List.map (fun (loc, bs, ss) -> (loc, None, bs, ss)) injs let rec combine_injs_over_location loc = function | [] -> [] - | ((loc', expr_opt, bs, inj_stmt), syms) :: injs' -> + | (loc', expr_opt, bs, inj_stmt) :: injs' -> let stmt = if String.equal (Cerb_location.location_to_string loc) (Cerb_location.location_to_string loc') then - [ ((expr_opt, bs, inj_stmt), syms) ] + [ (expr_opt, bs, inj_stmt) ] else [] in @@ -317,21 +317,18 @@ let get_c_block_local_ownership_checking_injs | A.(AilSblock _) -> let injs = get_c_block_entry_exit_injs statement in let injs' = get_c_control_flow_block_unmaps statement in - let injs' = List.map (fun (l, r, s, b) -> ((l, r, s, b), [])) injs' in let injs = injs @ injs' in - let locs = List.map (fun ((l, _, _, _), _) -> l) injs in + let locs = List.map (fun (l, _, _, _) -> l) injs in let locs = remove_duplicates [] locs in let combined_injs = List.map (fun l -> let injs' = combine_injs_over_location l injs in - let injs', syms = List.split injs' in let expr_opt_list, bs_list, stats_list = Executable_spec_utils.list_split_three injs' in let return_expr_opt = get_return_expr_opt expr_opt_list in - ( (l, return_expr_opt, List.concat bs_list, List.concat stats_list), - List.concat syms )) + (l, return_expr_opt, List.concat bs_list, List.concat stats_list)) locs in combined_injs @@ -356,5 +353,5 @@ let get_c_fn_local_ownership_checking_injs let ownership_stats_pair = get_c_local_ownership_checking params in (* TODO: Separate return injections here since they are now done differently *) let block_ownership_injs = get_c_block_local_ownership_checking_injs fn_body in - (Some (ownership_stats_pair, params), block_ownership_injs) + (Some ownership_stats_pair, block_ownership_injs) | _, _ -> (None, []) From ce5f9905fb99c8907a3e4d8e3c2a402e12d97357 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 3 Jan 2025 12:05:45 +0000 Subject: [PATCH 17/28] Revert "experiments for not repeating bindings across loops" This reverts commit aa438e6cc056c2a292bc066184aa523f36857e23. --- backend/cn/lib/cn_internal_to_ail.ml | 95 ++++++++-------------- backend/cn/lib/cn_internal_to_ail.mli | 7 +- backend/cn/lib/executable_spec_internal.ml | 6 +- backend/cn/lib/executable_spec_utils.ml | 4 +- 4 files changed, 43 insertions(+), 69 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 8af276b52..ab629ebee 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -615,12 +615,13 @@ type ail_executable_spec = post : ail_bindings_and_statements; in_stmt : (Locations.t * ail_bindings_and_statements) list; loops : - (Locations.t * ail_bindings_and_statements) list - * (Locations.t * ail_bindings_and_statements) list + ((Locations.t * ail_bindings_and_statements) + * (Locations.t * ail_bindings_and_statements)) + list } let empty_ail_executable_spec = - { pre = ([], []); post = ([], []); in_stmt = []; loops = ([], []) } + { pre = ([], []); post = ([], []); in_stmt = []; loops = [] } type 'a dest = @@ -3313,32 +3314,26 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu (List.concat bs, List.concat ss) -let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (cond_loc, loop_loc, at) = +let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = match at with | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in - let subst_loop = - ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') - in - let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)), _ = - cn_to_ail_loop_inv_aux dts globals preds (sym :: decl_syms) subst_loop - in - let ret_loop_bs, ret_loop_ss = - if List.mem Sym.equal sym decl_syms then - (loop_bs, loop_ss) - else ( - let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in - let binding = create_binding cn_sym cn_ctype in - let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in - (binding :: loop_bs, decl :: loop_ss)) - in + let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in + let binding = create_binding cn_sym cn_ctype in + (* TODO: Check this should always translate to the address of the given sym in the loop invariant case *) let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in + let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in let assign = A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) in + let subst_loop = + ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') + in + let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)) = + cn_to_ail_loop_inv_aux dts globals preds subst_loop + in ( (cond_loc, (cond_bs, assign :: cond_ss)), - (loop_loc, (ret_loop_bs, ret_loop_ss)), - sym :: decl_syms ) + (loop_loc, (binding :: loop_bs, decl :: loop_ss)) ) | L lat -> let rec modify_decls_for_loop decls modified_stats = let rec collect_initialised_syms_and_exprs = function @@ -3376,12 +3371,12 @@ let rec cn_to_ail_loop_inv_aux dts globals preds decl_syms (cond_loc, loop_loc, in let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in let decls, modified_stats = modify_decls_for_loop [] [] ss in - ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls)), decl_syms) + ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls))) -let cn_to_ail_loop_inv dts globals preds decl_syms ((cond_loc, loop_loc, _) as loop) = - let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss), new_decl_syms = - cn_to_ail_loop_inv_aux dts globals preds decl_syms loop +let cn_to_ail_loop_inv dts globals preds ((cond_loc, loop_loc, _) as loop) = + let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss) = + cn_to_ail_loop_inv_aux dts globals preds loop in let cn_stack_depth_incr_call = A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_incr_sym), []))) @@ -3404,9 +3399,7 @@ let cn_to_ail_loop_inv dts globals preds decl_syms ((cond_loc, loop_loc, _) as l in let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in - ( (cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), - (loop_loc, loop_bs_and_ss), - new_decl_syms ) + ((cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss)) let prepend_to_precondition ail_executable_spec (b1, s1) = @@ -3473,8 +3466,8 @@ let rec cn_to_ail_lat_internal_2 lat in prepend_to_precondition ail_executable_spec (b1, ss) - (* Postcondition, statements and loop invariants *) - | LAT.I (post, (stats, loops)) -> + (* Postcondition *) + | LAT.I (post, (stats, loop)) -> let rec remove_duplicates locs stats = match stats with | [] -> [] @@ -3519,32 +3512,7 @@ let rec cn_to_ail_lat_internal_2 let ail_statements = List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats in - let rec _get_ail_loop_invariants dts globals preds decl_syms = function - | [] -> ([], []) - | l :: ls -> - let cond_ail, loop_decl_ail, new_decl_syms = - cn_to_ail_loop_inv dts globals preds decl_syms l - in - let cond_ails, loop_decl_ails = - _get_ail_loop_invariants dts globals preds new_decl_syms ls - in - (cond_ail :: cond_ails, loop_decl_ail :: loop_decl_ails) - in - (* let ail_loop_invariants = get_ail_loop_invariants dts globals preds [] loops in *) - let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds []) loops in - let cond_stats, loop_decls, _ = - Executable_spec_utils.list_split_three ail_loop_invariants - in - (* let (cond_stats, loop_decls) = List.split ail_loop_invariants in *) - (* let rec shift_loop_decls = function - | [] -> [] - | [(_, (bs, ss))] -> [(Cerb_location.unknown, (bs, ss))] - | (loc, (decl_bs, decl_ss)) :: ds -> - let ds_bs_and_ss = shift_loop_decls ds in - let (ds_bs, ds_ss) = List.split (List.map snd ds_bs_and_ss) in - [loc, (decl_bs @ (List.concat ds_bs), decl_ss @ (List.concat ds_ss))] - in *) - (* let modified_ail_loop_invariants = (cond_stats, (loop_decls)) in *) + let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds) loop in let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in let ownership_stats_ = if without_ownership_checking then @@ -3563,11 +3531,11 @@ let rec cn_to_ail_lat_internal_2 { pre = ([], []); post = ([], [ block ]); in_stmt = ail_statements; - loops = (cond_stats, loop_decls) + loops = ail_loop_invariants } -let rec cn_to_ail_executable_spec_aux +let rec cn_to_ail_pre_post_aux_internal without_ownership_checking dts preds @@ -3582,7 +3550,7 @@ let rec cn_to_ail_executable_spec_aux let decl = A.(AilSdeclaration [ (cn_sym, Some (mk_expr rhs)) ]) in let subst_at = ESE.fn_args_and_body_subst (ESE.sym_subst (sym, bt, cn_sym)) at in let ail_executable_spec = - cn_to_ail_executable_spec_aux + cn_to_ail_pre_post_aux_internal without_ownership_checking dts preds @@ -3601,11 +3569,16 @@ let rec cn_to_ail_executable_spec_aux lat -let cn_to_ail_executable_spec ~without_ownership_checking dts preds globals c_return_type +let cn_to_ail_pre_post_internal + ~without_ownership_checking + dts + preds + globals + c_return_type = function | Some internal -> let ail_executable_spec = - cn_to_ail_executable_spec_aux + cn_to_ail_pre_post_aux_internal without_ownership_checking dts preds diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli index 61afa19b3..a0d1e2aba 100644 --- a/backend/cn/lib/cn_internal_to_ail.mli +++ b/backend/cn/lib/cn_internal_to_ail.mli @@ -56,8 +56,9 @@ type ail_executable_spec = post : ail_bindings_and_statements; in_stmt : (Locations.t * ail_bindings_and_statements) list; loops : - (Locations.t * ail_bindings_and_statements) list - * (Locations.t * ail_bindings_and_statements) list + ((Locations.t * ail_bindings_and_statements) + * (Locations.t * ail_bindings_and_statements)) + list } val generate_get_or_put_ownership_function @@ -169,7 +170,7 @@ val cn_to_ail_predicates_internal list * A.sigma_tag_definition option list -val cn_to_ail_executable_spec +val cn_to_ail_pre_post_internal : without_ownership_checking:bool -> A.sigma_cn_datatype list -> (Sym.t * Definition.Predicate.t) list -> diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index d55156943..dad4ca365 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -70,7 +70,7 @@ let generate_c_pres_and_posts_internal in let globals = extract_global_variables prog5.globs in let ail_executable_spec = - Cn_internal_to_ail.cn_to_ail_executable_spec + Cn_internal_to_ail.cn_to_ail_pre_post_internal ~without_ownership_checking dts preds @@ -145,8 +145,8 @@ let generate_c_pres_and_posts_internal (fun (loc, e_opt, strs) -> (loc, e_opt, [ String.concat "\n" strs ])) return_ownership_stmts in - let ail_cond_stats, ail_loop_decls = ail_executable_spec.loops in - (* let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in *) + let ail_loop_invariants = ail_executable_spec.loops in + let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in (* A bit of a hack *) let rec remove_last = function | [] -> [] diff --git a/backend/cn/lib/executable_spec_utils.ml b/backend/cn/lib/executable_spec_utils.ml index d4774e1c7..a1619638d 100644 --- a/backend/cn/lib/executable_spec_utils.ml +++ b/backend/cn/lib/executable_spec_utils.ml @@ -167,7 +167,7 @@ let get_start_loc ?(offset = 0) = function Cerb_location.point new_start_pos | None -> failwith - (__FUNCTION__ ^ ": Loc_regions has empty list of positions (should be non-empty)")) + "get_start_loc: Loc_regions has empty list of positions (should be non-empty)") | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } | Loc_unknown | Loc_other _ -> failwith "get_start_loc: Location should be Loc_region, Loc_regions or Loc_point" @@ -184,7 +184,7 @@ let get_end_loc ?(offset = 0) = function Cerb_location.point new_end_pos | None -> failwith - (__FUNCTION__ ^ ": Loc_regions has empty list of positions (should be non-empty)")) + "get_end_loc: Loc_regions has empty list of positions (should be non-empty)") | Loc_point pos -> Cerb_location.point { pos with pos_cnum = pos.pos_cnum + offset } | Loc_unknown | Loc_other _ -> failwith "get_end_loc: Location should be Loc_region, Loc_regions or Loc_point" From d9dc8549620956ffd41affd0bf8f50f65d2072c8 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Mon, 6 Jan 2025 15:44:27 +0000 Subject: [PATCH 18/28] Begin second attempt of augmenting each with a binding+decl for --- backend/cn/lib/cn_internal_to_ail.ml | 12 ------------ backend/cn/lib/cn_internal_to_ail.mli | 7 ------- backend/cn/lib/executable_spec_utils.ml | 12 ++++++++++++ backend/cn/lib/ownership_exec.ml | 26 ++++++++++++++++++++++--- 4 files changed, 35 insertions(+), 22 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index ab629ebee..8a715a0d5 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -78,18 +78,6 @@ let create_id_from_sym ?(lowercase = false) sym = let create_sym_from_id id = Sym.fresh_pretty (Id.get_string id) -let generate_sym_with_suffix - ?(suffix = "_tag") - ?(uppercase = false) - ?(lowercase = false) - constructor - = - let str = Sym.pp_string constructor ^ suffix in - let str = if uppercase then String.uppercase_ascii str else str in - let str = if lowercase then String.lowercase_ascii str else str in - Sym.fresh_pretty str - - let generate_error_msg_info_update_stats ?(cn_source_loc_opt = None) () = let cn_source_loc_arg = match cn_source_loc_opt with diff --git a/backend/cn/lib/cn_internal_to_ail.mli b/backend/cn/lib/cn_internal_to_ail.mli index a0d1e2aba..fb5d26802 100644 --- a/backend/cn/lib/cn_internal_to_ail.mli +++ b/backend/cn/lib/cn_internal_to_ail.mli @@ -41,13 +41,6 @@ val wrap_with_convert_from_cn_bool : CF.GenTypes.genTypeCategory A.expression -> CF.GenTypes.genTypeCategory A.expression -val generate_sym_with_suffix - : ?suffix:string -> - ?uppercase:bool -> - ?lowercase:bool -> - Sym.t -> - Sym.t - type ail_bindings_and_statements = A.bindings * CF.GenTypes.genTypeCategory A.statement_ list diff --git a/backend/cn/lib/executable_spec_utils.ml b/backend/cn/lib/executable_spec_utils.ml index a1619638d..a5a5f0dbd 100644 --- a/backend/cn/lib/executable_spec_utils.ml +++ b/backend/cn/lib/executable_spec_utils.ml @@ -55,6 +55,18 @@ let is_empty_ail_stmt = function | _ -> false +let generate_sym_with_suffix + ?(suffix = "_tag") + ?(uppercase = false) + ?(lowercase = false) + constructor + = + let str = Sym.pp_string constructor ^ suffix in + let str = if uppercase then String.uppercase_ascii str else str in + let str = if lowercase then String.lowercase_ascii str else str in + Sym.fresh_pretty str + + let rec list_split_three = function | [] -> ([], [], []) | (x, y, z) :: rest -> diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index 0d464a8ba..e7d3685a6 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -71,12 +71,29 @@ let generate_c_local_ownership_entry_fcall (local_sym, local_ctype) = (mk_expr (AilEident c_add_ownership_fn_sym), List.map mk_expr [ arg1; arg2; arg3 ])) +let generate_c_local_cn_addr_var sym = + (* Hardcoding parts of cn_to_ail_base_type to prevent circular dependency between + this module and Cn_internal_to_ail, which includes Ownership_exec already. *) + let cn_addr_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in + let annots = [ CF.Annot.Atypedef (Sym.fresh_pretty "cn_pointer") ] in + (* Ctype_ doesn't matter to pretty-printer when typedef annotations are present *) + let inner_ctype = mk_ctype ~annots C.Void in + let cn_ptr_ctype = mk_ctype C.(Pointer (empty_qualifiers, inner_ctype)) in + let binding = create_binding cn_addr_sym cn_ptr_ctype in + let addr_of_sym = mk_expr A.(AilEunary (Address, mk_expr (AilEident sym))) in + let fcall_sym = Sym.fresh_pretty "convert_to_cn_pointer" in + let conversion_fcall = A.(AilEcall (mk_expr (AilEident fcall_sym), [ addr_of_sym ])) in + let decl = A.(AilSdeclaration [ (cn_addr_sym, Some (mk_expr conversion_fcall)) ]) in + (binding, decl) + + (* int x = 0, y = 5; -> int x = 0, _dummy = (c_map_local(&x), 0), y = 5, _dummy2 = (c_map_local(&y), 0); *) +(* TODO: Include binding + declaration of _addr_cn via generate_c_local_cn_addr_var function *) let rec gen_loop_ownership_entry_decls bindings = function | [] -> ([], []) | (sym, expr_opt) :: xs -> @@ -99,15 +116,18 @@ let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = let new_bindings, new_decls = gen_loop_ownership_entry_decls bindings decls in [ (loc, new_bindings, [ A.AilSdeclaration new_decls ]) ]) else ( - let stats_ = + let ownership_bs_and_ss = List.map (fun (sym, _) -> let ctype = find_ctype_from_bindings bindings sym in let entry_fcall = generate_c_local_ownership_entry_fcall (sym, ctype) in - A.(AilSexpr entry_fcall)) + let entry_fcall_stat = A.(AilSexpr entry_fcall) in + let addr_cn_binding, addr_cn_decl = generate_c_local_cn_addr_var sym in + ([ addr_cn_binding ], [ entry_fcall_stat; addr_cn_decl ])) decls in - [ (get_end_loc loc, [], stats_) ]) + let bs, ss = List.split ownership_bs_and_ss in + [ (get_end_loc loc, List.concat bs, List.concat ss) ]) (* c_remove_local_footprint((uintptr_t) &xs, cn_ownership_global_ghost_state, From f52fa3f71cf6febc50e52549b61528238d0fb44e Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Mon, 6 Jan 2025 15:46:31 +0000 Subject: [PATCH 19/28] Begin second attempt of augmenting each c_map_local(sym) with a binding+decl for sym_addr_cn Previous commit message with backticks didn't work --- backend/cn/lib/ownership_exec.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index e7d3685a6..c468616e4 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -110,6 +110,7 @@ let rec gen_loop_ownership_entry_decls bindings = function let bindings', decls' = gen_loop_ownership_entry_decls bindings xs in (new_bindings @ bindings', (sym, expr_opt) :: (dummy_sym, Some dummy_rhs) :: decls') + let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = if dest_is_loop then ( From df4562fc7fdd042d54b1070ed8e4b0915ce80f70 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Mon, 13 Jan 2025 23:56:07 +0000 Subject: [PATCH 20/28] some more progress --- backend/cn/lib/cn_internal_to_ail.ml | 8 ++++---- backend/cn/lib/ownership_exec.ml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 8a715a0d5..ab7281008 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3306,22 +3306,22 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = match at with | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in - let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in + (* let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in let binding = create_binding cn_sym cn_ctype in (* TODO: Check this should always translate to the address of the given sym in the loop invariant case *) let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in let assign = A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) - in + in *) let subst_loop = ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') in let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)) = cn_to_ail_loop_inv_aux dts globals preds subst_loop in - ( (cond_loc, (cond_bs, assign :: cond_ss)), - (loop_loc, (binding :: loop_bs, decl :: loop_ss)) ) + ( (cond_loc, (cond_bs, (* assign :: *) cond_ss)), + (loop_loc, ((* binding :: *) loop_bs, (* decl :: *) loop_ss)) ) | L lat -> let rec modify_decls_for_loop decls modified_stats = let rec collect_initialised_syms_and_exprs = function diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index c468616e4..1b9502bdc 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -110,7 +110,7 @@ let rec gen_loop_ownership_entry_decls bindings = function let bindings', decls' = gen_loop_ownership_entry_decls bindings xs in (new_bindings @ bindings', (sym, expr_opt) :: (dummy_sym, Some dummy_rhs) :: decls') - + let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = if dest_is_loop then ( From 9e617e7f5583c00b245565ce7668d138c4019561 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Wed, 19 Feb 2025 11:43:52 +0000 Subject: [PATCH 21/28] Finish task of creating + initialising addr_cn variables for all stack-local variables --- backend/cn/lib/cn_internal_to_ail.ml | 14 +++++------ backend/cn/lib/executable_spec_internal.ml | 10 ++++---- backend/cn/lib/ownership_exec.ml | 27 ++++++++++++---------- 3 files changed, 27 insertions(+), 24 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index ab7281008..313483a4e 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3307,13 +3307,13 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in (* let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in - let binding = create_binding cn_sym cn_ctype in - (* TODO: Check this should always translate to the address of the given sym in the loop invariant case *) - let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in - let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in - let assign = - A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) - in *) + let binding = create_binding cn_sym cn_ctype in + (* TODO: Check this should always translate to the address of the given sym in the loop invariant case *) + let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in + let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in + let assign = + A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) + in *) let subst_loop = ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') in diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index dad4ca365..6715a3f2f 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -85,13 +85,13 @@ let generate_c_pres_and_posts_internal if without_ownership_checking then ((pre_str, post_str), []) else ( - let fn_ownership_stats_opt, block_ownership_injs = + let fn_ownership_bs_and_ss_opt, block_ownership_injs = Ownership_exec.get_c_fn_local_ownership_checking_injs instrumentation.fn sigm in - match fn_ownership_stats_opt with - | Some (entry_ownership_stats, exit_ownership_stats) -> - let entry_ownership_str = generate_ail_stat_strs ([], entry_ownership_stats) in - let exit_ownership_str = generate_ail_stat_strs ([], exit_ownership_stats) in + match fn_ownership_bs_and_ss_opt with + | Some (entry_ownership_bs_and_ss, exit_ownership_bs_and_ss) -> + let entry_ownership_str = generate_ail_stat_strs entry_ownership_bs_and_ss in + let exit_ownership_str = generate_ail_stat_strs exit_ownership_bs_and_ss in let pre_post_pair = ( pre_str @ ("\n\t/* C OWNERSHIP */\n\n" :: entry_ownership_str), (* NOTE - the nesting pre - entry - exit - post *) diff --git a/backend/cn/lib/ownership_exec.ml b/backend/cn/lib/ownership_exec.ml index 1b9502bdc..722d17415 100644 --- a/backend/cn/lib/ownership_exec.ml +++ b/backend/cn/lib/ownership_exec.ml @@ -87,6 +87,13 @@ let generate_c_local_cn_addr_var sym = (binding, decl) +let generate_c_local_ownership_entry_bs_and_ss (sym, ctype) = + let entry_fcall = generate_c_local_ownership_entry_fcall (sym, ctype) in + let entry_fcall_stat = A.(AilSexpr entry_fcall) in + let addr_cn_binding, addr_cn_decl = generate_c_local_cn_addr_var sym in + ([ addr_cn_binding ], [ entry_fcall_stat; addr_cn_decl ]) + + (* int x = 0, y = 5; -> @@ -111,7 +118,6 @@ let rec gen_loop_ownership_entry_decls bindings = function (new_bindings @ bindings', (sym, expr_opt) :: (dummy_sym, Some dummy_rhs) :: decls') - let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = if dest_is_loop then ( let new_bindings, new_decls = gen_loop_ownership_entry_decls bindings decls in @@ -121,10 +127,7 @@ let generate_c_local_ownership_entry_inj dest_is_loop loc decls bindings = List.map (fun (sym, _) -> let ctype = find_ctype_from_bindings bindings sym in - let entry_fcall = generate_c_local_ownership_entry_fcall (sym, ctype) in - let entry_fcall_stat = A.(AilSexpr entry_fcall) in - let addr_cn_binding, addr_cn_decl = generate_c_local_cn_addr_var sym in - ([ addr_cn_binding ], [ entry_fcall_stat; addr_cn_decl ])) + generate_c_local_ownership_entry_bs_and_ss (sym, ctype)) decls in let bs, ss = List.split ownership_bs_and_ss in @@ -150,13 +153,13 @@ let generate_c_local_ownership_exit (local_sym, local_ctype) = let get_c_local_ownership_checking params = - let entry_ownership_stats = - List.map - (fun param -> A.(AilSexpr (generate_c_local_ownership_entry_fcall param))) - params + let entry_ownership_bs_and_ss = + List.map (fun param -> generate_c_local_ownership_entry_bs_and_ss param) params in + let entry_ownership_bs, entry_ownership_ss = List.split entry_ownership_bs_and_ss in let exit_ownership_stats = List.map generate_c_local_ownership_exit params in - (entry_ownership_stats, exit_ownership_stats) + ( (List.concat entry_ownership_bs, List.concat entry_ownership_ss), + ([], exit_ownership_stats) ) let rec collect_visibles bindings = function @@ -371,8 +374,8 @@ let get_c_fn_local_ownership_checking_injs Some (_, _, Decl_function (_, _, param_types, _, _, _)) ) -> let param_types = List.map (fun (_, ctype, _) -> ctype) param_types in let params = List.combine param_syms param_types in - let ownership_stats_pair = get_c_local_ownership_checking params in + let ownership_bs_and_ss_pair = get_c_local_ownership_checking params in (* TODO: Separate return injections here since they are now done differently *) let block_ownership_injs = get_c_block_local_ownership_checking_injs fn_body in - (Some ownership_stats_pair, block_ownership_injs) + (Some ownership_bs_and_ss_pair, block_ownership_injs) | _, _ -> (None, []) From 429a2c2eb01e9744f9a9ffda6dbe856632bf9f32 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 21 Feb 2025 13:56:40 +0000 Subject: [PATCH 22/28] Enclose runtime loop invariant code in block --- backend/cn/lib/executable_spec_internal.ml | 26 +++++++++++----------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index 6715a3f2f..9041cba61 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -19,7 +19,6 @@ type executable_spec = } let generate_ail_stat_strs - ?(with_newline = false) (bs, (ail_stats_ : CF.GenTypes.genTypeCategory A.statement_ list)) = let is_assert_true = function @@ -35,13 +34,7 @@ let generate_ail_stat_strs (fun s -> CF.Pp_ail.pp_statement ~executable_spec:true ~bs (mk_stmt s)) ail_stats_ in - let doc = - List.map - (fun d -> - let newline = if with_newline then PPrint.hardline else PPrint.empty in - newline ^^ d ^^ PPrint.hardline) - doc - in + let doc = List.map (fun d -> d ^^ PPrint.hardline) doc in List.map CF.Pp_utils.to_plain_pretty_string doc @@ -128,7 +121,7 @@ let generate_c_pres_and_posts_internal in let block_ownership_stmts = List.map - (fun (loc, _, bs, ss) -> (loc, generate_ail_stat_strs ~with_newline:true (bs, ss))) + (fun (loc, _, bs, ss) -> (loc, generate_ail_stat_strs (bs, ss))) non_return_injs in let block_ownership_stmts = @@ -136,8 +129,7 @@ let generate_c_pres_and_posts_internal in let return_ownership_stmts = List.map - (fun (loc, e_opt, bs, ss) -> - (loc, e_opt, generate_ail_stat_strs ~with_newline:true (bs, ss))) + (fun (loc, e_opt, bs, ss) -> (loc, e_opt, generate_ail_stat_strs (bs, ss))) return_injs in let return_ownership_stmts = @@ -171,11 +163,19 @@ let generate_c_pres_and_posts_internal in let ail_loop_decl_injs = List.map - (fun (loc, bs_and_ss) -> (get_start_loc loc, generate_ail_stat_strs bs_and_ss)) + (fun (loc, bs_and_ss) -> + (get_start_loc loc, "{" :: generate_ail_stat_strs bs_and_ss)) ail_loop_decls in + let ail_loop_close_block_injs = + List.map (fun (loc, _) -> (get_end_loc loc, [ "}" ])) ail_loop_decls + in ( [ (instrumentation.fn, (pre_str, post_str)) ], - in_stmt @ block_ownership_stmts @ ail_cond_injs @ ail_loop_decl_injs, + in_stmt + @ block_ownership_stmts + @ ail_cond_injs + @ ail_loop_decl_injs + @ ail_loop_close_block_injs, return_ownership_stmts ) From f4fb977f701526e8d667e6091d74bd542fc461e2 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 21 Feb 2025 15:12:12 +0000 Subject: [PATCH 23/28] Add flag for disabling checking loop invariants at runtime --- backend/cn/bin/main.ml | 14 +++ backend/cn/lib/executable_spec.ml | 4 +- backend/cn/lib/executable_spec_internal.ml | 99 ++++++++++++---------- 3 files changed, 73 insertions(+), 44 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index af680ca62..fb7b740d8 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -405,6 +405,7 @@ let generate_executable_specs output_decorated output_decorated_dir without_ownership_checking + without_loop_invariants with_test_gen copy_source_dir = @@ -444,6 +445,7 @@ let generate_executable_specs (try Executable_spec.main ~without_ownership_checking + ~without_loop_invariants ~with_test_gen ~copy_source_dir filename @@ -473,6 +475,7 @@ let run_seq_tests magic_comment_char_dollar (* Executable spec *) without_ownership_checking + without_loop_invariants (* Test Generation *) output_dir with_static_hack @@ -525,6 +528,7 @@ let run_seq_tests Cn_internal_to_ail.augment_record_map (BaseTypes.Record []); Executable_spec.main ~without_ownership_checking + ~without_loop_invariants ~with_test_gen:true ~copy_source_dir:false filename @@ -562,6 +566,7 @@ let run_tests magic_comment_char_dollar (* Executable spec *) without_ownership_checking + without_loop_invariants (* Test Generation *) output_dir only @@ -663,6 +668,7 @@ let run_tests (try Executable_spec.main ~without_ownership_checking + ~without_loop_invariants ~with_test_gen:true ~copy_source_dir:false filename @@ -921,6 +927,11 @@ module Executable_spec_flags = struct Arg.(value & flag & info [ "without-ownership-checking" ] ~doc) + let without_loop_invariants = + let doc = "Disable checking of loop invariants within CN runtime testing" in + Arg.(value & flag & info [ "without-loop-invariants" ] ~doc) + + let with_test_gen = let doc = "Generate CN executable specifications in the correct format for feeding into \n\ @@ -1324,6 +1335,7 @@ let testing_cmd = $ Common_flags.no_inherit_loc $ Common_flags.magic_comment_char_dollar $ Executable_spec_flags.without_ownership_checking + $ Executable_spec_flags.without_loop_invariants $ Testing_flags.output_test_dir $ Testing_flags.only $ Testing_flags.skip @@ -1381,6 +1393,7 @@ let seq_test_cmd = $ Common_flags.no_inherit_loc $ Common_flags.magic_comment_char_dollar $ Executable_spec_flags.without_ownership_checking + $ Executable_spec_flags.without_loop_invariants $ Seq_testing_flags.output_test_dir $ Seq_testing_flags.with_static_hack $ Seq_testing_flags.gen_num_samples @@ -1426,6 +1439,7 @@ let instrument_cmd = $ Executable_spec_flags.output_decorated $ Executable_spec_flags.output_decorated_dir $ Executable_spec_flags.without_ownership_checking + $ Executable_spec_flags.without_loop_invariants $ Executable_spec_flags.with_test_gen $ Executable_spec_flags.copy_source_dir in diff --git a/backend/cn/lib/executable_spec.ml b/backend/cn/lib/executable_spec.ml index 9a0a7b37e..ce093a798 100644 --- a/backend/cn/lib/executable_spec.ml +++ b/backend/cn/lib/executable_spec.ml @@ -195,6 +195,7 @@ open Executable_spec_internal let main ?(without_ownership_checking = false) + ?(without_loop_invariants = false) ?(with_test_gen = false) ?(copy_source_dir = false) filename @@ -218,8 +219,9 @@ let main in Executable_spec_records.populate_record_map instrumentation prog5; let executable_spec = - generate_c_specs_internal + generate_c_specs without_ownership_checking + without_loop_invariants instrumentation symbol_table statement_locs diff --git a/backend/cn/lib/executable_spec_internal.ml b/backend/cn/lib/executable_spec_internal.ml index 9041cba61..b514eaac4 100644 --- a/backend/cn/lib/executable_spec_internal.ml +++ b/backend/cn/lib/executable_spec_internal.ml @@ -19,6 +19,7 @@ type executable_spec = } let generate_ail_stat_strs + ?(with_newline = false) (bs, (ail_stats_ : CF.GenTypes.genTypeCategory A.statement_ list)) = let is_assert_true = function @@ -34,7 +35,13 @@ let generate_ail_stat_strs (fun s -> CF.Pp_ail.pp_statement ~executable_spec:true ~bs (mk_stmt s)) ail_stats_ in - let doc = List.map (fun d -> d ^^ PPrint.hardline) doc in + let doc = + List.map + (fun d -> + let newline = if with_newline then PPrint.hardline else PPrint.empty in + newline ^^ d ^^ PPrint.hardline) + doc + in List.map CF.Pp_utils.to_plain_pretty_string doc @@ -47,8 +54,9 @@ let rec extract_global_variables = function | GlobalDecl ctype -> (sym, Sctypes.to_ctype ctype) :: extract_global_variables ds) -let generate_c_pres_and_posts_internal +let generate_c_specs_internal without_ownership_checking + without_loop_invariants (instrumentation : Executable_spec_extract.instrumentation) _ (sigm : _ CF.AilSyntax.sigma) @@ -121,7 +129,7 @@ let generate_c_pres_and_posts_internal in let block_ownership_stmts = List.map - (fun (loc, _, bs, ss) -> (loc, generate_ail_stat_strs (bs, ss))) + (fun (loc, _, bs, ss) -> (loc, generate_ail_stat_strs ~with_newline:true (bs, ss))) non_return_injs in let block_ownership_stmts = @@ -129,7 +137,8 @@ let generate_c_pres_and_posts_internal in let return_ownership_stmts = List.map - (fun (loc, e_opt, bs, ss) -> (loc, e_opt, generate_ail_stat_strs (bs, ss))) + (fun (loc, e_opt, bs, ss) -> + (loc, e_opt, generate_ail_stat_strs ~with_newline:true (bs, ss))) return_injs in let return_ownership_stmts = @@ -137,45 +146,47 @@ let generate_c_pres_and_posts_internal (fun (loc, e_opt, strs) -> (loc, e_opt, [ String.concat "\n" strs ])) return_ownership_stmts in - let ail_loop_invariants = ail_executable_spec.loops in - let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in - (* A bit of a hack *) - let rec remove_last = function - | [] -> [] - | [ _ ] -> [] - | x :: xs -> x :: remove_last xs - in - let rec remove_last_semicolon = function - | [] -> [] - | [ x ] -> - let split_x = String.split_on_char ';' x in - let without_whitespace_x = remove_last split_x in - let res = String.concat ";" without_whitespace_x in - [ res ] - | x :: xs -> x :: remove_last_semicolon xs - in - let ail_cond_injs = - List.map - (fun (loc, bs_and_ss) -> - ( get_start_loc loc, - remove_last_semicolon (generate_ail_stat_strs bs_and_ss) @ [ ", " ] )) - ail_cond_stats - in - let ail_loop_decl_injs = - List.map - (fun (loc, bs_and_ss) -> - (get_start_loc loc, "{" :: generate_ail_stat_strs bs_and_ss)) - ail_loop_decls - in - let ail_loop_close_block_injs = - List.map (fun (loc, _) -> (get_end_loc loc, [ "}" ])) ail_loop_decls + let loop_invariant_injs = + if without_loop_invariants then + [] + else ( + let ail_loop_invariants = ail_executable_spec.loops in + let ail_cond_stats, ail_loop_decls = List.split ail_loop_invariants in + (* A bit of a hack *) + let rec remove_last = function + | [] -> [] + | [ _ ] -> [] + | x :: xs -> x :: remove_last xs + in + let rec remove_last_semicolon = function + | [] -> [] + | [ x ] -> + let split_x = String.split_on_char ';' x in + let without_whitespace_x = remove_last split_x in + let res = String.concat ";" without_whitespace_x in + [ res ] + | x :: xs -> x :: remove_last_semicolon xs + in + let ail_cond_injs = + List.map + (fun (loc, bs_and_ss) -> + ( get_start_loc loc, + remove_last_semicolon (generate_ail_stat_strs bs_and_ss) @ [ ", " ] )) + ail_cond_stats + in + let ail_loop_decl_injs = + List.map + (fun (loc, bs_and_ss) -> + (get_start_loc loc, "{" :: generate_ail_stat_strs bs_and_ss)) + ail_loop_decls + in + let ail_loop_close_block_injs = + List.map (fun (loc, _) -> (get_end_loc loc, [ "}" ])) ail_loop_decls + in + ail_cond_injs @ ail_loop_decl_injs @ ail_loop_close_block_injs) in ( [ (instrumentation.fn, (pre_str, post_str)) ], - in_stmt - @ block_ownership_stmts - @ ail_cond_injs - @ ail_loop_decl_injs - @ ail_loop_close_block_injs, + in_stmt @ block_ownership_stmts @ loop_invariant_injs, return_ownership_stmts ) @@ -211,8 +222,9 @@ let generate_c_assume_pres_internal (* Executable_spec_extract.instrumentation list -> executable_spec *) -let generate_c_specs_internal +let generate_c_specs without_ownership_checking + without_loop_invariants instrumentation_list type_map (_ : Cerb_location.t CStatements.LocMap.t) @@ -220,8 +232,9 @@ let generate_c_specs_internal (prog5 : unit Mucore.file) = let generate_c_spec (instrumentation : Executable_spec_extract.instrumentation) = - generate_c_pres_and_posts_internal + generate_c_specs_internal without_ownership_checking + without_loop_invariants instrumentation type_map sigm From 485c3e7e0a2df7b4969a463549ddf3f5a910e93b Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 21 Feb 2025 15:22:33 +0000 Subject: [PATCH 24/28] delete some commented code --- backend/cn/lib/cn_internal_to_ail.ml | 11 ----------- backend/cn/lib/executable_spec_records.ml | 2 +- 2 files changed, 1 insertion(+), 12 deletions(-) diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 313483a4e..61f3b5bfc 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3306,14 +3306,6 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = match at with | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in - (* let cn_ctype = bt_to_ail_ctype (BT.Loc ()) in - let binding = create_binding cn_sym cn_ctype in - (* TODO: Check this should always translate to the address of the given sym in the loop invariant case *) - let rhs = wrap_with_convert_to A.(AilEunary (Address, mk_expr (AilEident sym))) bt in - let decl = A.(AilSdeclaration [ (cn_sym, None) ]) in - let assign = - A.(AilSexpr (mk_expr (AilEassign (mk_expr (AilEident cn_sym), mk_expr rhs)))) - in *) let subst_loop = ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') in @@ -3352,9 +3344,6 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = (decls @ [ none_decl ]) (modified_stats @ assign_stats) ss - (* | A.(AilSblock (bs, block_ss)) -> - let decls', modified_stats' = modify_decls_for_loop decls [] (List.map rm_stmt block_ss) in - modify_decls_for_loop (decls' @ decls) (modified_stats @ [A.(AilSblock (bs, (List.map mk_stmt modified_stats')))]) ss *) | _ -> modify_decls_for_loop decls (modified_stats @ [ s ]) ss) in let bs, ss = cn_to_ail_lat_internal_loop dts globals preds lat in diff --git a/backend/cn/lib/executable_spec_records.ml b/backend/cn/lib/executable_spec_records.ml index 574ab3e20..e044f59e6 100644 --- a/backend/cn/lib/executable_spec_records.ml +++ b/backend/cn/lib/executable_spec_records.ml @@ -122,7 +122,7 @@ let add_records_to_map_from_instrumentation (i : Executable_spec_extract.instrum aux_rt rt; List.iter add_records_to_map_from_cnprogs stmts; List.iter - (fun (_loc1, _loc2, loop_at) -> + (fun (_, _, loop_at) -> let loop_stmts = aux_at loop_at in List.iter add_records_to_map_from_cnprogs loop_stmts) loops From abef8954928710dd31aaf6e7d1a3bda7c70b63ed Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Fri, 21 Feb 2025 15:39:43 +0000 Subject: [PATCH 25/28] Disable loop invariant translation in CN test gen --- backend/cn/bin/main.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index fb7b740d8..3e1201c84 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -475,7 +475,7 @@ let run_seq_tests magic_comment_char_dollar (* Executable spec *) without_ownership_checking - without_loop_invariants + (* without_loop_invariants *) (* Test Generation *) output_dir with_static_hack @@ -527,8 +527,8 @@ let run_seq_tests let _, sigma = ail_prog in Cn_internal_to_ail.augment_record_map (BaseTypes.Record []); Executable_spec.main - ~without_ownership_checking - ~without_loop_invariants + ~without_ownership_checking (* TODO: Zain *) + ~without_loop_invariants:true ~with_test_gen:true ~copy_source_dir:false filename @@ -566,7 +566,7 @@ let run_tests magic_comment_char_dollar (* Executable spec *) without_ownership_checking - without_loop_invariants + (* without_loop_invariants *) (* Test Generation *) output_dir only @@ -667,8 +667,8 @@ let run_tests Cn_internal_to_ail.augment_record_map (BaseTypes.Record []); (try Executable_spec.main - ~without_ownership_checking - ~without_loop_invariants + ~without_ownership_checking (* TODO: Zain *) + ~without_loop_invariants:true ~with_test_gen:true ~copy_source_dir:false filename @@ -1335,7 +1335,6 @@ let testing_cmd = $ Common_flags.no_inherit_loc $ Common_flags.magic_comment_char_dollar $ Executable_spec_flags.without_ownership_checking - $ Executable_spec_flags.without_loop_invariants $ Testing_flags.output_test_dir $ Testing_flags.only $ Testing_flags.skip @@ -1393,7 +1392,6 @@ let seq_test_cmd = $ Common_flags.no_inherit_loc $ Common_flags.magic_comment_char_dollar $ Executable_spec_flags.without_ownership_checking - $ Executable_spec_flags.without_loop_invariants $ Seq_testing_flags.output_test_dir $ Seq_testing_flags.with_static_hack $ Seq_testing_flags.gen_num_samples From 02c7f24e8d46efdc80c86301eea27e2c45401f10 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Tue, 25 Feb 2025 17:07:12 +0000 Subject: [PATCH 26/28] Add bool member to Mu.Label for keeping track of whether user has provided any loop invariant --- backend/cn/lib/check.ml | 4 +- backend/cn/lib/cn_internal_to_ail.ml | 76 +++++++++++++--------- backend/cn/lib/consistent.ml | 8 ++- backend/cn/lib/core_to_mucore.ml | 8 ++- backend/cn/lib/executable_spec_extract.ml | 16 +++-- backend/cn/lib/executable_spec_extract.mli | 2 +- backend/cn/lib/executable_spec_records.ml | 2 +- backend/cn/lib/mucore.ml | 3 + backend/cn/lib/mucore.mli | 3 + backend/cn/lib/pp_mucore.ml | 3 +- backend/cn/lib/pp_mucore_ast.ml | 2 +- backend/cn/lib/pp_mucore_coq.ml | 2 +- backend/cn/lib/wellTyped.ml | 25 ++++++- 13 files changed, 106 insertions(+), 48 deletions(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 31513d189..d023d9799 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -2208,7 +2208,9 @@ let check_procedure pure (match def with | Mu.Return _loc -> return () - | Label (loc, label_args_and_body, _annots, _, _loop_info) -> + | Label + (loc, label_args_and_body, _annots, _, _loop_info, _contains_user_spec) + -> debug 2 (lazy diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 61f3b5bfc..927711388 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3302,19 +3302,26 @@ let rec cn_to_ail_lat_internal_loop ?(is_toplevel = true) dts globals preds = fu (List.concat bs, List.concat ss) -let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = +let rec cn_to_ail_loop_inv_aux + dts + globals + preds + (contains_user_spec, cond_loc, loop_loc, at) + = match at with | AT.Computational ((sym, bt), _, at') -> let cn_sym = generate_sym_with_suffix ~suffix:"_addr_cn" sym in let subst_loop = - ESE.loop_subst (ESE.sym_subst (sym, bt, cn_sym)) (cond_loc, loop_loc, at') + ESE.loop_subst + (ESE.sym_subst (sym, bt, cn_sym)) + (contains_user_spec, cond_loc, loop_loc, at') in let (_, (cond_bs, cond_ss)), (_, (loop_bs, loop_ss)) = cn_to_ail_loop_inv_aux dts globals preds subst_loop in - ( (cond_loc, (cond_bs, (* assign :: *) cond_ss)), - (loop_loc, ((* binding :: *) loop_bs, (* decl :: *) loop_ss)) ) + ((cond_loc, (cond_bs, cond_ss)), (loop_loc, (loop_bs, loop_ss))) | L lat -> + Printf.printf "Reached AT.L\n"; let rec modify_decls_for_loop decls modified_stats = let rec collect_initialised_syms_and_exprs = function | [] -> [] @@ -3351,32 +3358,40 @@ let rec cn_to_ail_loop_inv_aux dts globals preds (cond_loc, loop_loc, at) = ((cond_loc, (bs, modified_stats)), (loop_loc, (bs, decls))) -let cn_to_ail_loop_inv dts globals preds ((cond_loc, loop_loc, _) as loop) = - let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss) = - cn_to_ail_loop_inv_aux dts globals preds loop - in - let cn_stack_depth_incr_call = - A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_incr_sym), []))) - in - let cn_loop_leak_check_and_decr_call = - A.AilSexpr - (mk_expr (AilEcall (mk_expr (AilEident OE.cn_loop_leak_check_and_decr_sym), []))) - in - let cn_stack_depth_decr_call = - A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_decr_sym), []))) - in - let dummy_expr_as_stat = - A.( - AilSexpr - (mk_expr (AilEconst (ConstantInteger (IConstant (Z.of_int 0, Decimal, None)))))) - in - let stats = - (cn_stack_depth_incr_call :: cond_ss) - @ [ cn_loop_leak_check_and_decr_call; cn_stack_depth_decr_call; dummy_expr_as_stat ] - in - let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in - let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in - ((cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss)) +let cn_to_ail_loop_inv + dts + globals + preds + ((contains_user_spec, cond_loc, loop_loc, _) as loop) + = + if contains_user_spec then ( + let (_, (cond_bs, cond_ss)), (_, loop_bs_and_ss) = + cn_to_ail_loop_inv_aux dts globals preds loop + in + let cn_stack_depth_incr_call = + A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_incr_sym), []))) + in + let cn_loop_leak_check_and_decr_call = + A.AilSexpr + (mk_expr (AilEcall (mk_expr (AilEident OE.cn_loop_leak_check_and_decr_sym), []))) + in + let cn_stack_depth_decr_call = + A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_decr_sym), []))) + in + let dummy_expr_as_stat = + A.( + AilSexpr + (mk_expr (AilEconst (ConstantInteger (IConstant (Z.of_int 0, Decimal, None)))))) + in + let stats = + (cn_stack_depth_incr_call :: cond_ss) + @ [ cn_loop_leak_check_and_decr_call; cn_stack_depth_decr_call; dummy_expr_as_stat ] + in + let ail_gcc_stat_as_expr = A.(AilEgcc_statement ([], List.map mk_stmt stats)) in + let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in + Some ((cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss))) + else + None let prepend_to_precondition ail_executable_spec (b1, s1) = @@ -3490,6 +3505,7 @@ let rec cn_to_ail_lat_internal_2 List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats in let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds) loop in + let ail_loop_invariants = List.filter_map Fun.id ail_loop_invariants in let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in let ownership_stats_ = if without_ownership_checking then diff --git a/backend/cn/lib/consistent.ml b/backend/cn/lib/consistent.ml index 78eb932f3..69192d264 100644 --- a/backend/cn/lib/consistent.ml +++ b/backend/cn/lib/consistent.ml @@ -185,7 +185,13 @@ let procedure : Loc.t -> _ Mucore.args_and_body -> unit Typing.t = (fun _sym def -> match def with | Mucore.Return _ -> return () - | Label (loc, label_args_and_body, _annots, _parsed_spec, _loop_info) -> + | Label + ( loc, + label_args_and_body, + _annots, + _parsed_spec, + _loop_info, + _contains_user_spec ) -> pure_and_no_initial_resources loc (arguments diff --git a/backend/cn/lib/core_to_mucore.ml b/backend/cn/lib/core_to_mucore.ml index 78d2b0cb5..9750ee582 100644 --- a/backend/cn/lib/core_to_mucore.ml +++ b/backend/cn/lib/core_to_mucore.ml @@ -1142,10 +1142,11 @@ let normalise_label | Mi_Label (loc, lt, label_args, label_body, annots) -> (match CF.Annot.get_label_annot annots with | Some (LAloop loop_id) -> - let@ desugared_inv, cn_desugaring_state, loop_condition_loc = + let@ desugared_inv, cn_desugaring_state, loop_condition_loc, contains_user_spec = match Pmap.lookup loop_id loop_attributes with | Some { marker_id; attributes = attrs; loc_condition; loc_loop } -> let@ inv = Parse.loop_spec attrs in + let contains_user_spec = List.non_empty inv in let d_st = CAE. { markers_env; @@ -1156,7 +1157,7 @@ let normalise_label } in let@ inv, d_st = desugar_conds d_st inv in - return (inv, d_st.inner.cn_state, (loc_condition, loc_loop)) + return (inv, d_st.inner.cn_state, (loc_condition, loc_loop), contains_user_spec) | None -> assert false (* return ([], precondition_cn_desugaring_state) *) in @@ -1188,7 +1189,8 @@ let normalise_label label_args_and_body, annots, { label_spec = desugared_inv }, - `Loop loop_condition_loc )) + `Loop loop_condition_loc, + contains_user_spec )) (* | Some (LAloop_body _loop_id) -> *) (* assert_error loc !^"body label has not been inlined" *) | Some (LAloop_continue _loop_id) -> diff --git a/backend/cn/lib/executable_spec_extract.ml b/backend/cn/lib/executable_spec_extract.ml index 4c878ddc6..b920db846 100644 --- a/backend/cn/lib/executable_spec_extract.ml +++ b/backend/cn/lib/executable_spec_extract.ml @@ -10,10 +10,10 @@ type statements = statement list let statements_subst subst = List.map (statement_subst subst) -type loop = Locations.t * Locations.t * statements ArgumentTypes.t +type loop = bool * Locations.t * Locations.t * statements ArgumentTypes.t -let loop_subst subst ((cond_loc, loop_loc, at) : loop) = - (cond_loc, loop_loc, ArgumentTypes.subst statements_subst subst at) +let loop_subst subst ((contains_user_spec, cond_loc, loop_loc, at) : loop) = + (contains_user_spec, cond_loc, loop_loc, ArgumentTypes.subst statements_subst subst at) type loops = loop list @@ -106,10 +106,16 @@ let rec stmts_in_expr (Mucore.Expr (loc, _, _, e_)) = let from_loop ((_label_sym : Sym.t), (label_def : _ label_def)) : loop option = match label_def with | Return _ -> None - | Label (_loc, label_args_and_body, _annots, _, `Loop (loop_condition_loc, loop_loc)) -> + | Label + ( _loc, + label_args_and_body, + _annots, + _, + `Loop (loop_condition_loc, loop_loc), + contains_user_spec ) -> let label_args_and_body = Core_to_mucore.at_of_arguments Fun.id label_args_and_body in let label_args_and_statements = ArgumentTypes.map stmts_in_expr label_args_and_body in - Some (loop_condition_loc, loop_loc, label_args_and_statements) + Some (contains_user_spec, loop_condition_loc, loop_loc, label_args_and_statements) let from_fn (fn, decl) = diff --git a/backend/cn/lib/executable_spec_extract.mli b/backend/cn/lib/executable_spec_extract.mli index cc039f3b3..7baa73661 100644 --- a/backend/cn/lib/executable_spec_extract.mli +++ b/backend/cn/lib/executable_spec_extract.mli @@ -2,7 +2,7 @@ type statement = Locations.t * Cnprog.t list type statements = statement list -type loop = Locations.t * Locations.t * statements ArgumentTypes.t +type loop = bool * Locations.t * Locations.t * statements ArgumentTypes.t (* first location is for the loop condition; second is for the entire loop *) type loops = loop list diff --git a/backend/cn/lib/executable_spec_records.ml b/backend/cn/lib/executable_spec_records.ml index e044f59e6..1a4c4e1ef 100644 --- a/backend/cn/lib/executable_spec_records.ml +++ b/backend/cn/lib/executable_spec_records.ml @@ -122,7 +122,7 @@ let add_records_to_map_from_instrumentation (i : Executable_spec_extract.instrum aux_rt rt; List.iter add_records_to_map_from_cnprogs stmts; List.iter - (fun (_, _, loop_at) -> + (fun (_, _, _, loop_at) -> let loop_stmts = aux_at loop_at in List.iter add_records_to_map_from_cnprogs loop_stmts) loops diff --git a/backend/cn/lib/mucore.ml b/backend/cn/lib/mucore.ml index e5d915fa2..313cddaaf 100644 --- a/backend/cn/lib/mucore.ml +++ b/backend/cn/lib/mucore.ml @@ -380,6 +380,9 @@ type 'TY label_def = * Cerb_frontend.Annot.annot list * parse_ast_label_spec * [ `Loop of Locations.t * Locations.t ] + * bool +(* whether any loop invariant was provided by the user, for executable checking *) + (*first loc is condition, second is whole loop*) (*loop condition location, for executable checking *) diff --git a/backend/cn/lib/mucore.mli b/backend/cn/lib/mucore.mli index 3d69d39c6..99bb88ca0 100644 --- a/backend/cn/lib/mucore.mli +++ b/backend/cn/lib/mucore.mli @@ -283,6 +283,9 @@ type 'TY label_def = * Cerb_frontend.Annot.annot list * parse_ast_label_spec * [ `Loop of Locations.t * Locations.t ] + * bool +(* whether any loop invariant was provided by the user, for executable checking *) + (*first loc is condition, second is whole loop*) (*loop condition location, for executable checking *) diff --git a/backend/cn/lib/pp_mucore.ml b/backend/cn/lib/pp_mucore.ml index db39e2022..5109b55b1 100644 --- a/backend/cn/lib/pp_mucore.ml +++ b/backend/cn/lib/pp_mucore.ml @@ -704,7 +704,8 @@ module Make (Config : CONFIG) = struct label_args_and_body, _annots, _, - _loop_condition_loc ) -> + _loop_condition_loc, + _contains_user_spec ) -> P.break 1 ^^ !^"label" ^^^ pp_symbol sym diff --git a/backend/cn/lib/pp_mucore_ast.ml b/backend/cn/lib/pp_mucore_ast.ml index 3792111e9..4889aa8ff 100644 --- a/backend/cn/lib/pp_mucore_ast.ml +++ b/backend/cn/lib/pp_mucore_ast.ml @@ -241,7 +241,7 @@ module PP = struct let dtree_of_label l def = match def with | Return loc -> Dleaf (!^"return" ^^^ Cerb_location.pp_location ~clever:false loc) - | Label (loc, args_and_body, _, _, _) -> + | Label (loc, args_and_body, _, _, _, _) -> Dnode ( pp_symbol l ^^^ Cerb_location.pp_location ~clever:false loc, [ dtree_of_arguments dtree_of_expr args_and_body ] ) diff --git a/backend/cn/lib/pp_mucore_coq.ml b/backend/cn/lib/pp_mucore_coq.ml index 0c9af8e55..ac81c80c6 100644 --- a/backend/cn/lib/pp_mucore_coq.ml +++ b/backend/cn/lib/pp_mucore_coq.ml @@ -1848,7 +1848,7 @@ let pp_parse_ast_label_spec (s : parse_ast_label_spec) = let pp_label_def pp_type = function | Return loc -> pp_constructor1 "Return" [ pp_location loc ] - | Label (loc, args, annots, spec, `Loop loop_locs) -> + | Label (loc, args, annots, spec, `Loop loop_locs, _contains_user_spec) -> pp_constructor1 "Label" [ pp_location loc; diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index f2d49a33b..761c35b93 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -2202,7 +2202,13 @@ module WProc = struct match def with | Return loc -> (AT.of_rt function_rt (LAT.I False.False), CF.Annot.LAreturn, loc) - | Label (loc, label_args_and_body, annots, _parsed_spec, _loop_condition_loc) -> + | Label + ( loc, + label_args_and_body, + annots, + _parsed_spec, + _loop_condition_loc, + _contains_user_spec ) -> let lt = WLabel.typ label_args_and_body in let kind = Option.get (CF.Annot.get_label_annot annots) in (lt, kind, loc) @@ -2227,7 +2233,13 @@ module WProc = struct (fun _sym def -> match def with | Return loc -> return (Return loc) - | Label (loc, label_args_and_body, annots, parsed_spec, loop_info) -> + | Label + ( loc, + label_args_and_body, + annots, + parsed_spec, + loop_info, + contains_user_spec ) -> let@ label_args_and_body = pure (WArgs.welltyped @@ -2237,7 +2249,14 @@ module WProc = struct loc label_args_and_body) in - return (Label (loc, label_args_and_body, annots, parsed_spec, loop_info))) + return + (Label + ( loc, + label_args_and_body, + annots, + parsed_spec, + loop_info, + contains_user_spec ))) labels Sym.compare in From 243795c3a2d1028e190d455996601ed6a676bd73 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Tue, 25 Feb 2025 17:17:49 +0000 Subject: [PATCH 27/28] update TODO to mention Ethan instead of Zain --- backend/cn/bin/main.ml | 4 ++-- backend/cn/lib/cn_internal_to_ail.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index 3e1201c84..b582faada 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -527,7 +527,7 @@ let run_seq_tests let _, sigma = ail_prog in Cn_internal_to_ail.augment_record_map (BaseTypes.Record []); Executable_spec.main - ~without_ownership_checking (* TODO: Zain *) + ~without_ownership_checking (* TODO: Ethan *) ~without_loop_invariants:true ~with_test_gen:true ~copy_source_dir:false @@ -667,7 +667,7 @@ let run_tests Cn_internal_to_ail.augment_record_map (BaseTypes.Record []); (try Executable_spec.main - ~without_ownership_checking (* TODO: Zain *) + ~without_ownership_checking (* TODO: Ethan *) ~without_loop_invariants:true ~with_test_gen:true ~copy_source_dir:false diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index 927711388..b33ac8082 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3505,7 +3505,7 @@ let rec cn_to_ail_lat_internal_2 List.map (fun stat_pair -> cn_to_ail_statements dts globals stat_pair) stats in let ail_loop_invariants = List.map (cn_to_ail_loop_inv dts globals preds) loop in - let ail_loop_invariants = List.filter_map Fun.id ail_loop_invariants in + let ail_loop_invariants = List.filter_map Fun.id ail_loop_invariants in let post_bs, post_ss = cn_to_ail_post_internal dts globals preds post in let ownership_stats_ = if without_ownership_checking then From 6df1e33968c7942d98e5e65116a115f41442d540 Mon Sep 17 00:00:00 2001 From: Rini Banerjee Date: Tue, 25 Feb 2025 23:24:25 +0000 Subject: [PATCH 28/28] Refactor to make contains_user_spec flag part of the existing Loop info used for runtime checking --- backend/cn/lib/check.ml | 4 +--- backend/cn/lib/cn_internal_to_ail.ml | 2 +- backend/cn/lib/consistent.ml | 8 +------- backend/cn/lib/core_to_mucore.ml | 7 +++---- backend/cn/lib/executable_spec_extract.ml | 3 +-- backend/cn/lib/mucore.ml | 10 ++++----- backend/cn/lib/mucore.mli | 10 ++++----- backend/cn/lib/pp_mucore.ml | 8 ++------ backend/cn/lib/pp_mucore_ast.ml | 2 +- backend/cn/lib/pp_mucore_coq.ml | 4 ++-- backend/cn/lib/wellTyped.ml | 25 +++-------------------- 11 files changed, 23 insertions(+), 60 deletions(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index d023d9799..31513d189 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -2208,9 +2208,7 @@ let check_procedure pure (match def with | Mu.Return _loc -> return () - | Label - (loc, label_args_and_body, _annots, _, _loop_info, _contains_user_spec) - -> + | Label (loc, label_args_and_body, _annots, _, _loop_info) -> debug 2 (lazy diff --git a/backend/cn/lib/cn_internal_to_ail.ml b/backend/cn/lib/cn_internal_to_ail.ml index b33ac8082..6b5aa023f 100644 --- a/backend/cn/lib/cn_internal_to_ail.ml +++ b/backend/cn/lib/cn_internal_to_ail.ml @@ -3321,7 +3321,6 @@ let rec cn_to_ail_loop_inv_aux in ((cond_loc, (cond_bs, cond_ss)), (loop_loc, (loop_bs, loop_ss))) | L lat -> - Printf.printf "Reached AT.L\n"; let rec modify_decls_for_loop decls modified_stats = let rec collect_initialised_syms_and_exprs = function | [] -> [] @@ -3391,6 +3390,7 @@ let cn_to_ail_loop_inv let ail_stat_as_expr_stat = A.(AilSexpr (mk_expr ail_gcc_stat_as_expr)) in Some ((cond_loc, (cond_bs, [ ail_stat_as_expr_stat ])), (loop_loc, loop_bs_and_ss))) else + (* Produce no runtime loop invariant statements if the user has not written any spec for this loop*) None diff --git a/backend/cn/lib/consistent.ml b/backend/cn/lib/consistent.ml index 69192d264..78eb932f3 100644 --- a/backend/cn/lib/consistent.ml +++ b/backend/cn/lib/consistent.ml @@ -185,13 +185,7 @@ let procedure : Loc.t -> _ Mucore.args_and_body -> unit Typing.t = (fun _sym def -> match def with | Mucore.Return _ -> return () - | Label - ( loc, - label_args_and_body, - _annots, - _parsed_spec, - _loop_info, - _contains_user_spec ) -> + | Label (loc, label_args_and_body, _annots, _parsed_spec, _loop_info) -> pure_and_no_initial_resources loc (arguments diff --git a/backend/cn/lib/core_to_mucore.ml b/backend/cn/lib/core_to_mucore.ml index 9750ee582..791e575ae 100644 --- a/backend/cn/lib/core_to_mucore.ml +++ b/backend/cn/lib/core_to_mucore.ml @@ -1142,7 +1142,7 @@ let normalise_label | Mi_Label (loc, lt, label_args, label_body, annots) -> (match CF.Annot.get_label_annot annots with | Some (LAloop loop_id) -> - let@ desugared_inv, cn_desugaring_state, loop_condition_loc, contains_user_spec = + let@ desugared_inv, cn_desugaring_state, loop_info = match Pmap.lookup loop_id loop_attributes with | Some { marker_id; attributes = attrs; loc_condition; loc_loop } -> let@ inv = Parse.loop_spec attrs in @@ -1157,7 +1157,7 @@ let normalise_label } in let@ inv, d_st = desugar_conds d_st inv in - return (inv, d_st.inner.cn_state, (loc_condition, loc_loop), contains_user_spec) + return (inv, d_st.inner.cn_state, (loc_condition, loc_loop, contains_user_spec)) | None -> assert false (* return ([], precondition_cn_desugaring_state) *) in @@ -1189,8 +1189,7 @@ let normalise_label label_args_and_body, annots, { label_spec = desugared_inv }, - `Loop loop_condition_loc, - contains_user_spec )) + `Loop loop_info )) (* | Some (LAloop_body _loop_id) -> *) (* assert_error loc !^"body label has not been inlined" *) | Some (LAloop_continue _loop_id) -> diff --git a/backend/cn/lib/executable_spec_extract.ml b/backend/cn/lib/executable_spec_extract.ml index b920db846..7d38390ac 100644 --- a/backend/cn/lib/executable_spec_extract.ml +++ b/backend/cn/lib/executable_spec_extract.ml @@ -111,8 +111,7 @@ let from_loop ((_label_sym : Sym.t), (label_def : _ label_def)) : loop option = label_args_and_body, _annots, _, - `Loop (loop_condition_loc, loop_loc), - contains_user_spec ) -> + `Loop (loop_condition_loc, loop_loc, contains_user_spec) ) -> let label_args_and_body = Core_to_mucore.at_of_arguments Fun.id label_args_and_body in let label_args_and_statements = ArgumentTypes.map stmts_in_expr label_args_and_body in Some (contains_user_spec, loop_condition_loc, loop_loc, label_args_and_statements) diff --git a/backend/cn/lib/mucore.ml b/backend/cn/lib/mucore.ml index 313cddaaf..19b552c2c 100644 --- a/backend/cn/lib/mucore.ml +++ b/backend/cn/lib/mucore.ml @@ -379,12 +379,10 @@ type 'TY label_def = * 'TY expr arguments * Cerb_frontend.Annot.annot list * parse_ast_label_spec - * [ `Loop of Locations.t * Locations.t ] - * bool -(* whether any loop invariant was provided by the user, for executable checking *) - -(*first loc is condition, second is whole loop*) -(*loop condition location, for executable checking *) + * [ `Loop of Locations.t * Locations.t * bool ] +(* first loc is condition, second is whole loop *) +(* loop condition location, for executable checking *) +(* bool signifies whether any loop invariant was provided by the user, for executable checking *) type trusted = | Trusted of Locations.t diff --git a/backend/cn/lib/mucore.mli b/backend/cn/lib/mucore.mli index 99bb88ca0..50c56dc4a 100644 --- a/backend/cn/lib/mucore.mli +++ b/backend/cn/lib/mucore.mli @@ -282,12 +282,10 @@ type 'TY label_def = * 'TY expr arguments * Cerb_frontend.Annot.annot list * parse_ast_label_spec - * [ `Loop of Locations.t * Locations.t ] - * bool -(* whether any loop invariant was provided by the user, for executable checking *) - -(*first loc is condition, second is whole loop*) -(*loop condition location, for executable checking *) + * [ `Loop of Locations.t * Locations.t * bool ] +(* first loc is condition, second is whole loop *) +(* loop condition location, for executable checking *) +(* bool signifies whether any loop invariant was provided by the user, for executable checking *) type trusted = | Trusted of Locations.t diff --git a/backend/cn/lib/pp_mucore.ml b/backend/cn/lib/pp_mucore.ml index 5109b55b1..b1ec6ae22 100644 --- a/backend/cn/lib/pp_mucore.ml +++ b/backend/cn/lib/pp_mucore.ml @@ -700,12 +700,8 @@ module Make (Config : CONFIG) = struct | Return _ -> P.break 1 ^^ !^"return label" ^^^ pp_symbol sym | Label - ( _loc, - label_args_and_body, - _annots, - _, - _loop_condition_loc, - _contains_user_spec ) -> + (_loc, label_args_and_body, _annots, _, _loop_info) + -> P.break 1 ^^ !^"label" ^^^ pp_symbol sym diff --git a/backend/cn/lib/pp_mucore_ast.ml b/backend/cn/lib/pp_mucore_ast.ml index 4889aa8ff..3792111e9 100644 --- a/backend/cn/lib/pp_mucore_ast.ml +++ b/backend/cn/lib/pp_mucore_ast.ml @@ -241,7 +241,7 @@ module PP = struct let dtree_of_label l def = match def with | Return loc -> Dleaf (!^"return" ^^^ Cerb_location.pp_location ~clever:false loc) - | Label (loc, args_and_body, _, _, _, _) -> + | Label (loc, args_and_body, _, _, _) -> Dnode ( pp_symbol l ^^^ Cerb_location.pp_location ~clever:false loc, [ dtree_of_arguments dtree_of_expr args_and_body ] ) diff --git a/backend/cn/lib/pp_mucore_coq.ml b/backend/cn/lib/pp_mucore_coq.ml index ac81c80c6..bdb286aab 100644 --- a/backend/cn/lib/pp_mucore_coq.ml +++ b/backend/cn/lib/pp_mucore_coq.ml @@ -1848,14 +1848,14 @@ let pp_parse_ast_label_spec (s : parse_ast_label_spec) = let pp_label_def pp_type = function | Return loc -> pp_constructor1 "Return" [ pp_location loc ] - | Label (loc, args, annots, spec, `Loop loop_locs, _contains_user_spec) -> + | Label (loc, args, annots, spec, `Loop (cond_loc, loop_loc, _)) -> pp_constructor1 "Label" [ pp_location loc; pp_arguments (pp_expr pp_type) args; pp_list pp_annot_t annots; pp_parse_ast_label_spec spec; - pp_pair pp_location pp_location loop_locs + pp_pair pp_location pp_location (cond_loc, loop_loc) ] diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index 761c35b93..d6e1dd0d7 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -2202,13 +2202,7 @@ module WProc = struct match def with | Return loc -> (AT.of_rt function_rt (LAT.I False.False), CF.Annot.LAreturn, loc) - | Label - ( loc, - label_args_and_body, - annots, - _parsed_spec, - _loop_condition_loc, - _contains_user_spec ) -> + | Label (loc, label_args_and_body, annots, _parsed_spec, _loop_info) -> let lt = WLabel.typ label_args_and_body in let kind = Option.get (CF.Annot.get_label_annot annots) in (lt, kind, loc) @@ -2233,13 +2227,7 @@ module WProc = struct (fun _sym def -> match def with | Return loc -> return (Return loc) - | Label - ( loc, - label_args_and_body, - annots, - parsed_spec, - loop_info, - contains_user_spec ) -> + | Label (loc, label_args_and_body, annots, parsed_spec, loop_info) -> let@ label_args_and_body = pure (WArgs.welltyped @@ -2249,14 +2237,7 @@ module WProc = struct loc label_args_and_body) in - return - (Label - ( loc, - label_args_and_body, - annots, - parsed_spec, - loop_info, - contains_user_spec ))) + return (Label (loc, label_args_and_body, annots, parsed_spec, loop_info))) labels Sym.compare in