diff options
| -rw-r--r-- | src/rewrites.ml | 26 | ||||
| -rw-r--r-- | test/c/pattern_concat_nest.sail | 22 | ||||
| -rw-r--r-- | test/c/rv_duopod_bug.expect | 2 | ||||
| -rw-r--r-- | test/c/rv_duopod_bug.sail | 13 |
4 files changed, 34 insertions, 29 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index becf2a88..179f2feb 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1034,7 +1034,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = let mk_num_exp i = mk_lit_exp (L_num i) in let check_eq_exp l r = let exp = mk_exp (E_app_infix (l, Id_aux (Operator "==", Parse_ast.Unknown), r)) in - check_exp env exp bool_typ in + check_exp (Env.no_casts env) exp bool_typ in let access_bit_exp rootid l typ idx = let access_aux = E_vector_access (mk_exp (E_id rootid), mk_num_exp idx) in @@ -3307,7 +3307,7 @@ let rewrite_lit_ocaml (L_aux (lit, _)) = match lit with | L_num _ | L_string _ | L_hex _ | L_bin _ | L_real _ | L_unit -> false | _ -> true -let rewrite_defs_pat_lits rewrite_lit env = +let rewrite_defs_pat_lits rewrite_lit env ast = let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = let guards = ref [] in let counter = ref 0 in @@ -3347,8 +3347,18 @@ let rewrite_defs_pat_lits rewrite_lit env = end in + let rewrite_funcl (FCL_aux (FCL_Funcl (id, pexp), (l, annot))) = + FCL_aux (FCL_Funcl (id, rewrite_pexp pexp), (l, annot)) in + let rewrite_fun (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, annot))) = + FD_aux (FD_function (recopt, tannotopt, effectopt, List.map rewrite_funcl funcls), (l, annot)) in + let rewrite_def = function + | DEF_fundef fdef -> DEF_fundef (rewrite_fun fdef) + | def -> def + in + let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in - rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } + let Defs defs = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in + Defs (List.map rewrite_def defs) (* Now all expressions have no blocks anymore, any term is a sequence of let-expressions, @@ -4910,13 +4920,13 @@ let rewrites_lem = [ ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("pattern_literals", [Literal_arg "lem"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); ("remove_numeral_pats", []); + ("pattern_literals", [Literal_arg "lem"]); ("guarded_pats", []); ("bitvector_exps", []); (* ("register_ref_writes", rewrite_register_ref_writes); *) @@ -4952,13 +4962,13 @@ let rewrites_coq = [ ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("pattern_literals", [Literal_arg "lem"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); ("remove_numeral_pats", []); + ("pattern_literals", [Literal_arg "lem"]); ("guarded_pats", []); ("bitvector_exps", []); (* ("register_ref_writes", rewrite_register_ref_writes); *) @@ -4998,13 +5008,13 @@ let rewrites_ocaml = [ ("mapping_builtins", []); ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); - ("pattern_literals", [Literal_arg "ocaml"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); ("remove_not_pats", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); + ("pattern_literals", [Literal_arg "ocaml"]); ("remove_numeral_pats", []); ("exp_lift_assign", []); ("top_sort_defs", []); @@ -5027,12 +5037,12 @@ let rewrites_c = [ ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); + ("remove_vector_concat", []); + ("remove_bitvector_pats", []); ("pattern_literals", [Literal_arg "all"]); ("vector_concat_assignments", []); ("tuple_assignments", []); ("simple_assignments", []); - ("remove_vector_concat", []); - ("remove_bitvector_pats", []); ("exp_lift_assign", []); ("merge_function_clauses", []); ("optimize_recheck_defs", []); diff --git a/test/c/pattern_concat_nest.sail b/test/c/pattern_concat_nest.sail index 92150e66..398e814f 100644 --- a/test/c/pattern_concat_nest.sail +++ b/test/c/pattern_concat_nest.sail @@ -1,26 +1,6 @@ default Order dec -type bits ('n : Int) = vector('n, dec, bit) - -union option ('a : Type) = {None : unit, Some : 'a} - -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", c: "vector_subrange"} - : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm & 'm <= 'n. - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) - -val bitvector_access = {ocaml: "access", lem: "access_vec_dec", c: "vector_access"} - : forall ('n : Int) ('m : Int), 0 <= 'm & 'm + 1 <= 'n. - (bits('n), atom('m)) -> bit - -overload vector_access = {bitvector_access} - -val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"}: (bit, bit) -> bool - -overload operator == = { - eq_bit -} - -val and_bool = {ocaml: "and_bool", lem: "and_bool", smt: "and_bool", interpreter: "and_bool", c: "and_bool"}: (bool, bool) -> bool +$include <prelude.sail> //////////////////////////////////////////////////////////// diff --git a/test/c/rv_duopod_bug.expect b/test/c/rv_duopod_bug.expect new file mode 100644 index 00000000..681c7c43 --- /dev/null +++ b/test/c/rv_duopod_bug.expect @@ -0,0 +1,2 @@ +0 0x0000000000000000 +1 0xFFFFFFFFFFFFFFFF diff --git a/test/c/rv_duopod_bug.sail b/test/c/rv_duopod_bug.sail new file mode 100644 index 00000000..9a11996c --- /dev/null +++ b/test/c/rv_duopod_bug.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val rX : int -> bits(64) + +function rX 0 = sail_zeros(64) +and rX (r if r > 0) = sail_ones(64) + +function main() -> unit = { + print_bits("0 ", rX(0)); + print_bits("1 ", rX(1)) +} |