diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail2_deep_shallow_convert.lem | 68 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 63 | ||||
| -rw-r--r-- | src/lem_interp/sail2_instr_kinds.lem | 175 | ||||
| -rw-r--r-- | src/optimize.ml | 58 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 20 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 4 | ||||
| -rw-r--r-- | src/process_file.ml | 4 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 26 | ||||
| -rw-r--r-- | src/sail.ml | 17 | ||||
| -rw-r--r-- | src/toFromInterp_backend.ml | 8 |
11 files changed, 263 insertions, 181 deletions
diff --git a/src/gen_lib/sail2_deep_shallow_convert.lem b/src/gen_lib/sail2_deep_shallow_convert.lem index b963e537..2e3543b4 100644 --- a/src/gen_lib/sail2_deep_shallow_convert.lem +++ b/src/gen_lib/sail2_deep_shallow_convert.lem @@ -455,17 +455,61 @@ instance (ToFromInterpValue write_kind) end +let a64_barrier_domainToInterpValue = function + | A64_FullShare -> + V_ctor (Id_aux (Id "A64_FullShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 0) (toInterpValue ()) + | A64_InnerShare -> + V_ctor (Id_aux (Id "A64_InnerShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 1) (toInterpValue ()) + | A64_OuterShare -> + V_ctor (Id_aux (Id "A64_OuterShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 2) (toInterpValue ()) + | A64_NonShare -> + V_ctor (Id_aux (Id "A64_NonShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 3) (toInterpValue ()) +end +let rec a64_barrier_domainFromInterpValue v = match v with + | V_ctor (Id_aux (Id "A64_FullShare") _) _ _ v -> A64_FullShare + | V_ctor (Id_aux (Id "A64_InnerShare") _) _ _ v -> A64_InnerShare + | V_ctor (Id_aux (Id "A64_OuterShare") _) _ _ v -> A64_OuterShare + | V_ctor (Id_aux (Id "A64_NonShare") _) _ _ v -> A64_NonShare + | V_tuple [v] -> a64_barrier_domainFromInterpValue v + | v -> failwith ("fromInterpValue a64_barrier_domain: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue a64_barrier_domain) + let toInterpValue = a64_barrier_domainToInterpValue + let fromInterpValue = a64_barrier_domainFromInterpValue +end + +let a64_barrier_typeToInterpValue = function + | A64_barrier_all -> + V_ctor (Id_aux (Id "A64_barrier_all") Unknown) (T_id "a64_barrier_type") (C_Enum 0) (toInterpValue ()) + | A64_barrier_LD -> + V_ctor (Id_aux (Id "A64_barrier_LD") Unknown) (T_id "a64_barrier_type") (C_Enum 1) (toInterpValue ()) + | A64_barrier_ST -> + V_ctor (Id_aux (Id "A64_barrier_ST") Unknown) (T_id "a64_barrier_type") (C_Enum 2) (toInterpValue ()) +end +let rec a64_barrier_typeFromInterpValue v = match v with + | V_ctor (Id_aux (Id "A64_barrier_all") _) _ _ v -> A64_barrier_all + | V_ctor (Id_aux (Id "A64_barrier_LD") _) _ _ v -> A64_barrier_LD + | V_ctor (Id_aux (Id "A64_barrier_ST") _) _ _ v -> A64_barrier_ST + | V_tuple [v] -> a64_barrier_typeFromInterpValue v + | v -> failwith ("fromInterpValue a64_barrier_type: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue a64_barrier_type) + let toInterpValue = a64_barrier_typeToInterpValue + let fromInterpValue = a64_barrier_typeFromInterpValue +end + + let barrier_kindToInterpValue = function | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ()) | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ()) | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ()) | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ()) - | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ()) - | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ()) - | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ()) - | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ()) - | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) - | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) + | Barrier_DMB (dom,typ) -> + V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ)) + | Barrier_DSB (dom,typ) -> + V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ)) | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ()) @@ -482,12 +526,12 @@ let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync - | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB - | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST - | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD - | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB - | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST - | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD + | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> + let (dom, typ) = fromInterpValue v in + Barrier_DMB (dom,typ) + | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> + let (dom, typ) = fromInterpValue v in + Barrier_DSB (dom,typ) | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 74e43a8f..3413494e 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -579,74 +579,13 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ -> NIA_indirect_address | _ -> failwith "Register footprint analysis did not return nia of expected type" end in - let readk_to_readk = function - | "Read_plain" -> Read_plain - | "Read_reserve" -> Read_reserve - | "Read_acquire" -> Read_acquire - | "Read_exclusive" -> Read_exclusive - | "Read_exclusive_acquire" -> Read_exclusive_acquire - | "Read_stream" -> Read_stream - | "Read_RISCV_acquire" -> Read_RISCV_acquire - | "Read_RISCV_strong_acquire" -> Read_RISCV_strong_acquire - | "Read_RISCV_reserved" -> Read_RISCV_reserved - | "Read_RISCV_reserved_acquire" -> Read_RISCV_reserved_acquire - | "Read_RISCV_reserved_strong_acquire" -> Read_RISCV_reserved_strong_acquire - | "Read_X86_locked" -> Read_X86_locked - | r -> failwith ("unknown read kind: " ^ r) end in - let writek_to_writek = function - | "Write_plain" -> Write_plain - | "Write_conditional" -> Write_conditional - | "Write_release" -> Write_release - | "Write_exclusive" -> Write_exclusive - | "Write_exclusive_release" -> Write_exclusive_release - | "Write_RISCV_release" -> Write_RISCV_release - | "Write_RISCV_strong_release" -> Write_RISCV_strong_release - | "Write_RISCV_conditional" -> Write_RISCV_conditional - | "Write_RISCV_conditional_release" -> Write_RISCV_conditional_release - | "Write_RISCV_conditional_strong_release" -> Write_RISCV_conditional_strong_release - | "Write_X86_locked" -> Write_X86_locked - | w -> failwith ("unknown write kind: " ^ w) end in - let ik_to_ik = function - | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) -> - IK_barrier (match b with - | "Barrier_Sync" -> Barrier_Sync - | "Barrier_LwSync" -> Barrier_LwSync - | "Barrier_Eieio" -> Barrier_Eieio - | "Barrier_Isync" -> Barrier_Isync - | "Barrier_DMB" -> Barrier_DMB - | "Barrier_DMB_ST" -> Barrier_DMB_ST - | "Barrier_DMB_LD" -> Barrier_DMB_LD - | "Barrier_DSB" -> Barrier_DSB - | "Barrier_DSB_ST" -> Barrier_DSB_ST - | "Barrier_DSB_LD" -> Barrier_DSB_LD - | "Barrier_ISB" -> Barrier_ISB - | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC - | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE - end) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> - IK_mem_read(readk_to_readk r) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ - (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) -> - IK_mem_write(writek_to_writek w) - | Interp_ast.V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ - (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ; - (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) -> - IK_mem_rmw(readk_to_readk readk, writek_to_writek writek) - | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ -> - IK_branch - | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> - IK_simple - | _ -> failwith "Analysis returned unexpected instruction kind" - end in let (regs1,regs2,regs3,nias,dia,ik) = (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3, List.map nia_to_nia nias, dia_to_dia dia, - ik_to_ik ik) in + fromInterpValue ik) in ((regs1,regs2,regs3,nias,dia,ik), events) | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end) | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed" diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem index bd3a3eb7..f3cdfbc9 100644 --- a/src/lem_interp/sail2_instr_kinds.lem +++ b/src/lem_interp/sail2_instr_kinds.lem @@ -136,58 +136,86 @@ instance (Show write_kind) end end +type a64_barrier_domain = + A64_FullShare + | A64_InnerShare + | A64_OuterShare + | A64_NonShare + +type a64_barrier_type = + A64_barrier_all + | A64_barrier_LD + | A64_barrier_ST + type barrier_kind = (* Power barriers *) - Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + Barrier_Sync of unit | Barrier_LwSync of unit | Barrier_Eieio of unit | Barrier_Isync of unit (* AArch64 barriers *) - | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB - | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB - | Barrier_TM_COMMIT + | Barrier_DMB of (a64_barrier_domain * a64_barrier_type) + | Barrier_DSB of (a64_barrier_domain * a64_barrier_type) + | Barrier_ISB of unit + | Barrier_TM_COMMIT of unit (* MIPS barriers *) - | Barrier_MIPS_SYNC + | Barrier_MIPS_SYNC of unit (* RISC-V barriers *) - | Barrier_RISCV_rw_rw - | Barrier_RISCV_r_rw - | Barrier_RISCV_r_r - | Barrier_RISCV_rw_w - | Barrier_RISCV_w_w - | Barrier_RISCV_w_rw - | Barrier_RISCV_rw_r - | Barrier_RISCV_r_w - | Barrier_RISCV_w_r - | Barrier_RISCV_tso - | Barrier_RISCV_i + | Barrier_RISCV_rw_rw of unit + | Barrier_RISCV_r_rw of unit + | Barrier_RISCV_r_r of unit + | Barrier_RISCV_rw_w of unit + | Barrier_RISCV_w_w of unit + | Barrier_RISCV_w_rw of unit + | Barrier_RISCV_rw_r of unit + | Barrier_RISCV_r_w of unit + | Barrier_RISCV_w_r of unit + | Barrier_RISCV_tso of unit + | Barrier_RISCV_i of unit (* X86 *) - | Barrier_x86_MFENCE + | Barrier_x86_MFENCE of unit +let string_a64_barrier_domain = function + | A64_FullShare -> "A64_FullShare" + | A64_InnerShare -> "A64_InnerShare" + | A64_OuterShare -> "A64_OuterShare" + | A64_NonShare -> "A64_NonShare" +end + +instance (Show a64_barrier_domain) + let show = string_a64_barrier_domain +end + +let string_a64_barrier_type = function + | A64_barrier_all -> "A64_barrier_all" + | A64_barrier_LD -> "A64_barrier_LD" + | A64_barrier_ST -> "A64_barrier_ST" +end + +instance (Show a64_barrier_type) + let show = string_a64_barrier_type +end instance (Show barrier_kind) let show = function - | Barrier_Sync -> "Barrier_Sync" - | Barrier_LwSync -> "Barrier_LwSync" - | Barrier_Eieio -> "Barrier_Eieio" - | Barrier_Isync -> "Barrier_Isync" - | Barrier_DMB -> "Barrier_DMB" - | Barrier_DMB_ST -> "Barrier_DMB_ST" - | Barrier_DMB_LD -> "Barrier_DMB_LD" - | Barrier_DSB -> "Barrier_DSB" - | Barrier_DSB_ST -> "Barrier_DSB_ST" - | Barrier_DSB_LD -> "Barrier_DSB_LD" - | Barrier_ISB -> "Barrier_ISB" - | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT" - | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" - | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" - | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" - | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" - | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" - | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" - | Barrier_RISCV_w_rw -> "Barrier_RISCV_w_rw" - | Barrier_RISCV_rw_r -> "Barrier_RISCV_rw_r" - | Barrier_RISCV_r_w -> "Barrier_RISCV_r_w" - | Barrier_RISCV_w_r -> "Barrier_RISCV_w_r" - | Barrier_RISCV_tso -> "Barrier_RISCV_tso" - | Barrier_RISCV_i -> "Barrier_RISCV_i" - | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" + | Barrier_Sync () -> "Barrier_Sync" + | Barrier_LwSync () -> "Barrier_LwSync" + | Barrier_Eieio () -> "Barrier_Eieio" + | Barrier_Isync () -> "Barrier_Isync" + | Barrier_DMB (dom,typ) -> "Barrier_DMB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")" + | Barrier_DSB (dom,typ) -> "Barrier_DSB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")" + | Barrier_ISB () -> "Barrier_ISB" + | Barrier_TM_COMMIT () -> "Barrier_TM_COMMIT" + | Barrier_MIPS_SYNC () -> "Barrier_MIPS_SYNC" + | Barrier_RISCV_rw_rw () -> "Barrier_RISCV_rw_rw" + | Barrier_RISCV_r_rw () -> "Barrier_RISCV_r_rw" + | Barrier_RISCV_r_r () -> "Barrier_RISCV_r_r" + | Barrier_RISCV_rw_w () -> "Barrier_RISCV_rw_w" + | Barrier_RISCV_w_w () -> "Barrier_RISCV_w_w" + | Barrier_RISCV_w_rw () -> "Barrier_RISCV_w_rw" + | Barrier_RISCV_rw_r () -> "Barrier_RISCV_rw_r" + | Barrier_RISCV_r_w () -> "Barrier_RISCV_r_w" + | Barrier_RISCV_w_r () -> "Barrier_RISCV_w_r" + | Barrier_RISCV_tso () -> "Barrier_RISCV_tso" + | Barrier_RISCV_i () -> "Barrier_RISCV_i" + | Barrier_x86_MFENCE () -> "Barrier_x86_MFENCE" end end @@ -304,32 +332,45 @@ instance (EnumerationType write_kind) end end +instance (EnumerationType a64_barrier_domain) + let toNat = function + | A64_FullShare -> 0 + | A64_InnerShare -> 1 + | A64_OuterShare -> 2 + | A64_NonShare -> 3 + end +end + +instance (EnumerationType a64_barrier_type) + let toNat = function + | A64_barrier_all -> 0 + | A64_barrier_LD -> 1 + | A64_barrier_ST -> 2 + end +end + instance (EnumerationType barrier_kind) let toNat = function - | Barrier_Sync -> 0 - | Barrier_LwSync -> 1 - | Barrier_Eieio ->2 - | Barrier_Isync -> 3 - | Barrier_DMB -> 4 - | Barrier_DMB_ST -> 5 - | Barrier_DMB_LD -> 6 - | Barrier_DSB -> 7 - | Barrier_DSB_ST -> 8 - | Barrier_DSB_LD -> 9 - | Barrier_ISB -> 10 - | Barrier_TM_COMMIT -> 11 - | Barrier_MIPS_SYNC -> 12 - | Barrier_RISCV_rw_rw -> 13 - | Barrier_RISCV_r_rw -> 14 - | Barrier_RISCV_r_r -> 15 - | Barrier_RISCV_rw_w -> 16 - | Barrier_RISCV_w_w -> 17 - | Barrier_RISCV_w_rw -> 18 - | Barrier_RISCV_rw_r -> 19 - | Barrier_RISCV_r_w -> 20 - | Barrier_RISCV_w_r -> 21 - | Barrier_RISCV_tso -> 22 - | Barrier_RISCV_i -> 23 - | Barrier_x86_MFENCE -> 24 + | Barrier_Sync () -> 0 + | Barrier_LwSync () -> 1 + | Barrier_Eieio () -> 2 + | Barrier_Isync () -> 3 + | Barrier_DMB (dom,typ) -> 4 + (toNat dom) + (4 * (toNat typ)) (* 4-15 *) + | Barrier_DSB (dom,typ) -> 16 + (toNat dom) + (4 * (toNat typ)) (* 16-27 *) + | Barrier_ISB () -> 28 + | Barrier_TM_COMMIT () -> 29 + | Barrier_MIPS_SYNC () -> 30 + | Barrier_RISCV_rw_rw () -> 31 + | Barrier_RISCV_r_rw () -> 32 + | Barrier_RISCV_r_r () -> 33 + | Barrier_RISCV_rw_w () -> 34 + | Barrier_RISCV_w_w () -> 35 + | Barrier_RISCV_w_rw () -> 36 + | Barrier_RISCV_rw_r () -> 37 + | Barrier_RISCV_r_w () -> 38 + | Barrier_RISCV_w_r () -> 39 + | Barrier_RISCV_tso () -> 40 + | Barrier_RISCV_i () -> 41 + | Barrier_x86_MFENCE () -> 42 end end diff --git a/src/optimize.ml b/src/optimize.ml index 1fc2fbe8..b0d05bef 100644 --- a/src/optimize.ml +++ b/src/optimize.ml @@ -52,43 +52,57 @@ open Ast open Ast_util open Rewriter +let rec split_at_function' id defs acc = + match defs with + | [] -> None + | ([def], env) :: defs when is_fundef id def -> Some (acc, (def, env), defs) + | (def, env) :: defs -> split_at_function' id defs ((def, env) :: acc) + +let split_at_function id defs = + match split_at_function' id defs [] with + | None -> None + | Some (pre_defs, def, post_defs) -> + Some (List.rev pre_defs, def, post_defs) + let recheck (Defs defs) = let defs = Type_check.check_with_envs Type_check.initial_env defs in let rec find_optimizations = function - | ([DEF_pragma ("optimize", pragma, p_l)], env) - :: ([DEF_spec vs as def1], _) - :: ([DEF_fundef fdef as def2], _) - :: defs -> + | ([DEF_pragma ("optimize", pragma, p_l)], env) :: ([DEF_spec vs as def1], _) :: defs -> let id = id_of_val_spec vs in let args = Str.split (Str.regexp " +") (String.trim pragma) in begin match args with | ["unroll"; n]-> let n = int_of_string n in + begin match split_at_function id defs with + | Some (intervening_defs, ((DEF_fundef fdef as def2, _)), defs) -> + let rw_app subst (fn, args) = + if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args) + in + let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in + let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in - let rw_app subst (fn, args) = - if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args) - in - let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in - let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in - - let specs = ref [def1] in - let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in + let specs = ref [def1] in + let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in - for i = 1 to n do - let current_id = append_id id ("_unroll_" ^ string_of_int i) in - let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in - (* Create a valspec for the new unrolled function *) - specs := !specs @ [DEF_spec (rename_valspec current_id vs)]; - (* Then duplicate it's function body and make it call the next unrolled function *) - bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))] - done; + for i = 1 to n do + let current_id = append_id id ("_unroll_" ^ string_of_int i) in + let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in + (* Create a valspec for the new unrolled function *) + specs := !specs @ [DEF_spec (rename_valspec current_id vs)]; + (* Then duplicate it's function body and make it call the next unrolled function *) + bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))] + done; - !specs @ !bodies @ find_optimizations defs + !specs @ List.concat (List.map fst intervening_defs) @ !bodies @ find_optimizations defs + | _ -> + Reporting.warn "Could not find function body for unroll pragma at " p_l ""; + def1 :: find_optimizations defs + end | _ -> Reporting.warn "Unrecognised optimize pragma at" p_l ""; - def1 :: def2 :: find_optimizations defs + def1 :: find_optimizations defs end | (defs, _) :: defs' -> diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 25abfed8..58c71e82 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1625,22 +1625,22 @@ let doc_exp, doc_let = ,_),body'),_) -> body' | _ -> body in - let msuffix, measure_pp = - match measure with - | None -> "", [] - | Some exp -> "T", [expY exp] - in let used_vars_body = find_e_ids body in let varstuple_pp, lambda = make_loop_vars [] varstuple in + let msuffix, measure_pp = + match measure with + | None -> "", [] + | Some exp -> "T", [parens (prefix 2 1 (group lambda) (expN exp))] + in parens ( (prefix 2 1) - ((separate space) (string (combinator ^ csuffix ^ msuffix):: - measure_pp@[varstuple_pp])) - ((prefix 0 1) - (parens (prefix 2 1 (group lambda) (expN cond))) - (parens (prefix 2 1 (group lambda) (expN body)))) + (string (combinator ^ csuffix ^ msuffix)) + (separate (break 1) + (varstuple_pp::measure_pp@ + [parens (prefix 2 1 (group lambda) (expN cond)); + parens (prefix 2 1 (group lambda) (expN body))])) ) end | Id_aux (Id "early_return", _) -> diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index fe241ee7..1367d9eb 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1150,6 +1150,8 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty @@ -1222,6 +1224,8 @@ let doc_typdef_lem env (TD_aux(td, (l, annot))) = match td with (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty diff --git a/src/process_file.ml b/src/process_file.ml index 60261196..8b542445 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -95,10 +95,14 @@ let default_symbols = [ "FEATURE_IMPLICITS"; "FEATURE_CONSTANT_TYPES"; "FEATURE_BITVECTOR_TYPE"; + "FEATURE_UNION_BARRIER"; ] let symbols = ref default_symbols +let have_symbol symbol = + StringSet.mem symbol !symbols + let clear_symbols () = symbols := default_symbols let cond_pragma l defs = diff --git a/src/process_file.mli b/src/process_file.mli index 91cde014..55c7906b 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -53,6 +53,7 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs val clear_symbols : unit -> unit +val have_symbol : string -> bool val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t diff --git a/src/rewrites.ml b/src/rewrites.ml index 3012e49b..87891b6d 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 @@ -3309,7 +3309,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 @@ -3349,8 +3349,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, @@ -4913,13 +4923,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); *) @@ -4955,13 +4965,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); *) @@ -5001,13 +5011,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", []); @@ -5030,12 +5040,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/src/sail.ml b/src/sail.ml index e9b1914d..516b3726 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -70,6 +70,7 @@ let opt_file_arguments = ref ([]:string list) let opt_process_elf : string option ref = ref None let opt_ocaml_generators = ref ([]:string list) let opt_splice = ref ([]:string list) +let opt_have_feature = ref None let set_target name = Arg.Unit (fun _ -> opt_target := Some name) @@ -276,6 +277,9 @@ let options = Arg.align ([ ( "-memo", Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache], " memoize calls to z3, and intermediate compilation results"); + ( "-have_feature", + Arg.String (fun symbol -> opt_have_feature := Some symbol), + " check if a feature symbol is set by default"); ( "-splice", Arg.String (fun s -> opt_splice := s :: !opt_splice), "<filename> add functions from file, replacing existing definitions where necessary"); @@ -410,6 +414,9 @@ let load_files ?check:(check=false) type_envs files = else let ast = Scattered.descatter ast in let ast, type_envs = rewrite_ast_initial type_envs ast in + (* Recheck after descattering so that the internal type environments always + have complete variant types *) + let ast, type_envs = Type_error.check Type_check.initial_env ast in let out_name = match !opt_file_out with | None when parsed = [] -> "out.sail" @@ -545,7 +552,17 @@ let target name out_name ast type_envs = | Some t -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Undefined target: " ^ t)) +let feature_check () = + match !opt_have_feature with + | None -> () + | Some symbol -> + if Process_file.have_symbol symbol then + exit 0 + else + exit 2 + let main () = + feature_check (); if !opt_print_version then print_endline version else diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml index 49739c30..b787fad4 100644 --- a/src/toFromInterp_backend.ml +++ b/src/toFromInterp_backend.ml @@ -141,6 +141,8 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = begin match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty @@ -199,6 +201,8 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) = end | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_domain", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_type", _), _, _) -> empty | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty @@ -296,6 +300,8 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) = begin match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "a64_barrier_domain"),_) -> empty + | Id_aux ((Id "a64_barrier_type"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "trans_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty @@ -349,6 +355,8 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) = end | TD_enum (Id_aux (Id "read_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "write_kind", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_domain", _), _, _) -> empty + | TD_enum (Id_aux (Id "a64_barrier_type", _), _, _) -> empty | TD_enum (Id_aux (Id "barrier_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "trans_kind", _), _, _) -> empty | TD_enum (Id_aux (Id "cache_op_kind", _), _, _) -> empty |