[CN-exec] RB+CP cleaning up executable checking utils.c and utils.h (#651)

---------

Co-authored-by: Rini Banerjee <[email protected]>

Author: cp526

backend/cn/lib/cn_internal_to_ail.ml

@@ -116,15 +116,23 @@ let generate_error_msg_info_update_stats ?(cn_source_loc_opt = None) () =
   ]
 
 
+let cn_pop_msg_info_sym = Sym.fresh_pretty "cn_pop_msg_info"
+
+let generate_cn_pop_msg_info =
+  let expr_ = A.(AilEcall (mk_expr (AilEident cn_pop_msg_info_sym), [])) in
+  [ A.(AilSexpr (mk_expr expr_)) ]
+
+
 let cn_assert_sym = Sym.fresh_pretty "cn_assert"
 
-let generate_cn_assert ?(cn_source_loc_opt = None) ail_expr =
+let generate_cn_assert (*?(cn_source_loc_opt = None)*) ail_expr =
   let assertion_expr_ = A.(AilEcall (mk_expr (AilEident cn_assert_sym), [ ail_expr ])) in
   let assertion_stat = A.(AilSexpr (mk_expr assertion_expr_)) in
-  let error_msg_update_stats_ =
+  (*let error_msg_update_stats_ =
     generate_error_msg_info_update_stats ~cn_source_loc_opt ()
-  in
-  error_msg_update_stats_ @ [ assertion_stat ]
+    in*)
+  (*error_msg_update_stats_ @*)
+  [ assertion_stat ]
 
 
 let rec bt_to_cn_base_type = function
@@ -689,8 +697,10 @@ let dest_with_unit_check
   fun d (b, s, e, is_unit) ->
   match d with
   | Assert loc ->
-    let assert_stmts = generate_cn_assert ~cn_source_loc_opt:(Some loc) e in
-    (b, s @ assert_stmts)
+    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 assert_stmts = generate_cn_assert (*~cn_source_loc_opt:(Some loc)*) e in
+    (b, s @ upd_s @ assert_stmts @ pop_s)
   | Return ->
     let return_stmt = if is_unit then A.(AilSreturnVoid) else A.(AilSreturn e) in
     (b, s @ [ return_stmt ])
@@ -855,7 +865,7 @@ let rec cn_to_ail_expr_aux_internal
     a dest ->
     a
   =
-  fun const_prop pred_name dts globals (IT (term_, basetype, loc)) d ->
+  fun const_prop pred_name dts globals (IT (term_, basetype, _loc)) d ->
   match term_ with
   | Const const ->
     let ail_expr_, is_unit = cn_to_ail_const_internal const in
@@ -1331,10 +1341,12 @@ let rec cn_to_ail_expr_aux_internal
     let bs, ss, es = list_split_three bs_ss_es in
     let f = mk_expr A.(AilEident sym) in
     let ail_expr_ = A.AilEcall (f, es) in
-    let error_msg_update_stats_ =
+    (*let error_msg_update_stats_ =
       generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) ()
-    in
-    dest d (List.concat bs, List.concat ss @ error_msg_update_stats_, mk_expr ail_expr_)
+      in*)
+    dest
+      d
+      (List.concat bs, List.concat ss (*@ error_msg_update_stats_*), mk_expr ail_expr_)
   | Let ((var, t1), body) ->
     let b1, s1, e1 =
       cn_to_ail_expr_aux_internal const_prop pred_name dts globals t1 PassBack
@@ -2542,7 +2554,7 @@ let cn_to_ail_resource_internal
   dts
   globals
   (preds : (Sym.t * RP.definition) list)
-  loc
+  _loc
   =
   let calculate_return_type = function
     | ResourceTypes.Owned (sct, _) ->
@@ -2597,9 +2609,9 @@ let cn_to_ail_resource_internal
           list_split_three
             (List.map (fun it -> cn_to_ail_expr_internal dts globals it PassBack) p.iargs)
         in
-        let error_msg_update_stats_ =
+        (*let error_msg_update_stats_ =
           generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) ()
