[CN-exec] Fix anonymous records

backend/cn/lib/cn_internal_to_ail.ml

@@ -54,37 +54,20 @@ module MembersKey = struct
     | [], [] -> 0
     | _, [] -> 1
     | [], _ -> -1
-    | (id, _) :: ms, (id', _) :: ms' ->
+    | (id, cn_bt) :: ms, (id', cn_bt') :: ms' ->
       let c = String.compare (Id.s id) (Id.s id') in
-      if c == 0 then
-        0
+      if c == 0 then (
+        let c' =
+          BaseTypes.compare (cn_base_type_to_bt cn_bt) (cn_base_type_to_bt cn_bt')
+        in
+        if c' == 0 then
+          compare ms ms'
+        else
+          c')
       else
-        compare ms ms'
+        c
 end
 
-let members_equal ms ms' =
-  if List.length ms != List.length ms' then
-    false
-  else if List.length ms == 0 then
-    true
-  else (
-    let ids, cn_bts = List.split ms in
-    let ids', cn_bts' = List.split ms' in
-    let ctypes_eq =
-      List.map2
-        (fun cn_bt cn_bt' ->
-          let bt = cn_base_type_to_bt cn_bt in
-          let bt' = cn_base_type_to_bt cn_bt' in
-          BT.equal bt bt')
-        cn_bts
-        cn_bts'
-    in
-    let ctypes_eq = List.fold_left ( && ) true ctypes_eq in
-    let ids_eq = List.map2 Id.equal ids ids' in
-    let ids_eq = List.fold_left ( && ) true ids_eq in
-    ctypes_eq && ids_eq)
-
-
 module RecordMap = Map.Make (MembersKey)
 
 let records = ref RecordMap.empty
@@ -108,15 +91,10 @@ let generate_sym_with_suffix
   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
-  (* Printf.printf "%s\n" str; *)
   Sym.fresh_pretty str
 
 
 let generate_error_msg_info_update_stats ?(cn_source_loc_opt = None) () =
-  (* let line_number_member_lhs = mk_expr A.(AilEmemberofptr (error_msg_info_ident, Id.id "line_number")) in
-     let curr_line_number = mk_expr A.(AilEident (Sym.fresh_pretty "__LINE__")) in
-     let addition_expr = mk_expr A.(AilEbinary (curr_line_number, Arithmetic Add, mk_expr (AilEconst (ConstantInteger (IConstant (Z.of_int 1, Decimal, None)))))) in
-     let line_number_assign_stat_ = [A.(AilSexpr (mk_expr (AilEassign (line_number_member_lhs, addition_expr))))] in *)
   let cn_source_loc_arg =
     match cn_source_loc_opt with
     | Some loc ->
@@ -186,26 +164,21 @@ let str_of_bt_bitvector_type sign size =
   sign_str ^ size_str
 
 
-let generate_record_sym sym members =
-  match sym with
-  | Some sym' ->
-    let sym'' = generate_sym_with_suffix ~suffix:"_record" sym' in
-    records := RecordMap.add members sym'' !records;
-    sym''
-  | None ->
-    let map_bindings = RecordMap.bindings !records in
-    (* Printf.printf "Record table size: %d\n" (List.length map_bindings); *)
-    let eq_members_bindings =
-      List.filter (fun (k, v) -> members_equal k members) map_bindings
-    in
-    (match eq_members_bindings with
-     | [] ->
-       (* First time reaching record of this type - add to map *)
-       let count = RecordMap.cardinal !records in
-       let sym' = Sym.fresh_pretty ("record_" ^ string_of_int count) in
-       records := RecordMap.add members sym' !records;
-       sym'
-     | (_, sym') :: _ -> sym')
+let augment_record_map ?cn_sym bt =
+  let sym_prefix = match cn_sym with Some sym' -> sym' | None -> Sym.fresh () in
+  match bt_to_cn_base_type bt with
+  | CN_record members ->
+    (* Augment records map if entry does not exist already *)
+    if not (RecordMap.mem members !records) then (
+      let sym' = generate_sym_with_suffix ~suffix:"_record" sym_prefix in
+      records := RecordMap.add members sym' !records)
+  | _ -> ()
+
+
+let lookup_records_map members =
+  match RecordMap.find_opt members !records with
+  | Some sym -> sym
+  | None -> failwith "Record not found in map"
 
 
 (* TODO: Complete *)
@@ -227,7 +200,7 @@ let rec cn_to_ail_base_type ?(pred_sym = None) cn_typ =
       (* gets replaced with typedef anyway (TODO: clean up) *)
     | CN_struct sym -> C.(Struct (generate_sym_with_suffix ~suffix:"_cn" sym))
     | CN_record members ->
-      let sym = generate_record_sym pred_sym members in
+      let sym = lookup_records_map members in
       Struct sym
     (* Every struct is converted into a struct pointer *)
     | CN_datatype sym -> Struct sym
@@ -236,11 +209,12 @@ let rec cn_to_ail_base_type ?(pred_sym = None) cn_typ =
       generate_ail_array bt
       (* TODO: What is the optional second pair element for? Have just put None for now *)
     | CN_tuple ts ->
+      failwith (__FUNCTION__ ^ ":Tuples not yet supported")
       (* Printf.printf "Entered CN_tuple case\n"; *)
-      let some_id = create_id_from_sym (Sym.fresh_pretty "some_sym") in
-      let members = List.map (fun t -> (some_id, t)) ts in
-      let sym = generate_record_sym pred_sym members in
-      Struct sym
+      (* let some_id = create_id_from_sym (Sym.fresh_pretty "some_sym") in
+         let members = List.map (fun t -> (some_id, t)) ts in
+         let sym = lookup_records_map members in
+         Struct sym *)
     | CN_set bt -> generate_ail_array bt
     | CN_user_type_name _ -> failwith "TODO CN_user_type_name"
     | CN_c_typedef_name _ -> failwith "TODO CN_c_typedef_name"
@@ -1108,7 +1082,7 @@ let rec cn_to_ail_expr_aux_internal
     let transformed_ms =
       List.map (fun (id, it) -> (id, bt_to_cn_base_type (IT.bt it))) ms
     in
-    let sym_name = generate_record_sym pred_name transformed_ms in
+    let sym_name = lookup_records_map transformed_ms in
     let ctype_ = C.(Pointer (empty_qualifiers, mk_ctype (Struct sym_name))) in
     let res_binding = create_binding res_sym (mk_ctype ctype_) in
     let fn_call =
@@ -2921,7 +2895,10 @@ let cn_to_ail_function_internal
         cn_to_ail_expr_internal_with_pred_name (Some fn_sym) cn_datatypes [] it Return
       in
       (bs, Some (List.map mk_stmt ss))
-    | Uninterp -> ([], None)
+    | Uninterp ->
+      failwith
+        "Uninterpreted CN functions not supported at runtime. Please provide a concrete \
+         function definition"
   in
   let ail_record_opt = generate_record_opt fn_sym lf_def.return_bt in
   let params = List.map (fun (sym, bt) -> (sym, bt_to_ail_ctype bt)) lf_def.args in

backend/cn/lib/cn_internal_to_ail.mli

@@ -17,6 +17,8 @@ module RecordMap : module type of Map.Make (MembersKey)
 
 val records : Sym.t RecordMap.t ref
 
+val augment_record_map : ?cn_sym:Sym.sym -> BT.t -> unit
+
 val bt_to_cn_base_type : BT.t -> Sym.t CF.Cn.cn_base_type
 
 val bt_to_ail_ctype : ?pred_sym:Sym.t option -> BT.t -> C.ctype

backend/cn/lib/executable_spec.ml

@@ -213,8 +213,8 @@ let main
   let oc = Stdlib.open_out (Filename.concat prefix output_filename) in
   let cn_oc = Stdlib.open_out (Filename.concat prefix "cn.c") in
   let cn_header_oc = Stdlib.open_out (Filename.concat prefix "cn.h") in
-  populate_record_map prog5;
   let instrumentation, symbol_table = Core_to_mucore.collect_instrumentation prog5 in
+  Executable_spec_records.populate_record_map instrumentation prog5;
   let executable_spec =
     generate_c_specs_internal
       with_ownership_checking

backend/cn/lib/executable_spec_internal.ml

@@ -4,6 +4,10 @@ open PPrint
 open Executable_spec_utils
 module BT = BaseTypes
 module A = CF.AilSyntax
+module IT = IndexTerms
+module LRT = LogicalReturnTypes
+module LAT = LogicalArgumentTypes
+module AT = ArgumentTypes
 (* Executable spec helper functions *)
 
 type executable_spec =
@@ -41,33 +45,6 @@ let generate_ail_stat_strs
   List.map CF.Pp_utils.to_plain_pretty_string doc
 
 
-let populate_record_map_aux (sym, bt_ret_type) =
-  match Cn_internal_to_ail.bt_to_cn_base_type bt_ret_type with
-  | CF.Cn.CN_record members ->
-    let sym' = Cn_internal_to_ail.generate_sym_with_suffix ~suffix:"_record" sym in
-    Cn_internal_to_ail.records
-    := Cn_internal_to_ail.RecordMap.add members sym' !Cn_internal_to_ail.records
-  | _ -> ()
-
-
-(* Populate record table with function and predicate record return types *)
-let populate_record_map (prog5 : unit Mucore.mu_file) =
-  let fun_syms_and_ret_types =
-    List.map
-      (fun (sym, (def : LogicalFunctions.definition)) -> (sym, def.return_bt))
-      prog5.mu_logical_predicates
-  in
-  let pred_syms_and_ret_types =
-    List.map
-      (fun (sym, (def : ResourcePredicates.definition)) -> (sym, def.oarg_bt))
-      prog5.mu_resource_predicates
-  in
-  let _ =
-    List.map populate_record_map_aux (fun_syms_and_ret_types @ pred_syms_and_ret_types)
-  in
-  ()
-
-
 let rec extract_global_variables = function
   | [] -> []
   | (sym, mu_globs) :: ds ->

backend/cn/lib/executable_spec_records.ml

@@ -0,0 +1,139 @@
+module CF = Cerb_frontend
+module CB = Cerb_backend
+open Executable_spec_utils
+module BT = BaseTypes
+module A = CF.AilSyntax
+module IT = IndexTerms
+module LRT = LogicalReturnTypes
+module LAT = LogicalArgumentTypes
+module AT = ArgumentTypes
+
+let rec add_records_to_map_from_it it =
+  match IT.term it with
+  | IT.Sym _s -> ()
+  | Const _c -> ()
+  | Unop (_uop, t1) -> add_records_to_map_from_it t1
+  | Binop (_bop, t1, t2) -> List.iter add_records_to_map_from_it [ t1; t2 ]
+  | ITE (t1, t2, t3) -> List.iter add_records_to_map_from_it [ t1; t2; t3 ]
+  | EachI ((_, (_, _), _), t) -> add_records_to_map_from_it t
+  | Tuple _ts -> failwith "TODO: Tuples not yet supported"
+  | NthTuple (_, _t) -> failwith "TODO: Tuples not yet supported"
+  | Struct (_tag, members) ->
+    List.iter (fun (_, it') -> add_records_to_map_from_it it') members
+  | StructMember (t, _member) -> add_records_to_map_from_it t
+  | StructUpdate ((t1, _member), t2) -> List.iter add_records_to_map_from_it [ t1; t2 ]
+  | Record members ->
+    (* Anonymous record instantiation -> add to records map *)
+    Cn_internal_to_ail.augment_record_map (IT.bt it);
+    List.iter (fun (_, it') -> add_records_to_map_from_it it') members
+  | RecordMember (t, _member) -> add_records_to_map_from_it t
+  | RecordUpdate ((t1, _member), t2) -> List.iter add_records_to_map_from_it [ t1; t2 ]
+  | Cast (_cbt, t) -> add_records_to_map_from_it t
+  | MemberShift (t, _tag, _id) -> add_records_to_map_from_it t
+  | ArrayShift { base; ct = _; index = _ } -> add_records_to_map_from_it base
+  | CopyAllocId { addr; loc } -> List.iter add_records_to_map_from_it [ addr; loc ]
+  | HasAllocId loc -> add_records_to_map_from_it loc
+  | SizeOf _ct -> ()
+  | OffsetOf (_tag, _member) -> ()
+  | Nil _bt -> ()
+  | Cons (t1, t2) -> List.iter add_records_to_map_from_it [ t1; t2 ]
+  | Head t -> add_records_to_map_from_it t
+  | Tail t -> add_records_to_map_from_it t
+  | NthList (i, xs, d) -> List.iter add_records_to_map_from_it [ i; xs; d ]
+  | ArrayToList (arr, i, len) -> List.iter add_records_to_map_from_it [ arr; i; len ]
+  | Representable (_sct, t) -> add_records_to_map_from_it t
+  | Good (_sct, t) -> add_records_to_map_from_it t
+  | WrapI (_ity, t) -> add_records_to_map_from_it t
+  | Aligned { t; align } -> List.iter add_records_to_map_from_it [ t; align ]
+  | MapConst (_bt, t) -> add_records_to_map_from_it t
+  | MapSet (t1, t2, t3) -> List.iter add_records_to_map_from_it [ t1; t2; t3 ]
+  | MapGet (t1, t2) -> List.iter add_records_to_map_from_it [ t1; t2 ]
+  | MapDef ((_, _), t) -> add_records_to_map_from_it t
+  | Apply (_pred, ts) -> List.iter add_records_to_map_from_it ts
+  | Let ((_, t1), t2) -> List.iter add_records_to_map_from_it [ t1; t2 ]
+  | Match (e, cases) -> List.iter add_records_to_map_from_it (e :: List.map snd cases)
+  | Constructor (_sym, args) -> List.iter add_records_to_map_from_it (List.map snd args)
+
+
+let add_records_to_map_from_resource = function
+  | ResourceTypes.P p -> List.iter add_records_to_map_from_it (p.pointer :: p.iargs)
+  | Q q ->
+    List.iter add_records_to_map_from_it (q.pointer :: q.step :: q.permission :: q.iargs)
+
+
+let add_records_to_map_from_lc = function
+  | LogicalConstraints.T it | Forall (_, it) -> add_records_to_map_from_it it
+
+
+let add_records_to_map_from_cn_statement = function
+  | Cnprog.M_CN_assert lc -> add_records_to_map_from_lc lc
+  (* All other CN statements are (currently) no-ops at runtime *)
+  | M_CN_pack_unpack _ | M_CN_have _ | M_CN_instantiate _ | M_CN_split_case _
+  | M_CN_extract _ | M_CN_unfold _ | M_CN_apply _ | M_CN_inline _ | M_CN_print _ ->
+    ()
+
+
+let add_records_to_map_from_cnprogs (_, cn_progs) =
+  let rec aux = function
+    | Cnprog.M_CN_let (_, (_, { ct = _; pointer }), prog) ->
+      add_records_to_map_from_it pointer;
+      aux prog
+    | M_CN_statement (_, stmt) -> add_records_to_map_from_cn_statement stmt
+  in
+  List.iter aux cn_progs
+
+
+let add_records_to_map_from_instrumentation (i : Core_to_mucore.instrumentation) =
+  let rec aux_lrt = function
+    | LRT.Define ((_, it), _, t) ->
+      add_records_to_map_from_it it;
+      aux_lrt t
+    | Resource ((_, (re, _)), _, t) ->
+      add_records_to_map_from_resource re;
+      aux_lrt t
+    | Constraint (lc, _, t) ->
+      add_records_to_map_from_lc lc;
+      aux_lrt t
+    | I -> ()
+  in
+  let rec aux_lat = function
+    | LAT.Define ((_, it), _, lat) ->
+      add_records_to_map_from_it it;
+      aux_lat lat
+    | Resource ((_, (ret, _)), _, lat) ->
+      add_records_to_map_from_resource ret;
+      aux_lat lat
+    | Constraint (lc, _, lat) ->
+      add_records_to_map_from_lc lc;
+      aux_lat lat
+    (* Postcondition *)
+    | I (ReturnTypes.Computational (_, _, t), stats) ->
+      List.iter add_records_to_map_from_cnprogs stats;
+      aux_lrt t
+  in
+  let rec aux_at = function
+    | AT.Computational ((_, _), _, at) -> aux_at at
+    | L lat -> aux_lat lat
+  in
+  match i.internal with Some instr -> aux_at instr | None -> ()
+
+
+(* Populate record table *)
+let populate_record_map
+  (instrumentation : Core_to_mucore.instrumentation list)
+  (prog5 : unit Mucore.mu_file)
+  =
+  let fun_syms_and_ret_types =
+    List.map
+      (fun (sym, (def : LogicalFunctions.definition)) -> (sym, def.return_bt))
+      prog5.mu_logical_predicates
+  in
+  let pred_syms_and_ret_types =
+    List.map
+      (fun (sym, (def : ResourcePredicates.definition)) -> (sym, def.oarg_bt))
+      prog5.mu_resource_predicates
+  in
+  List.iter
+    (fun (cn_sym, bt) -> Cn_internal_to_ail.augment_record_map ~cn_sym bt)
+    (fun_syms_and_ret_types @ pred_syms_and_ret_types);
+  List.iter add_records_to_map_from_instrumentation instrumentation