diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 9 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 10 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 6 |
3 files changed, 11 insertions, 14 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index b98c53c4..2c9c11ee 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -148,9 +148,8 @@ let rec ctyp_of_typ ctx typ = - If the length is less than 64, then use a small bits type, sbits. - If the length may be larger than 64, use a large bits type lbits. *) | Typ_app (id, [A_aux (A_nexp n, _); - A_aux (A_order ord, _); - A_aux (A_typ (Typ_aux (Typ_id vtyp_id, _)), _)]) - when string_of_id id = "vector" && string_of_id vtyp_id = "bit" -> + A_aux (A_order ord, _)]) + when string_of_id id = "bitvector" -> let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in begin match nexp_simp n with | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction) @@ -1429,8 +1428,8 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = end | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) - | "undefined_vector", CT_fbits _ -> "UNDEFINED(fbits)" - | "undefined_vector", CT_lbits _ -> "UNDEFINED(lbits)" + | "undefined_bitvector", CT_fbits _ -> "UNDEFINED(fbits)" + | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)" | "undefined_bit", _ -> "UNDEFINED(fbits)" | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) | fname, _ -> fname diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index f8cb3bcd..90c0022d 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -310,10 +310,10 @@ let rec compile_aval l ctx = function begin let bitstring = List.map value_of_aval_bit avals in let len = List.length avals in - match destruct_vector ctx.tc_env typ with - | Some (_, Ord_aux (Ord_inc, _), _) -> + match destruct_bitvector ctx.tc_env typ with + | Some (_, Ord_aux (Ord_inc, _)) -> [], V_lit (VL_bits (bitstring, false), CT_fbits (len, false)), [] - | Some (_, Ord_aux (Ord_dec, _), _) -> + | Some (_, Ord_aux (Ord_dec, _)) -> [], V_lit (VL_bits (bitstring, true), CT_fbits (len, true)), [] | Some _ -> raise (Reporting.err_general l "Encountered order polymorphic bitvector literal") @@ -337,8 +337,8 @@ let rec compile_aval l ctx = function [iclear (CT_lbits true) gs] (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *) - | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ (Typ_aux (Typ_id bit_id, _)), _)]), _)) - when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 -> + | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _)]), _)) + when string_of_id id = "bitvector" && List.length avals <= 64 -> let len = List.length avals in let direction = match ord with | Ord_aux (Ord_inc, _) -> false diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 897c685a..0d70695b 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1147,10 +1147,8 @@ let rec ctyp_of_typ ctx typ = CT_list (ctyp_of_typ ctx typ) (* Note that we have to use lbits for zero-length bitvectors because they are not allowed by SMTLIB *) - | Typ_app (id, [A_aux (A_nexp n, _); - A_aux (A_order ord, _); - A_aux (A_typ (Typ_aux (Typ_id vtyp_id, _)), _)]) - when string_of_id id = "vector" && string_of_id vtyp_id = "bit" -> + | Typ_app (id, [A_aux (A_nexp n, _); A_aux (A_order ord, _)]) + when string_of_id id = "bitvector" -> let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in begin match nexp_simp n with | Nexp_aux (Nexp_constant n, _) when Big_int.equal n Big_int.zero -> CT_lbits direction |