-        in
+          in*)
         let fcall =
           A.(
             AilEcall
@@ -2608,7 +2620,7 @@ let cn_to_ail_resource_internal
         let binding = create_binding sym (bt_to_ail_ctype ~pred_sym:(Some pname) bt) in
         ( mk_expr fcall,
           binding :: List.concat bs,
-          List.concat ss @ error_msg_update_stats_,
+          List.concat ss (*@ error_msg_update_stats_*),
           None )
     in
     let s_decl =
@@ -2704,17 +2716,17 @@ let cn_to_ail_resource_internal
           list_split_three
             (List.map (fun it -> cn_to_ail_expr_internal dts globals it PassBack) q.iargs)
         in
-        let error_msg_update_stats_ =
+        (*let error_msg_update_stats_ =
           generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some loc) ()
-        in
+          in*)
         let fcall =
           A.(
             AilEcall
               ( mk_expr (AilEident pname),
                 (mk_expr (AilEident ptr_add_sym) :: es) @ [ mk_expr (AilEident enum_sym) ]
               ))
         in
-        (mk_expr fcall, List.concat bs, List.concat ss @ error_msg_update_stats_, None)
+        (mk_expr fcall, List.concat bs, List.concat ss (*@ error_msg_update_stats_*), None)
     in
     let typedef_name = get_typedef_string (bt_to_ail_ctype i_bt) in
     let incr_func_name =
@@ -2981,14 +2993,18 @@ let rec cn_to_ail_lat_internal ?(is_toplevel = true) dts pred_sym_opt globals pr
     let b2, s2 = cn_to_ail_lat_internal ~is_toplevel dts pred_sym_opt 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 ~is_toplevel dts pred_sym_opt globals preds lat in
