From 325ec55dea017c7b095c407454835014d31f70b8 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 25 Mar 2019 14:57:22 +0000 Subject: Lem: Output constant bitvectors as hex or bin literals Requires Lem version with support for those literals, e.g. 0007a1c. --- src/ast_util.ml | 36 ++++++++++++++++- src/ast_util.mli | 2 + src/pretty_print_lem.ml | 24 ++++++++---- src/rewrites.ml | 100 ++++++++++++++++++------------------------------ 4 files changed, 90 insertions(+), 72 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index a7c97338..3e1cc8d5 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1536,6 +1536,41 @@ let hex_to_bin hex = |> List.map Sail_lib.char_of_bit |> (fun bits -> String.init (List.length bits) (List.nth bits)) +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_aux (lit, l)) = + + 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.err_unreachable l __POS__ "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_ascii s_hex))) + | L_bin s_bin -> explode s_bin + | _ -> raise (Reporting.err_unreachable l __POS__ "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.err_unreachable (gen_loc l) __POS__ "binary had non-zero or one")) s_bin + + (* Functions for working with locations *) let locate_id f (Id_aux (name, l)) = Id_aux (name, f l) @@ -2038,4 +2073,3 @@ let rec find_annot_defs sl = function | [] -> None let rec find_annot_ast sl (Defs defs) = find_annot_defs sl defs - diff --git a/src/ast_util.mli b/src/ast_util.mli index 815ef421..d61d068a 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -459,6 +459,8 @@ val subst : id -> 'a exp -> 'a exp -> 'a exp val hex_to_bin : string -> string +val vector_string_to_bit_list : lit -> lit list + (** {2 Manipulating locations} *) (** locate takes an expression and recursively sets the location in diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 20c9a69f..301e55f4 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -389,22 +389,24 @@ let doc_tannot_lem ctxt env eff typ = let min_int32 = Big_int.of_int64 (Int64.of_int32 Int32.min_int) let max_int32 = Big_int.of_int64 (Int64.of_int32 Int32.max_int) -let doc_lit_lem (L_aux(lit,l)) = +let rec doc_lit_lem (L_aux(lit,l)) = match lit with | L_unit -> utf8string "()" | L_zero -> utf8string "B0" | L_one -> utf8string "B1" | L_false -> utf8string "false" | L_true -> utf8string "true" - | L_num i when Big_int.less_equal min_int32 i && Big_int.less_equal i max_int32 -> + | L_num i -> let ipp = Big_int.to_string i in utf8string ( if Big_int.less i Big_int.zero then "((0"^ipp^"):ii)" else "("^ipp^":ii)") - | L_num i -> - utf8string (Printf.sprintf "(integerOfString \"%s\")" (Big_int.to_string i)) - | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) - | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) + | L_hex n when !opt_mwords -> utf8string ("0x" ^ n) + | L_bin n when !opt_mwords -> utf8string ("0b" ^ n) + | L_hex _ | L_bin _ -> + vector_string_to_bit_list (L_aux(lit,l)) + |> flow_map (semi ^^ break 0) doc_lit_lem + |> group |> align |> brackets | L_undef -> utf8string "(return (failwith \"undefined value of unsupported type\"))" | L_string s -> utf8string ("\"" ^ (String.escaped s) ^ "\"") @@ -838,8 +840,14 @@ let doc_exp_lem, doc_let_lem = else if Env.is_register id env && is_regtyp (typ_of full_exp) env then doc_id_lem (append_id id "_ref") else if is_ctor env id then doc_id_lem_ctor id else doc_id_lem id - | E_lit lit -> doc_lit_lem lit - | E_cast(typ,e) -> expV aexp_needed e + | E_lit lit -> + let env = env_of full_exp in + let typ = Env.expand_synonyms env (typ_of full_exp) in + let eff = effect_of full_exp in + if typ_needs_printed typ + then parens (doc_lit_lem lit ^^ doc_tannot_lem ctxt env (effectful eff) typ) + else doc_lit_lem lit + | E_cast (typ,e) -> expV aexp_needed e (*parens (expN e ^^ doc_tannot_lem ctxt (env_of full_exp) (effectful (effect_of full_exp)) typ)*) | E_tuple exps -> parens (align (group (separate_map (comma ^^ break 1) expN exps))) | E_record fexps -> diff --git a/src/rewrites.ml b/src/rewrites.ml index 502b910c..01658006 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -145,40 +145,6 @@ 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.err_unreachable l __POS__ "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_ascii s_hex))) - | L_bin s_bin -> explode s_bin - | _ -> raise (Reporting.err_unreachable l __POS__ "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.err_unreachable (gen_loc l) __POS__ "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. *) @@ -300,30 +266,6 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids = rewrite_typ -let rewrite_bitvector_exps env defs = - let e_aux = function - | (E_vector es, ((l, tannot) as a)) when not (is_empty_tannot tannot) -> - let env = env_of_annot (l, tannot) in - let typ = typ_of_annot (l, tannot) in - let eff = effect_of_annot tannot in - if is_bitvector_typ typ then - try - let len = mk_lit_exp (L_num (Big_int.of_int (List.length es))) in - let es = mk_exp (E_list (List.map strip_exp es)) in - let exp = mk_exp (E_app (mk_id "bitvector_of_bitlist", [len; es])) in - check_exp env exp typ - with - | _ -> E_aux (E_vector es, a) - else - E_aux (E_vector es, a) - | (e_aux, a) -> E_aux (e_aux, a) - in - let rewrite_exp _ = fold_exp { id_exp_alg with e_aux = e_aux } in - if IdSet.mem (mk_id "bitvector_of_bitlist") (val_spec_ids defs) then - rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } defs - else defs - - let rewrite_defs_remove_assert defs = let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with | E_constraint _ -> @@ -1275,7 +1217,7 @@ let rewrite_defs_vector_string_pats_to_bit_list env = 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) + | 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_aux)), annot) | lit -> P_aux (P_lit l_aux, annot) end | pat -> (P_aux (pat, annot)) @@ -1285,7 +1227,7 @@ let rewrite_defs_vector_string_pats_to_bit_list env = 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) + | 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_aux)), annot) | lit -> E_aux (E_lit l_aux, annot) end | exp -> (E_aux (exp, annot)) @@ -1299,6 +1241,39 @@ let rewrite_defs_vector_string_pats_to_bit_list env = in rewrite_defs_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp } +let rewrite_bit_lists_to_lits env = + (* TODO Make all rewriting passes support bitvector literals instead of + converting back and forth *) + let open Sail2_values in + let bit_of_lit = function + | L_aux (L_zero, _) -> Some B0 + | L_aux (L_one, _) -> Some B1 + | _ -> None + in + let bit_of_exp = function E_aux (E_lit lit, _) -> bit_of_lit lit | _ -> None in + let string_of_chars cs = String.concat "" (List.map (String.make 1) cs) in + let lit_of_bits bits = match hexstring_of_bits bits with + | Some h -> L_hex (string_of_chars h) + | None -> L_bin (string_of_chars (List.map bitU_char bits)) + in + let e_aux (e, (l, annot)) = + let rewrap e = E_aux (e, (l, annot)) in + try + let env = env_of_annot (l, annot) in + let typ = typ_of_annot (l, annot) in + match e with + | E_vector es when is_bitvector_typ typ -> + (match just_list (List.map bit_of_exp es) with + | Some bits -> + check_exp env (mk_exp (E_cast (typ, mk_lit_exp (lit_of_bits bits)))) typ + | None -> rewrap e) + | E_cast (typ', E_aux (E_cast (_, e'), _)) -> rewrap (E_cast (typ', e')) + | _ -> rewrap e + with _ -> rewrap e + in + let rewrite_exp rw = fold_exp { id_exp_alg with e_aux = e_aux; } in + rewrite_defs_base { rewriters_base with 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) = @@ -2032,7 +2007,7 @@ let rewrite_simple_types env (Defs defs) = let rec simple_lit (L_aux (lit_aux, l) as lit) = match lit_aux with | L_bin _ | L_hex _ -> - E_list (List.map (fun b -> E_aux (E_lit b, simple_annot l bit_typ)) (vector_string_to_bit_list l lit_aux)) + E_list (List.map (fun b -> E_aux (E_lit b, simple_annot l bit_typ)) (vector_string_to_bit_list lit)) | _ -> E_lit lit in let simple_def = function @@ -4688,7 +4663,6 @@ let rewrite_defs_lem = [ ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("guarded_pats", rewrite_defs_guarded_pats); - ("bitvector_exps", rewrite_bitvector_exps); (* ("register_ref_writes", rewrite_register_ref_writes); *) ("nexp_ids", rewrite_defs_nexp_ids); ("fix_val_specs", rewrite_fix_val_specs); @@ -4711,6 +4685,7 @@ let rewrite_defs_lem = [ ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds); ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns); ("merge function clauses", merge_funcls); + ("bit_lists_to_lits", rewrite_bit_lists_to_lits); ("recheck_defs", recheck_defs) ] @@ -4732,7 +4707,6 @@ let rewrite_defs_coq = [ ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("guarded_pats", rewrite_defs_guarded_pats); - ("bitvector_exps", rewrite_bitvector_exps); (* ("register_ref_writes", rewrite_register_ref_writes); *) ("nexp_ids", rewrite_defs_nexp_ids); ("fix_val_specs", rewrite_fix_val_specs); -- cgit v1.2.3