diff options
| author | jp | 2020-02-23 17:45:35 +0000 |
|---|---|---|
| committer | jp | 2020-02-23 17:45:35 +0000 |
| commit | e37855c0c43b8369aefa91cfd17889452011b137 (patch) | |
| tree | a62a9300112abd81830b1650a7d2d29421f62540 /src/jib/c_backend.ml | |
| parent | 219f8ef5aec4d6a4f918693bccc9dc548716ea41 (diff) | |
| parent | dd32e257ddecdeece792b508cc05c9acab153e70 (diff) | |
Merge branch 'sail2' of https://github.com/rems-project/sail into sail2
Diffstat (limited to 'src/jib/c_backend.ml')
| -rw-r--r-- | src/jib/c_backend.ml | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 2b144d35..2b2234b5 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1481,6 +1481,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)" | "undefined_bit", _ -> "UNDEFINED(fbits)" | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) + | "undefined_list", _ -> Printf.sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp) | fname, _ -> fname in if fname = "reg_deref" then @@ -1844,6 +1845,9 @@ let codegen_list_clear id ctyp = ^^ string " sail_free(*rop);" ^^ string "}" +let codegen_list_recreate id = + string (Printf.sprintf "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id)) + let codegen_list_set id ctyp = string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) ^^ string " if (op == NULL) { *rop = NULL; return; };\n" @@ -1879,6 +1883,20 @@ let codegen_pick id ctyp = else string (Printf.sprintf "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp)) +let codegen_list_equal id ctyp = + let open Printf in + ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id) + ^^ ksprintf string " if (op1 == NULL && op2 == NULL) { return true; };\n" + ^^ ksprintf string " if (op1 == NULL || op2 == NULL) { return false; };\n" + ^^ ksprintf string " return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id) + ^^ string "}" + +let codegen_list_undefined id ctyp = + let open Printf in + ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp) + ^^ ksprintf string " *rop = NULL;\n" + ^^ string "}" + let codegen_list ctx ctyp = let id = mk_id (string_of_ctyp (CT_list ctyp)) in if IdSet.mem id !generated then @@ -1889,9 +1907,12 @@ let codegen_list ctx ctyp = codegen_node id ctyp ^^ twice hardline ^^ codegen_list_init id ^^ twice hardline ^^ codegen_list_clear id ctyp ^^ twice hardline + ^^ codegen_list_recreate id ^^ twice hardline ^^ codegen_list_set id ctyp ^^ twice hardline ^^ codegen_cons id ctyp ^^ twice hardline ^^ codegen_pick id ctyp ^^ twice hardline + ^^ codegen_list_equal id ctyp ^^ twice hardline + ^^ codegen_list_undefined id ctyp ^^ twice hardline end (* Generate functions for working with non-bit vectors of some specific type. *) |