-    (b1 @ b2, s1 @ s2)
+    (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 ss = s @ generate_cn_assert ~cn_source_loc_opt:(Some loc) e 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 ~is_toplevel dts pred_sym_opt globals preds lat in
     (b1 @ b2, ss @ s2)
   | LAT.I it ->
@@ -3019,6 +3035,13 @@ let cn_to_ail_predicate_internal
           preds
           c.packing_ft
       in
+      let ss =
+        (*let upd_s = generate_error_msg_info_update_stats ~cn_source_loc_opt:(Some rp_def.loc) () in
+          let pop_s = generate_cn_pop_msg_info in*)
+        (*upd_s @*)
+        ss
+        (*@ pop_s*)
+      in
       (match c.guard with
        | IT (Const (Bool true), _, _) ->
          let bs'', ss'' = clause_translate cs in
@@ -3114,25 +3137,36 @@ let rec cn_to_ail_post_aux_internal dts globals preds = function
     (b1 @ b2 @ [ binding ], (decl :: s1) @ s2)
   | LRT.Resource ((name, (re, bt)), (loc, _str_opt), t) ->
     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 new_lrt =
       Core_to_mucore.fn_spec_instrumentation_sym_subst_lrt (name, bt, new_name) t
     in
     let b2, s2 = cn_to_ail_post_aux_internal dts globals preds new_lrt in
-    (b1 @ b2, s1 @ s2)
+    (b1 @ b2, upd_s @ s1 @ pop_s @ s2)
   | LRT.Constraint (lc, (loc, _str_opt), t) ->
+    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, s, e = cn_to_ail_logical_constraint_internal dts globals PassBack lc in
-    let ss = s @ generate_cn_assert ~cn_source_loc_opt:(Some loc) e 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_post_aux_internal dts globals preds t in
     (b1 @ b2, ss @ s2)
   | LRT.I -> ([], [])
 
 
-let cn_to_ail_post_internal dts globals preds (RT.Computational (_bound, _oinfo, t)) =
+let cn_to_ail_post_internal
+  (*loc*) dts
+  globals
+  preds
+  (RT.Computational (_bound, _oinfo, t))
+  =
+  (*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 bs, ss = cn_to_ail_post_aux_internal dts globals preds t in
-  (bs, List.map mk_stmt ss)
+  (bs, List.map mk_stmt (*upd_s @*) ss (*@ pop_s*))
 
 
 (* TODO: Add destination passing *)
@@ -3196,8 +3230,10 @@ let rec cn_to_ail_cnprog_internal_aux dts globals = function
   else
     ((loc', b1 @ b2 @ [binding], s @ ail_stat_ :: ss), false) *)
   | Statement (loc, stmt) ->
+    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 (bs, ss), no_op = cn_to_ail_cnstatement_internal dts globals (Assert loc) stmt in
-    ((bs, ss), no_op)
+    ((bs, upd_s @ ss @ pop_s), no_op)
 
 
 let cn_to_ail_cnprog_internal dts globals cn_prog =
@@ -3206,11 +3242,13 @@ let cn_to_ail_cnprog_internal dts globals cn_prog =
 
 
 let cn_to_ail_statements dts globals (loc, cn_progs) =
+  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 bs_and_ss =
     List.map (fun prog -> cn_to_ail_cnprog_internal dts globals prog) cn_progs
   in
   let bs, ss = List.split bs_and_ss in
-  (loc, (List.concat bs, List.concat ss))
+  (loc, (List.concat bs, upd_s @ List.concat ss @ pop_s))
 
 
 let prepend_to_precondition ail_executable_spec (b1, s1) =
@@ -3242,6 +3280,8 @@ let rec cn_to_ail_lat_internal_2 with_ownership_checking dts globals preds c_ret
     in
     prepend_to_precondition ail_executable_spec (binding :: b1, decl :: s1)
   | 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 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
@@ -3258,10 +3298,12 @@ let rec cn_to_ail_lat_internal_2 with_ownership_checking dts globals preds c_ret
         c_return_type
         new_lat
     in
-    prepend_to_precondition ail_executable_spec (b1, s1)
+    prepend_to_precondition ail_executable_spec (b1, upd_s @ s1 @ pop_s)
   | LAT.Constraint (lc, (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, s, e = cn_to_ail_logical_constraint_internal dts globals PassBack lc in
-    let ss = s @ generate_cn_assert ~cn_source_loc_opt:(Some loc) e in
+    let ss = upd_s @ s @ generate_cn_assert (*~cn_source_loc_opt:(Some loc)*) e @ pop_s in
     let ail_executable_spec =
       cn_to_ail_lat_internal_2 with_ownership_checking dts globals preds c_return_type lat
     in

backend/cn/lib/ownership_exec.ml

@@ -9,17 +9,17 @@ let cn_ghost_state_struct_type =
   mk_ctype ~annots:[ CF.Annot.Atypedef (Sym.fresh_pretty "ownership_ghost_state") ] C.Void
 
 
-let cn_stack_depth_sym = Sym.fresh_pretty "cn_stack_depth"
+let get_cn_stack_depth_sym = Sym.fresh_pretty "get_cn_stack_depth"
 
 let cn_stack_depth_ctype = C.mk_ctype_integer (Signed Long)
 
 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 c_map_local_ownership_fn_sym = Sym.fresh_pretty "c_add_local_to_ghost_state"
+let c_add_ownership_fn_sym = Sym.fresh_pretty "c_add_to_ghost_state"
 
-let c_remove_local_ownership_fn_sym = Sym.fresh_pretty "c_remove_local_from_ghost_state"
+let c_remove_ownership_fn_sym = Sym.fresh_pretty "c_remove_from_ghost_state"
 
 (* TODO: Use these to reduce verbosity of output. Mirrors C+CN input slightly less since
    we replace declarations with a call to one of these macros *)
@@ -63,12 +63,6 @@ let get_end_loc ?(offset = 0) = function
       "get_end_loc: Location of AilSdeclaration should be Loc_region or Loc_regions"
 
 
-let create_ail_ownership_global_decls () =
-  [ (cn_ghost_state_sym, C.mk_ctype_pointer empty_qualifiers cn_ghost_state_struct_type);
-    (cn_stack_depth_sym, cn_stack_depth_ctype)
-  ]
-
-
 let get_ownership_global_init_stats () =
   let cn_ghost_state_init_fcall =
     mk_expr
@@ -96,9 +90,10 @@ let generate_c_local_ownership_entry_fcall (local_sym, local_ctype) =
       AilEcast (empty_qualifiers, C.uintptr_t, mk_expr (AilEunary (Address, local_ident))))
   in
   let arg2 = A.(AilEsizeof (empty_qualifiers, local_ctype)) in
+  let arg3 = A.(AilEcall (mk_expr (AilEident get_cn_stack_depth_sym), [])) in
   mk_expr
     (AilEcall
-       (mk_expr (AilEident c_map_local_ownership_fn_sym), List.map mk_expr [ arg1; arg2 ]))
+       (mk_expr (AilEident c_add_ownership_fn_sym), List.map mk_expr [ arg1; arg2; arg3 ]))
 
 
 (* int x = 0, y = 5;
@@ -154,7 +149,7 @@ let generate_c_local_ownership_exit (local_sym, local_ctype) =
       (mk_expr
          A.(
            AilEcall
-             ( mk_expr (AilEident c_remove_local_ownership_fn_sym),
+             ( mk_expr (AilEident c_remove_ownership_fn_sym),
                List.map mk_expr [ arg1; arg2 ] ))))
 
 

runtime/libcn/include/cn-executable/utils.h

@@ -39,6 +39,7 @@ struct cn_error_message_info {
     char *file_name;
     int line_number;
     char *cn_source_loc;
+    struct cn_error_message_info *parent;
 };
 
 void initialise_error_msg_info_(const char *function_name, char *file_name, int line_number);
@@ -47,13 +48,15 @@ void initialise_error_msg_info_(const char *function_name, char *file_name, int
 
 
 /* TODO: Implement */
-struct cn_error_messages {
+/*struct cn_error_messages {
     struct cn_error_message_info *top_level_error_msg_info;
     struct cn_error_message_info *nested_error_msg_info;
-};
+};*/
 
 void update_error_message_info_(const char *function_name, char *file_name, int line_number, char *cn_source_loc);
 
+void cn_pop_msg_info();
+
 #define update_cn_error_message_info(x)\
     update_error_message_info_(__func__, __FILE__, __LINE__ + 1, x)
 
@@ -120,6 +123,7 @@ typedef hash_table cn_map;
 
 void initialise_ownership_ghost_state(void);
 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);
 
@@ -522,13 +526,13 @@ void cn_assume_ownership(void *generic_c_ptr, unsigned long size, char *fun);
 void cn_check_ownership(enum OWNERSHIP owned_enum, uintptr_t generic_c_ptr, size_t size);
 
 /* C ownership checking */
-void c_add_local_to_ghost_state(uintptr_t ptr_to_local, size_t size);
-void c_remove_local_from_ghost_state(uintptr_t ptr_to_local, size_t size);
-void c_ownership_check(uintptr_t generic_c_ptr, int offset);
+void c_add_to_ghost_state(uintptr_t ptr_to_local, size_t size, signed long stack_depth);
+void c_remove_from_ghost_state(uintptr_t ptr_to_local, size_t size);
+void c_ownership_check(char *access_kind, uintptr_t generic_c_ptr, int offset, signed long expected_stack_depth);
 
 // Unused 
 #define c_concat_with_mapping_stat(STAT, CTYPE, VAR_NAME, GHOST_STATE, STACK_DEPTH)\
-    STAT; c_add_local_to_ghost_state((uintptr_t) &VAR_NAME, GHOST_STATE, sizeof(CTYPE), STACK_DEPTH);
+    STAT; c_add_to_ghost_state((uintptr_t) &VAR_NAME, GHOST_STATE, sizeof(CTYPE), STACK_DEPTH);
 
 #define c_declare_and_map_local(CTYPE, VAR_NAME)\
     c_concat_with_mapping_stat(CTYPE VAR_NAME, CTYPE, VAR_NAME)
@@ -558,7 +562,7 @@ static inline void cn_postfix(void *ptr, size_t size)
   ({                                                          \
     typeof(LV) *__tmp = &(LV);                                \
     update_cn_error_message_info_access_check(NULL);          \
-    c_ownership_check((uintptr_t) __tmp, sizeof(typeof(LV))); \
+    c_ownership_check("Load", (uintptr_t) __tmp, sizeof(typeof(LV)), get_cn_stack_depth()); \
     cn_load(__tmp, sizeof(typeof(LV)));                       \
     *__tmp;                                                   \
   })
@@ -568,7 +572,7 @@ static inline void cn_postfix(void *ptr, size_t size)
     typeof(LV) *__tmp;                                        \
     __tmp = &(LV);                                            \
     update_cn_error_message_info_access_check(NULL);          \
-    c_ownership_check((uintptr_t) __tmp, sizeof(typeof(LV))); \
+    c_ownership_check("Store", (uintptr_t) __tmp, sizeof(typeof(LV)), get_cn_stack_depth()); \
     cn_store(__tmp, sizeof(typeof(LV)));                      \
     *__tmp op##= (X);                                         \
  })
@@ -580,7 +584,7 @@ static inline void cn_postfix(void *ptr, size_t size)
     typeof(LV) *__tmp;                                        \
     __tmp = &(LV);                                            \
     update_cn_error_message_info_access_check(NULL);          \
-    c_ownership_check((uintptr_t) __tmp, sizeof(typeof(LV))); \
+    c_ownership_check("Postfix operation", (uintptr_t) __tmp, sizeof(typeof(LV)), get_cn_stack_depth()); \
     cn_postfix(__tmp, sizeof(typeof(LV)));                    \
     (*__tmp) OP;                                              \
  })