diff options
| -rw-r--r-- | src/constraint.ml | 2 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 4 | ||||
| -rw-r--r-- | test/c/toplevel_tyvar.expect | 1 | ||||
| -rw-r--r-- | test/c/toplevel_tyvar.sail | 14 | ||||
| -rw-r--r-- | test/typecheck/pass/type_pow_zero.sail | 12 |
5 files changed, 30 insertions, 3 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index d8241e1d..1a4129ff 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -181,7 +181,7 @@ let to_smt l vars constr = | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2] | Nexp_exp nexp -> begin match nexp_simp nexp with - | Nexp_aux (Nexp_constant c, _) when Big_int.greater c Big_int.zero -> + | Nexp_aux (Nexp_constant c, _) when Big_int.greater_equal c Big_int.zero -> Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c))) | nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp] | nexp -> sfun "^" [Atom "2"; smt_nexp nexp] diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index c13b7f3b..242f31b2 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -398,14 +398,14 @@ let analyze_primop' ctx id args typ = c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")")); match extern, args with - | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) -> begin match cval_ctyp v1 with | CT_fbits _ | CT_sbits _ -> AE_val (AV_cval (V_call (Eq, [v1; v2]), typ)) | _ -> no_change end - | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] -> + | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) -> begin match cval_ctyp v1 with | CT_fbits _ | CT_sbits _ -> AE_val (AV_cval (V_call (Neq, [v1; v2]), typ)) diff --git a/test/c/toplevel_tyvar.expect b/test/c/toplevel_tyvar.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/toplevel_tyvar.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/toplevel_tyvar.sail b/test/c/toplevel_tyvar.sail new file mode 100644 index 00000000..af2f4d1e --- /dev/null +++ b/test/c/toplevel_tyvar.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +let 'var = 32 + +function main() -> unit = { + let x: bits('var) = 0xFFFF_FFFF; + let y: bits(32) = 0xFFFF_FFFF; + assert(x == y); + print_endline("ok") +} diff --git a/test/typecheck/pass/type_pow_zero.sail b/test/typecheck/pass/type_pow_zero.sail new file mode 100644 index 00000000..cc7b5736 --- /dev/null +++ b/test/typecheck/pass/type_pow_zero.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <flow.sail> + +/* Run this test with CVC4, as we want to test that 1 - 1 gets +simplified, and 2 ^ 0 evaluates directly to 1. CVC4 doesn't deal with +power unlike z3, so by using it we ensure we check this. */ +$option -smt_solver cvc4 + +function test() -> unit = { + _prove(constraint(2 ^ (1 - 1) == 1)) +} |