diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 82 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 41 |
3 files changed, 125 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index cbd56240..75e695eb 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -1215,3 +1215,85 @@ let interp_instruction_analysis end in (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind) + +let interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment = + fst (instruction_analysis context endianness analysis_function + reg_info (Just environment) instruction) + + + +val print_and_fail_of_inequal : forall 'a. Show 'a => + (string -> unit) -> + (instruction -> string) -> + (string * 'a) -> (string * 'a) -> unit +let print_and_fail_if_inequal + (print_endline,pp_instruction,instruction) + (name1,xs1) (name2,xs2) = + if xs1 = xs2 then () + else + let () = print_endline (name1^": "^show xs1) in + let () = print_endline (name2^": "^show xs2) in + failwith (name1^" and "^ name2^" inequal for instruction " ^ pp_instruction instruction) + +let interp_compare_analyses + print_endline + pp_instruction + (non_pseudo_registers : set reg_name -> set reg_name) + context + endianness + interp_exhaustive + instruction + nia_reg + ism + environment + analysis_function + reg_info = + let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = + interp_instruction_analysis interp_exhaustive instruction nia_reg ism + environment in + let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) = + (Set.fromList regs_in1, + Set.fromList regs_out1, + Set.fromList regs_feeding_address1, + Set.fromList nias1) in + let (regs_in1S,regs_out1S,regs_feeding_addres1S) = + (non_pseudo_registers regs_in1S, + non_pseudo_registers regs_out1S, + non_pseudo_registers regs_feeding_address1S) in + + let (regs_in2,regs_out2,regs_feeding_address2,nias2,dia2,inst_kind2) = + interp_handwritten_instruction_analysis + context endianness instruction analysis_function reg_info environment in + let (regs_in2S,regs_out2S,regs_feeding_address2S,nias2S) = + (Set.fromList regs_in2, + Set.fromList regs_out2, + Set.fromList regs_feeding_address2, + Set.fromList nias2) in + let (regs_in2S,regs_out2S,regs_feeding_addres2S) = + (non_pseudo_registers regs_in2S, + non_pseudo_registers regs_out2S, + non_pseudo_registers regs_feeding_address2S) in + + let aux = (print_endline,pp_instruction,instruction) in + let () = (print_and_fail_if_inequal aux) + ("regs_in exhaustive",regs_in1S) + ("regs_in hand",regs_in2S) in + let () = (print_and_fail_if_inequal aux) + ("regs_out exhaustive",regs_out1S) + ("regs_out hand",regs_out2S) in + let () = (print_and_fail_if_inequal aux) + ("regs_feeding_address exhaustive",regs_feeding_address1S) + ("regs_feeding_address hand",regs_feeding_address2S) in + let () = (print_and_fail_if_inequal aux) + ("nias exhaustive",nias1S) + ("nias hand",nias2S) in + let () = (print_and_fail_if_inequal aux) + ("dia exhaustive",dia1) + ("dia hand",dia2) in + let () = (print_and_fail_if_inequal aux) + ("inst_kind exhaustive",inst_kind1) + ("inst_kind hand",inst_kind2) in + + (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) + + diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 9d339d25..3d354774 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -345,6 +345,8 @@ let eq_vec v = List.listEqualBy (fun v1 v2 -> match eq (V_tuple [v1; v2]) with V_lit (L_aux L_one _) -> true | _ -> false end) c1s c2s then V_lit (L_aux L_one Unknown) + else if has_unknown v1 || has_unknown v2 + then V_unknown else V_lit (L_aux L_zero Unknown) | (V_unknown, _) -> V_unknown | (_, V_unknown) -> V_unknown diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 76ac1797..3f38f521 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -398,6 +398,18 @@ type write_kind = (* AArch64 writes *) | Write_release | Write_exclusive | Write_exclusive_release +instance (Show write_kind) + let show = function + | Write_plain -> "Write_plain" + | Write_tag -> "Write_tag" + | Write_tag_conditional -> "Write_tag_conditional" + | Write_conditional -> "Write_conditional" + | Write_release -> "Write_release" + | Write_exclusive -> "Write_exclusive" + | Write_exclusive_release -> "Write_exclusive_release" + end +end + type barrier_kind = (* Power barriers *) Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync @@ -407,6 +419,23 @@ type barrier_kind = (* MIPS barriers *) | Barrier_MIPS_SYNC +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_MIPS_SYNC -> "Barrier_MIPS_SYNC" + end +end + type instruction_kind = | IK_barrier of barrier_kind | IK_mem_read of read_kind @@ -419,6 +448,18 @@ they just have particular nias (and will be IK_simple *) | IK_simple +instance (Show instruction_kind) + let show = function + | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind) + | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) + | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) + | IK_cond_branch -> "IK_cond_branch" + | IK_simple -> "IK_simple" + end +end + + + let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with | (Read_plain, Read_plain) -> EQ |