diff options
Diffstat (limited to 'src/jib/c_backend.ml')
| -rw-r--r-- | src/jib/c_backend.ml | 48 |
1 files changed, 27 insertions, 21 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index f6d8dd80..0fe986e4 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -405,40 +405,46 @@ let analyze_primop' ctx id args typ = match extern, args with (* - | "eq_bits", [AV_cval (v1, _, CT_fbits _); AV_cval (v2, _, _)] -> - AE_val (AV_cval (F_op (v1, "==", v2), typ, CT_bool)) - | "eq_bits", [AV_cval (v1, _, CT_sbits _); AV_cval (v2, _, _)] -> - AE_val (AV_cval (F_call ("eq_sbits", [v1; v2]), typ, CT_bool)) - - | "neq_bits", [AV_cval (v1, _, CT_fbits _); AV_cval (v2, _, _)] -> - AE_val (AV_cval (F_op (v1, "!=", v2), typ, CT_bool)) - | "neq_bits", [AV_cval (v1, _, CT_sbits _); AV_cval (v2, _, _)] -> - AE_val (AV_cval (F_call ("neq_sbits", [v1; v2]), typ, CT_bool)) - - | "eq_int", [AV_cval (v1, typ1, _); AV_cval (v2, typ2, _)] -> - AE_val (AV_cval (F_op (v1, "==", v2), typ, CT_bool)) + | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + AE_val (AV_cval (V_op (v1, "==", v2), typ)) + | CT_sbits _ -> + AE_val (AV_cval (V_call ("eq_sbits", [v1; v2]), typ)) + | _ -> no_change + end - | "zeros", [_] -> - begin match destruct_vector ctx.tc_env typ with - | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) - when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> - AE_val (AV_C_fragment (F_raw "0x0", typ, CT_fbits (Big_int.to_int n, true))) + | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + begin match cval_ctyp v1 with + | CT_fbits _ -> + AE_val (AV_cval (V_op (v1, "!=", v2), typ)) + | CT_sbits _ -> + AE_val (AV_cval (V_call ("neq_sbits", [v1; v2]), typ)) | _ -> no_change end - | "zero_extend", [AV_C_fragment (v1, _, CT_fbits _); _] -> + | "eq_int", [AV_cval (v1, _); AV_cval (v2, _)] -> + AE_val (AV_cval (V_op (v1, "==", v2), typ)) + + | "zeros", [_] -> begin match destruct_vector ctx.tc_env typ with | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> - AE_val (AV_C_fragment (v1, typ, CT_fbits (Big_int.to_int n, true))) + let n = Big_int.to_int n in + AE_val (AV_cval (V_lit (VL_bits (Util.list_init n (fun _ -> Sail2_values.B0), true), CT_fbits (n, true)), typ)) | _ -> no_change end - | "zero_extend", [AV_C_fragment (v1, _, CT_sbits _); _] -> + | "zero_extend", [AV_cval (v1, _); _] -> begin match destruct_vector ctx.tc_env typ with | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> - AE_val (AV_C_fragment (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true))) + begin match cval_ctyp v1 with + | CT_fbits _ -> + AE_val (AV_C_fragment (v1, typ, CT_fbits (Big_int.to_int n, true))) + | CT_sbits _ -> + AE_val (AV_C_fragment (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true))) + end | _ -> no_change end |