From e6b4776f43e99ce121d167fa42b80dfe090cf752 Mon Sep 17 00:00:00 2001 From: Jon French Date: Thu, 23 Aug 2018 10:53:14 +0100 Subject: Move vector_string_to_bit_list from its odd place in Rewriter.rewrite_pat to an explicit rewrite step in Rewrites, just before pat_lits --- src/rewriter.ml | 42 ---------------------------------- src/rewriter.mli | 3 --- src/rewrites.ml | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 68 insertions(+), 45 deletions(-) (limited to 'src') diff --git a/src/rewriter.ml b/src/rewriter.ml index 82e1ec95..4521758b 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -240,40 +240,6 @@ let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match destruct_tannot (snd annot | None -> LB_aux (lb, (l, empty_tannot)) -let explode s = - let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in - exp (String.length s - 1) [] - -let vector_string_to_bit_list l lit = - - let hexchar_to_binlist = function - | '0' -> ['0';'0';'0';'0'] - | '1' -> ['0';'0';'0';'1'] - | '2' -> ['0';'0';'1';'0'] - | '3' -> ['0';'0';'1';'1'] - | '4' -> ['0';'1';'0';'0'] - | '5' -> ['0';'1';'0';'1'] - | '6' -> ['0';'1';'1';'0'] - | '7' -> ['0';'1';'1';'1'] - | '8' -> ['1';'0';'0';'0'] - | '9' -> ['1';'0';'0';'1'] - | 'A' -> ['1';'0';'1';'0'] - | 'B' -> ['1';'0';'1';'1'] - | 'C' -> ['1';'1';'0';'0'] - | 'D' -> ['1';'1';'0';'1'] - | 'E' -> ['1';'1';'1';'0'] - | 'F' -> ['1';'1';'1';'1'] - | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in - - let s_bin = match lit with - | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex))) - | L_bin s_bin -> explode s_bin - | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in - - List.map (function '0' -> L_aux (L_zero, gen_loc l) - | '1' -> L_aux (L_one, gen_loc l) - | _ -> raise (Reporting_basic.err_unreachable (gen_loc l) "binary had non-zero or one")) s_bin - let rewrite_pexp rewriters = let rewrite = rewriters.rewrite_exp rewriters in function @@ -286,10 +252,6 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) = let rewrap p = P_aux (p,(l,annot)) in let rewrite = rewriters.rewrite_pat rewriters in match pat with - | P_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> - let ps = List.map (fun p -> P_aux (P_lit p, (l, mk_tannot (pat_env_of orig_pat) bit_typ no_effect))) - (vector_string_to_bit_list l lit) in - rewrap (P_vector ps) | P_lit _ | P_wild | P_id _ | P_var _ -> rewrap pat | P_or(pat1, pat2) -> rewrap (P_or(rewrite pat1, rewrite pat2)) | P_not(pat) -> rewrap (P_not(rewrite pat)) @@ -312,10 +274,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = match exp with | E_block exps -> rewrap (E_block (List.map rewrite exps)) | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps)) - | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> - let es = List.map (fun p -> E_aux (E_lit p, (l, mk_tannot (env_of orig_exp) bit_typ no_effect))) - (vector_string_to_bit_list l lit) in - rewrap (E_vector es) | E_id _ | E_lit _ -> rewrap exp | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp)) | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps)) diff --git a/src/rewriter.mli b/src/rewriter.mli index da4702b5..2acc1814 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -239,6 +239,3 @@ val fix_eff_fexp : tannot fexp -> tannot fexp val fix_eff_fexps : tannot fexps -> tannot fexps val fix_eff_opt_default : tannot opt_default -> tannot opt_default - -(* AA: How this is used in rewrite_pat seems suspect to me *) -val vector_string_to_bit_list : Parse_ast.l -> lit_aux -> lit list diff --git a/src/rewrites.ml b/src/rewrites.ml index b7104da3..b032e3ec 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -145,6 +145,40 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match destruct_tannot annot w | Some (_, _, eff) -> effectful_effs eff | _ -> false +let explode s = + let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in + exp (String.length s - 1) [] + +let vector_string_to_bit_list l lit = + + let hexchar_to_binlist = function + | '0' -> ['0';'0';'0';'0'] + | '1' -> ['0';'0';'0';'1'] + | '2' -> ['0';'0';'1';'0'] + | '3' -> ['0';'0';'1';'1'] + | '4' -> ['0';'1';'0';'0'] + | '5' -> ['0';'1';'0';'1'] + | '6' -> ['0';'1';'1';'0'] + | '7' -> ['0';'1';'1';'1'] + | '8' -> ['1';'0';'0';'0'] + | '9' -> ['1';'0';'0';'1'] + | 'A' -> ['1';'0';'1';'0'] + | 'B' -> ['1';'0';'1';'1'] + | 'C' -> ['1';'1';'0';'0'] + | 'D' -> ['1';'1';'0';'1'] + | 'E' -> ['1';'1';'1';'0'] + | 'F' -> ['1';'1';'1';'1'] + | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in + + let s_bin = match lit with + | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex))) + | L_bin s_bin -> explode s_bin + | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in + + List.map (function '0' -> L_aux (L_zero, gen_loc l) + | '1' -> L_aux (L_one, gen_loc l) + | _ -> raise (Reporting_basic.err_unreachable (gen_loc l) "binary had non-zero or one")) s_bin + let find_used_vars exp = (* Overapproximates the set of used identifiers, but for the use cases below this is acceptable. *) @@ -1580,6 +1614,36 @@ let rewrite_defs_remove_numeral_pats = rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp; rewrite_fun = rewrite_fun } +let rewrite_defs_vector_string_pats_to_bit_list = + let rewrite_p_aux (pat, (annot : tannot annot)) = + let env = env_of_annot annot in + match pat with + | P_lit (L_aux (lit, l) as l_aux) -> + begin match lit with + | L_hex _ | L_bin _ -> P_aux (P_vector (List.map (fun p -> P_aux (P_lit p, (l, mk_tannot env bit_typ no_effect))) (vector_string_to_bit_list l lit)), annot) + | lit -> P_aux (P_lit l_aux, annot) + end + | pat -> (P_aux (pat, annot)) + in + let rewrite_e_aux (exp, (annot : tannot annot)) = + let env = env_of_annot annot in + match exp with + | E_lit (L_aux (lit, l) as l_aux) -> + begin match lit with + | L_hex _ | L_bin _ -> E_aux (E_vector (List.map (fun e -> E_aux (E_lit e, (l, mk_tannot env bit_typ no_effect))) (vector_string_to_bit_list l lit)), annot) + | lit -> E_aux (E_lit l_aux, annot) + end + | exp -> (E_aux (exp, annot)) + in + let pat_alg = { id_pat_alg with p_aux = rewrite_p_aux } in + let rewrite_pat rw pat = + fold_pat pat_alg pat + in + let rewrite_exp rw exp = + fold_exp { id_exp_alg with e_aux = rewrite_e_aux; pat_alg = pat_alg } exp + in + rewrite_defs_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp } + (* Remove pattern guards by rewriting them to if-expressions within the pattern expression. *) let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = @@ -4420,6 +4484,7 @@ let rewrite_defs_lem = [ ("rewrite_atoms_to_singletons", if_mono Monomorphise.rewrite_atoms_to_singletons); ("recheck_defs", if_mono recheck_defs); ("rewrite_undefined", rewrite_undefined_if_gen false); + ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -4460,6 +4525,7 @@ let rewrite_defs_coq = [ ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("rewrite_undefined", rewrite_undefined_if_gen true); + ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -4501,6 +4567,7 @@ let rewrite_defs_ocaml = [ ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("rewrite_undefined", rewrite_undefined_if_gen false); + ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("pat_lits", rewrite_defs_pat_lits rewrite_no_strings); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -4524,6 +4591,7 @@ let rewrite_defs_c = [ ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("rewrite_undefined", rewrite_undefined_if_gen false); + ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("pat_lits", rewrite_defs_pat_lits rewrite_no_strings); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); -- cgit v1.2.3