diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-28 13:32:21 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-28 13:32:21 +0000 |
| commit | befbc76f89f3d8abc8da17caf91ea4a87ec96eeb (patch) | |
| tree | d84d76258ca9b2505713552bb62be8c40714787b | |
| parent | 26c166e279ec05837b6b3b5db80a7ef3c520db32 (diff) | |
checklink: first import of Valentin Robert's validator for asm and link
cparser: renamed Errors to Cerrors; removed packing into Cparser.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
41 files changed, 5565 insertions, 79 deletions
@@ -27,7 +27,11 @@ OCB_OPTIONS=\ -j 2 \ -no-hygiene \ -no-links \ - -I extraction $(INCLUDES) + -I extraction -I cparser $(INCLUDES) +OCB_OPTIONS_CHECKLINK=\ + $(OCB_OPTIONS) \ + -I checklink \ + -use-ocamlfind VPATH=$(DIRS) GPATH=$(DIRS) @@ -114,7 +118,15 @@ ccomp.byte: driver/Configuration.ml runtime: $(MAKE) -C runtime -.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte cinterp cinterp.byte runtime +cchecklink: driver/Configuration.ml + $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \ + && rm -f cchecklink && $(SLN) _build/checklink/Validator.native cchecklink + +cchecklink.byte: driver/Configuration.ml + $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \ + && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte + +.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte all: $(MAKE) proof @@ -152,7 +164,7 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod -w $*.v -driver/Configuration.ml: Makefile.config +driver/Configuration.ml: Makefile.config VERSION (echo let stdlib_path = "\"$(LIBDIR)\""; \ echo let prepro = "\"$(CPREPRO)\""; \ echo let asm = "\"$(CASM)\""; \ @@ -160,7 +172,9 @@ driver/Configuration.ml: Makefile.config echo let arch = "\"$(ARCH)\""; \ echo let variant = "\"$(VARIANT)\""; \ echo let system = "\"$(SYSTEM)\""; \ - echo let need_stdlib_wrapper = $(NEED_STDLIB_WRAPPER)) \ + echo let need_stdlib_wrapper = $(NEED_STDLIB_WRAPPER); \ + version=`cat VERSION`; \ + echo let version = "\"$$version\"") \ > driver/Configuration.ml depend: $(FILES) @@ -1,2 +1,3 @@ -<cparser/*.cmx>: for-pack(Cparser) <driver/Driver.*{byte,native}>: use_unix,use_str,use_Cparser +<checklink/*.ml>: pkg_bitstring +<checklink/Validator.*{byte,native}>: pkg_unix,pkg_str,pkg_bitstring,use_Cparser diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index 6c01a36..ea3c7df 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -15,7 +15,6 @@ (* Processor-dependent builtin C functions *) -open Cparser open C let builtins = { diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6386445..508c414 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -15,12 +15,9 @@ open Printf -module CompcertErrors = Errors (* avoid shadowing by Cparser.Errors *) - -open Cparser -open Cparser.C -open Cparser.Env -open Cparser.Builtins +open C +open Env +open Builtins open Camlcoq open AST @@ -222,12 +219,12 @@ let make_builtin_memcpy args = | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) -> let sz1 = match Initializers.constval sz with - | CompcertErrors.OK(Vint n) -> camlint_of_coqint n + | Errors.OK(Vint n) -> camlint_of_coqint n | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; 0l in let al1 = match Initializers.constval al with - | CompcertErrors.OK(Vint n) -> camlint_of_coqint n + | Errors.OK(Vint n) -> camlint_of_coqint n | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; 0l in let fn = register_inlined_memcpy sz1 al1 in @@ -249,7 +246,7 @@ let convertAttr a = List.mem AVolatile a let convertIkind = function | C.IBool -> (Unsigned, IBool) - | C.IChar -> ((if (!Cparser.Machine.config).Cparser.Machine.char_signed + | C.IChar -> ((if (!Machine.config).Machine.char_signed then Signed else Unsigned), I8) | C.ISChar -> (Signed, I8) | C.IUChar -> (Unsigned, I8) @@ -725,9 +722,9 @@ let convertFundecl env (sto, id, ty, optinit) = let string_of_errmsg msg = let string_of_err = function - | CompcertErrors.MSG s -> camlstring_of_coqstring s - | CompcertErrors.CTX i -> extern_atom i - | CompcertErrors.CTXL i -> "" (* should not happen *) + | Errors.MSG s -> camlstring_of_coqstring s + | Errors.CTX i -> extern_atom i + | Errors.CTXL i -> "" (* should not happen *) in String.concat "" (List.map string_of_err msg) let rec convertInit env init = @@ -749,8 +746,8 @@ and convertInitList env il = let convertInitializer env ty i = match Initializers.transl_init (convertTyp env ty) (convertInit env i) with - | CompcertErrors.OK init -> init - | CompcertErrors.Error msg -> + | Errors.OK init -> init + | Errors.Error msg -> error (sprintf "Initializer is not a compile-time constant (%s)" (string_of_errmsg msg)); [] diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index 4b4c0f1..63bd3f9 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -17,7 +17,6 @@ open Printf open Camlcoq -open Cparser (* #pragma section *) diff --git a/cfrontend/Cparser.mllib b/cfrontend/Cparser.mllib deleted file mode 100644 index e942137..0000000 --- a/cfrontend/Cparser.mllib +++ /dev/null @@ -1 +0,0 @@ -Cparser diff --git a/cfrontend/Cparser.mlpack b/cfrontend/Cparser.mlpack deleted file mode 100644 index b59e30f..0000000 --- a/cfrontend/Cparser.mlpack +++ /dev/null @@ -1,23 +0,0 @@ -cparser/C -cparser/Errors -cparser/Cabs -cparser/Cabshelper -cparser/Parse_aux -cparser/Parser -cparser/Lexer -cparser/Machine -cparser/Env -cparser/Cprint -cparser/Cutil -cparser/Ceval -cparser/Cleanup -cparser/Builtins -cparser/Elab -cparser/Rename -cparser/Transform -cparser/Unblock -cparser/StructReturn -cparser/Bitfields -cparser/PackedStructs -cparser/Parse - diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml new file mode 100644 index 0000000..8f78a07 --- /dev/null +++ b/checklink/Asm_printers.ml @@ -0,0 +1,230 @@ +open Asm +open AST +open BinInt +open BinPos +open Library + +let rec int_of_pos = function + | Coq_xH -> 1 + | Coq_xO q -> 2 * int_of_pos q + | Coq_xI q -> 2 * int_of_pos q + 1 + +let string_of_pos p = string_of_int (int_of_pos p) + +let string_of_coq_Z = function + | Z0 -> "0" + | Zpos p -> string_of_pos p + | Zneg p -> "-" ^ string_of_pos p + +let string_of_ident = string_of_pos +let string_of_label = string_of_pos +let string_of_iint = string_of_coq_Z + +let string_of_ireg = function +| GPR0 -> "GPR0" +| GPR1 -> "GPR1" +| GPR2 -> "GPR2" +| GPR3 -> "GPR3" +| GPR4 -> "GPR4" +| GPR5 -> "GPR5" +| GPR6 -> "GPR6" +| GPR7 -> "GPR7" +| GPR8 -> "GPR8" +| GPR9 -> "GPR9" +| GPR10 -> "GPR10" +| GPR11 -> "GPR11" +| GPR12 -> "GPR12" +| GPR13 -> "GPR13" +| GPR14 -> "GPR14" +| GPR15 -> "GPR15" +| GPR16 -> "GPR16" +| GPR17 -> "GPR17" +| GPR18 -> "GPR18" +| GPR19 -> "GPR19" +| GPR20 -> "GPR20" +| GPR21 -> "GPR21" +| GPR22 -> "GPR22" +| GPR23 -> "GPR23" +| GPR24 -> "GPR24" +| GPR25 -> "GPR25" +| GPR26 -> "GPR26" +| GPR27 -> "GPR27" +| GPR28 -> "GPR28" +| GPR29 -> "GPR29" +| GPR30 -> "GPR30" +| GPR31 -> "GPR31" + +let string_of_freg = function +| FPR0 -> "FPR0" +| FPR1 -> "FPR1" +| FPR2 -> "FPR2" +| FPR3 -> "FPR3" +| FPR4 -> "FPR4" +| FPR5 -> "FPR5" +| FPR6 -> "FPR6" +| FPR7 -> "FPR7" +| FPR8 -> "FPR8" +| FPR9 -> "FPR9" +| FPR10 -> "FPR10" +| FPR11 -> "FPR11" +| FPR12 -> "FPR12" +| FPR13 -> "FPR13" +| FPR14 -> "FPR14" +| FPR15 -> "FPR15" +| FPR16 -> "FPR16" +| FPR17 -> "FPR17" +| FPR18 -> "FPR18" +| FPR19 -> "FPR19" +| FPR20 -> "FPR20" +| FPR21 -> "FPR21" +| FPR22 -> "FPR22" +| FPR23 -> "FPR23" +| FPR24 -> "FPR24" +| FPR25 -> "FPR25" +| FPR26 -> "FPR26" +| FPR27 -> "FPR27" +| FPR28 -> "FPR28" +| FPR29 -> "FPR29" +| FPR30 -> "FPR30" +| FPR31 -> "FPR31" + +let string_of_preg = function +| IR (i0) -> "IR(" ^ string_of_ireg i0 ^ ")" +| FR (f0) -> "FR(" ^ string_of_freg f0 ^ ")" +| PC -> "PC" +| LR -> "LR" +| CTR -> "CTR" +| CARRY -> "CARRY" +| CR0_0 -> "CR0_0" +| CR0_1 -> "CR0_1" +| CR0_2 -> "CR0_2" +| CR0_3 -> "CR0_3" + +let string_of_external_function e = + match e with + | EF_builtin(name, sg) -> "EF_builtin" + | EF_vload(chunk) -> "EF_vload" + | EF_vstore(chunk) -> "EF_vstore" + | EF_vload_global(_, _, _) -> "EF_vload_global" + | EF_vstore_global(_, _, _) -> "EF_vstore_global" + | EF_malloc -> "EF_malloc" + | EF_free -> "EF_free" + | EF_memcpy(sz, al) -> + "EF_memcpy(" ^ string_of_z sz ^ ", " ^ string_of_z al ^ ")" + | EF_annot(_, _) -> "EF_annot" + | EF_annot_val(txt, targ) -> "EF_annot_val" + | _ -> "UNKNOWN" + +let string_of_constant = function +| Cint (i0) -> "Cint(" ^ string_of_iint i0 ^ ")" +| Csymbol_low (i0, i1) -> "Csymbol_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" +| Csymbol_high (i0, i1) -> "Csymbol_high(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" +| Csymbol_sda (i0, i1) -> "Csymbol_sda(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" + +let string_of_crbit = function +| CRbit_0 -> "CRbit_0" +| CRbit_1 -> "CRbit_1" +| CRbit_2 -> "CRbit_2" +| CRbit_3 -> "CRbit_3" + +let string_of_memory_chunk mc = "MEMORY_CHUNK" + +let string_of_annot_param = function +| APreg (p0)-> "APreg(" ^ string_of_preg p0 ^ ")" +| APstack(m0, c1)-> "APstack(" ^ string_of_memory_chunk m0 ^ ", " ^ string_of_coq_Z c1 ^ ")" + +let string_of_instruction = function +| Padd (i0, i1, i2) -> "Padd(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Padde (i0, i1, i2) -> "Padde(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Paddi (i0, i1, c2) -> "Paddi(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Paddic (i0, i1, c2) -> "Paddic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Paddis (i0, i1, c2) -> "Paddis(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Paddze (i0, i1) -> "Paddze(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pallocframe(c0, i1) -> "Pallocframe(" ^ string_of_coq_Z c0 ^ ", " ^ string_of_iint i1 ^ ")" +| Pand_ (i0, i1, i2) -> "Pand_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pandc (i0, i1, i2) -> "Pandc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pandi_ (i0, i1, c2) -> "Pandi_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Pandis_ (i0, i1, c2) -> "Pandis_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Pb (l0) -> "Pb(" ^ string_of_label l0 ^ ")" +| Pbctr -> "Pbctr" +| Pbctrl -> "Pbctrl" +| Pbf (c0, l1) -> "Pbf(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" +| Pbl (i0) -> "Pbl(" ^ string_of_ident i0 ^ ")" +| Pbs (i0) -> "Pbs(" ^ string_of_ident i0 ^ ")" +| Pblr -> "Pblr" +| Pbt (c0, l1) -> "Pbt(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" +| Pbtbl (i0, l1) -> "Pbtbl(" ^ string_of_ireg i0 ^ ", " ^ string_of_list string_of_label ", " l1 ^ ")" +| Pcmplw (i0, i1) -> "Pcmplw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pcmplwi (i0, c1) -> "Pcmplwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" +| Pcmpw (i0, i1) -> "Pcmpw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pcmpwi (i0, c1) -> "Pcmpwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" +| Pcror (c0, c1, c2) -> "Pcror(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" +| Pdivw (i0, i1, i2) -> "Pdivw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pdivwu (i0, i1, i2) -> "Pdivwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Peqv (i0, i1, i2) -> "Peqv(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pextsb (i0, i1) -> "Pextsb(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pextsh (i0, i1) -> "Pextsh(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pfreeframe(c0, i1) -> "Pfreeframe(" ^ string_of_coq_Z c0 ^ ", " ^ string_of_iint i1 ^ ")" +| Pfabs (f0, f1) -> "Pfabs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfadd (f0, f1, f2) -> "Pfadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" +| Pfcmpu (f0, f1) -> "Pfcmpu(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfcti (i0, f1) -> "Pfcti(" ^ string_of_ireg i0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfdiv (f0, f1, f2) -> "Pfdiv(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" +| Pfmake (f0, i1, i2) -> "Pfmake(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pfmr (f0, f1) -> "Pfmr(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfmul (f0, f1, f2) -> "Pfmul(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" +| Pfneg (f0, f1) -> "Pfneg(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfrsp (f0, f1) -> "Pfrsp(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfsub (f0, f1, f2) -> "Pfsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" +| Plbz (i0, c1, i2) -> "Plbz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plbzx (i0, i1, i2) -> "Plbzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plfd (f0, c1, i2) -> "Plfd(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plfdx (f0, i1, i2) -> "Plfdx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plfs (f0, c1, i2) -> "Plfs(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plfsx (f0, i1, i2) -> "Plfsx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plha (i0, c1, i2) -> "Plha(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plhax (i0, i1, i2) -> "Plhax(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plhz (i0, c1, i2) -> "Plhz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plhzx (i0, i1, i2) -> "Plhzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plfi (f0, f1) -> "Plfi(" ^ string_of_freg f0 ^ ", " ^ string_of_float f1 ^ ")" +| Plwz (i0, c1, i2) -> "Plwz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plwzx (i0, i1, i2) -> "Plwzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pmfcrbit (i0, c1) -> "Pmfcrbit(" ^ string_of_ireg i0 ^ ", " ^ string_of_crbit c1 ^ ")" +| Pmflr (i0) -> "Pmflr(" ^ string_of_ireg i0 ^ ")" +| Pmr (i0, i1) -> "Pmr(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pmtctr (i0) -> "Pmtctr(" ^ string_of_ireg i0 ^ ")" +| Pmtlr (i0) -> "Pmtlr(" ^ string_of_ireg i0 ^ ")" +| Pmulli (i0, i1, c2) -> "Pmulli(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Pmullw (i0, i1, i2) -> "Pmullw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pnand (i0, i1, i2) -> "Pnand(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pnor (i0, i1, i2) -> "Pnor(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Por (i0, i1, i2) -> "Por(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Porc (i0, i1, i2) -> "Porc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pori (i0, i1, c2) -> "Pori(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Poris (i0, i1, c2) -> "Poris(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Prlwinm (i0, i1, i2, i3) -> "Prlwinm(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_iint i2 ^ ", " ^ string_of_iint i3 ^ ")" +| Prlwimi (i0, i1, i2, i3) -> "Prlwimi(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_iint i2 ^ ", " ^ string_of_iint i3 ^ ")" +| Pslw (i0, i1, i2) -> "Pslw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Psraw (i0, i1, i2) -> "Psraw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Psrawi (i0, i1, i2) -> "Psrawi(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_iint i2 ^ ")" +| Psrw (i0, i1, i2) -> "Psrw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstb (i0, c1, i2) -> "Pstb(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstbx (i0, i1, i2) -> "Pstbx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstfd (f0, c1, i2) -> "Pstfd(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstfdx (f0, i1, i2) -> "Pstfdx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstfs (f0, c1, i2) -> "Pstfs(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstfsx (f0, i1, i2) -> "Pstfsx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Psth (i0, c1, i2) -> "Psth(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Psthx (i0, i1, i2) -> "Psthx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstw (i0, c1, i2) -> "Pstw(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstwx (i0, i1, i2) -> "Pstwx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Psubfc (i0, i1, i2) -> "Psubfc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Psubfe (i0, i1, i2) -> "Psubfe(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Psubfic (i0, i1, c2) -> "Psubfic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Pxor (i0, i1, i2) -> "Pxor(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pxori (i0, i1, c2) -> "Pxori(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Pxoris (i0, i1, c2) -> "Pxoris(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Plabel (l0) -> "Plabel(" ^ string_of_label l0 ^ ")" +| Pbuiltin (e0, p1, p2) -> "Pbuiltin(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_preg ", " p1 ^ ", " ^ string_of_preg p2 ^ ")" +| Pannot (e0, a1) -> "Pannot(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_annot_param ", " a1 ^ ")" + diff --git a/checklink/Bitstring_utils.ml b/checklink/Bitstring_utils.ml new file mode 100644 index 0000000..2253b63 --- /dev/null +++ b/checklink/Bitstring_utils.ml @@ -0,0 +1,25 @@ +(** Note that a bitstring is a triple (string * int * int), where the string + contains the contents (the last char is filled up with zeros if necessary), + the firts int gives the first bit to consider, and the second int gives the + bit length of the considered bitstring. +*) +type bitstring = Bitstring.bitstring + +(** Checks whether a given number of bits of a bitstring are zeroed. The + bitstring may be longer. + @param size number of bits to check +*) +let rec is_zeros (bs: bitstring) (size: int): bool = + size = 0 || + if size >= 64 + then ( + bitmatch bs with + | { 0L : 64 : int ; rest : -1 : bitstring } -> + is_zeros rest (size - 64) + | { _ } -> false + ) + else ( + bitmatch bs with + | { 0L : size : int } -> true + | { _ } -> false + ) diff --git a/checklink/Check.ml b/checklink/Check.ml new file mode 100644 index 0000000..a40fe59 --- /dev/null +++ b/checklink/Check.ml @@ -0,0 +1,3080 @@ +open Asm +open Asm_printers +open AST +open BinInt +open BinPos +open Bitstring_utils +open C2C +open ELF_parsers +open ELF_printers +open ELF_types +open ELF_utils +open Frameworks +open Lens +open Library +open PPC_parsers +open PPC_printers +open PPC_types +open PPC_utils +open Sections + +(** Enables immediate printing of log information to stdout. + Warning: will print out everything before backtracking. +*) +let debug = ref false + +(** Whether to dump the ELF map *) +let dump_elfmap = ref false + +(* + module ELFCoverage = MakeRangeSet(MeasurableUInt32) + module SymCoverage = MakeRangeSet(MeasurableInt) +*) + +(** CompCert Asm *) +type ccode = Asm.instruction list + +(** Adds a log entry into the framework. *) +let add_log (entry: log_entry) (efw: e_framework): e_framework = + if !debug then print_endline (string_of_log_entry entry); + {efw with log = entry :: efw.log} + +(** [flag] should have only one bit set. *) +let is_set_flag (flag: int32) (bitset: int32): bool = + Int32.logand bitset flag <> 0l + +(** Checks that [atom]'s binding matches [sym]'s. *) +let check_st_bind atom (sym: elf32_sym): s_framework -> s_framework = + let static = atom.a_storage = C.Storage_static || atom.a_inline in + match static, sym.st_bind with + | true, STB_LOCAL -> id + | false, STB_GLOBAL -> id + | _ -> ( + sf_ef ^%= + add_log (ERROR( + "Symbol: " ^ sym.st_name ^ " has a wrong binding (local vs. global)" + )) + ) + +(** Taken from CompCert *) +let name_of_section_Linux: + section_name -> string + = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else ".bss" + | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_const -> ".rodata" + | Section_small_const -> ".sdata2" + | Section_string -> ".rodata" + | Section_literal -> ".rodata" (* should have been .rodata.cst8, but ld script + merges it with .rodata *) + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> s + +(** Taken from CompCert *) +let name_of_section_Diab: + section_name -> string + = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else ".bss" + | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_const -> ".text" + | Section_small_const -> ".sdata2" + | Section_string -> ".text" + | Section_literal -> ".text" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> s + +(** Taken from CompCert *) +let name_of_section: + section_name -> string + = + begin match Configuration.system with + | "macosx" -> assert false + | "linux" -> name_of_section_Linux + | "diab" -> name_of_section_Diab + | _ -> assert false + end + +(** Compares a CompCert section name with an ELF section name. *) +let match_sections_name + (c_section: section_name) (e_name: string) (sfw: s_framework): + s_framework + = + let c_name = name_of_section c_section in + if e_name = c_name || + (c_name = ".bss" && e_name = ".sbss") (* this is complicated! *) + then sfw + else ( + sfw + >>> (sf_ef ^%= + (add_log (ERROR( + "Section should be " ^ c_name ^ " instead of " ^ e_name))) + ) + ) + +(** Checks the symbol table entry of the function symbol number [sym_ndx], + according to CompCert's [ident]. +*) +let check_fun_symtab + (ident: ident) (sym_ndx: int) (sfw: s_framework): + s_framework + = + let elf = sfw.ef.elf in + let symtab_sndx = from_some (section_ndx_by_name elf ".symtab") in + let symtab_ent_start = + Int32.(add + elf.e_shdra.(symtab_sndx).sh_offset + (int_int32 (16 * sym_ndx))) in + let sym = sfw.ef.elf.e_symtab.(sym_ndx) in + let atom = Hashtbl.find sfw.atoms ident in + let section = + match atom.a_sections with + | [t; _; _] -> t + | _ -> Section_text + in + sfw + >>> check_st_bind atom sym + >>> ( + if sym.st_type = STT_FUNC + then id + else (sf_ef ^%= + add_log (ERROR("Symbol should have type STT_FUNC")) + ) + ) + >>> ( + if sym.st_other = 0 + then id + else (sf_ef ^%= + add_log (ERROR("Symbol should have st_other set to 0")) + ) + ) + >>> match_sections_name section elf.e_shdra.(sym.st_shndx).sh_name + >>> (sf_ef ^%= + add_range symtab_ent_start 16l 4 (Symtab_function(sym)) + ) + +(** Checks that the offset [ofs] is well aligned with regards to [al], expressed + in bytes. *) +let is_well_aligned (ofs: int32) (al: int): bool = + al = 0 || Int32.rem ofs (int_int32 al) = 0l + +(** Adds a function symbol to the set of covered symbols. *) +let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework = + let elf = ffw.sf.ef.elf in + let sym = elf.e_symtab.(ndx) in + let sym_sndx = sym.st_shndx in + let sym_size = sym.st_size in + let sym_shdr = elf.e_shdra.(sym_sndx) in + let sym_vaddr = sym.st_value in + let sym_ofs_local = Int32.sub sym_vaddr sym_shdr.sh_addr in + let sxn_ofs = sym_shdr.sh_offset in + let sym_begin = Int32.add sxn_ofs sym_ofs_local in + let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in + let align = + match atom.a_alignment with + | Some(a) -> a + | None -> 0 + in + ffw + (*>>> ((ff_ef |-- chkd_syms) ^%= (SymCoverage.add ndx))*) + >>> (ff_ef ^%= + (add_range sym_begin sym_size align (Function_symbol(sym))) + ) + >>> (ff_sf ^%= + if not (is_well_aligned sym_ofs_local align) + then ( + sf_ef ^%= + add_log (ERROR( + "Symbol not correctly aligned in the ELF file" + )) + ) + else id + ) + >>> (ff_sf ^%= check_fun_symtab ffw.this_ident ndx) + +(** Taken from CompCert *) +let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$" + +(** Tries to refine the mapping for key [k] in [ident_to_sym_ndx] so that it is + mapped to [vaddr]. Fails if no symbol in [k]'s mapping has that virtual + address, unless the symbol is a stub from CompCert. Otherwise, it filters + out all symbols whose virtual address does not match [vaddr]. +*) +let idmap_unify + (k: positive) (vaddr: int32) (sfw: s_framework): s_framework on_success = + try ( + let id_ndxes = PosMap.find k sfw.ident_to_sym_ndx in + match List.filter + (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_value = vaddr) + id_ndxes with + | [] -> + if Str.string_match + re_variadic_stub (Hashtbl.find sfw.ident_to_name k) 0 + then (* this points to a stub *) + try ( + let v = PosMap.find k sfw.stub_ident_to_vaddr in + if vaddr = v + then OK(sfw) + else ERR( + "Incoherent constraints for stub: " ^ + Hashtbl.find sfw.ident_to_name k + ) + ) + with Not_found -> + OK( + sfw + >>> (stub_ident_to_vaddr ^%= PosMap.add k vaddr) + ) + else (* not a stub, so this is a real error *) + ERR( + "Incoherent constraints for ident " ^ + Hashtbl.find sfw.ident_to_name k ^ + " with value " ^ + string_of_int32 vaddr ^ + " and candidates [" ^ + (string_of_list + (fun ndx -> + string_of_int32 + sfw.ef.elf.e_symtab.(ndx).st_value + ) + ", " id_ndxes + ) ^ + "]" + ) + | ndxes -> + if id_ndxes = ndxes + then OK(sfw) + else OK((ident_to_sym_ndx ^%= (PosMap.add k ndxes)) sfw) + ) + with + | Not_found -> + ERR( + "Missing ident: " ^ Hashtbl.find sfw.ident_to_name k ^ + " should be at vaddr: " ^ string_of_int32 vaddr + ) + +(** Checks whether the label [k] points to [v] in [label_to_vaddr]. If it points + to another virtual address, this returns an ERR. If it points to nothing, + the mapping [k] -> [v] is added. Thus, the first time a label is + encountered determines the expected virtual address of its destination. + Subsequent references to the label will have to conform. +*) +let lblmap_unify (k: label) (v: int32) (ffw: f_framework) + : f_framework on_success = + try ( + let v' = PosMap.find k ffw.label_to_vaddr in + if v = v' + then OK ffw + else ( + ERR( + "Incoherent constraints for label " ^ + string_of_positive k ^ " with values " ^ + string_of_int32 v ^ " and " ^ string_of_int32 v' + ) + ) + ) + with + | Not_found -> + OK { + ffw with + label_to_vaddr = PosMap.add k v ffw.label_to_vaddr + } + +let ireg_arr: ireg array = + [| + GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11; + GPR12; GPR13; GPR14; GPR15; GPR16; GPR17; GPR18; GPR19; GPR20; GPR21; GPR22; + GPR23; GPR24; GPR25; GPR26; GPR27; GPR28; GPR29; GPR30; GPR31 + |] + +let freg_arr: freg array = + [| + FPR0; FPR1; FPR2; FPR3; FPR4; FPR5; FPR6; FPR7; FPR8; FPR9; FPR10; FPR11; + FPR12; FPR13; FPR14; FPR15; FPR16; FPR17; FPR18; FPR19; FPR20; FPR21; FPR22; + FPR23; FPR24; FPR25; FPR26; FPR27; FPR28; FPR29; FPR30; FPR31 + |] + +let crbit_arr: crbit array = + [| + CRbit_0; CRbit_1; CRbit_2; CRbit_3 + |] + +(** Generic condition checker *) +let check (cond: bool) (msg: string) (ffw: f_framework): f_framework = + if cond + then ffw + else ffw >>> ff_ef ^%= add_log (ERROR(msg)) + +let check_eq (msg: string) (a: 'a) (b: 'a): f_framework -> f_framework = + check (a = b) msg + +let match_bools: bool -> bool -> f_framework -> f_framework = + check_eq "match_bools" +let match_ints: int -> int -> f_framework -> f_framework = + check_eq "match_ints" +let match_int32s: int32 -> int32 -> f_framework -> f_framework = + check_eq "match_int32s" +let match_floats: float -> float -> f_framework -> f_framework = + check_eq "match_floats" +let match_crbits cb eb = check_eq "match_crbits" cb (crbit_arr.(eb)) +let match_iregs cr er = check_eq "match_iregs" cr (ireg_arr.(er)) +let match_fregs cr er = check_eq "match_fregs" cr (freg_arr.(er)) + +let name_of_ndx (efw: e_framework) (ndx: int): string = + let st = efw.elf.e_symtab.(ndx) in + st.st_name ^ " at address " ^ (string_of_int32 st.st_value) + +(** Filters the lower 16 bits of an int32. *) +let low: int32 -> int32 = Int32.logand 0x0000ffffl + +(** high_exts x is equal to: + + - the 16 high bits of x if its lower 16 bits form a positive 16 bit integer + + - the 16 high bits of x plus one otherwise + + This is so that: x == high_exts x + exts (low x) +*) +let high_exts (x: int32): int32 = Int32.( + if logand x 0x00008000l = 0l + then logand x 0xffff0000l + else add 0x00010000l (logand x 0xffff0000l) +) + +(** Matches a CompCert constant against an [int32]. *) +let match_csts (cc: constant) (ec: int32) (ffw: f_framework): f_framework = + let sfw = ffw |. ff_sf in + let efw = ffw |. ff_ef in + match cc with + | Cint (i) -> + check_eq "match_csts Cint" ec (z_int32_lax i) ffw + | Csymbol_low (ident, i) -> + let candidates = + try PosMap.find ident sfw.ident_to_sym_ndx + with Not_found -> [] + in + let vaddrs = + List.filter + (fun ndx -> + let ident_vaddr = efw.elf.e_symtab.(ndx).st_value in + Int32.(low (add ident_vaddr (z_int32_lax i)) = low ec) + ) + candidates + in + begin match vaddrs with + | [] -> + let sym_names = List.map (name_of_ndx efw) candidates in + (ff_ef ^%= + (add_log (ERROR("Csymbol_low " ^ string_of_list id ", " sym_names))) + ) ffw + | _ -> + if candidates = vaddrs + then ffw + else ( + ffw + >>> ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) + ) + end + | Csymbol_high (ident, i) -> + (* In this case, ec is 0x0000XXXX standing for XXXX0000 *) + let candidates = + try PosMap.find ident sfw.ident_to_sym_ndx + with Not_found -> [] + in + let vaddrs = + List.filter + (fun ndx -> + let ident_vaddr = efw.elf.e_symtab.(ndx).st_value in + Int32.(high_exts (add ident_vaddr (z_int32_lax i)) + = shift_left ec 16)) + candidates in + begin match vaddrs with + | [] -> + let sym_names = + List.map (name_of_ndx efw) candidates in + (ff_ef ^%= + (add_log (ERROR("Csymbol_high " ^ string_of_list id ", " sym_names))) + ) ffw + | _ -> + if candidates = vaddrs + then ffw + else ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) ffw + end + | Csymbol_sda (ident, i) -> + ffw + >>> ff_ef ^%= (add_log (ERROR("TODO"))) + +let match_z_int32 (cz: coq_Z) (ei: int32) = + check_eq "match_z_int32" (z_int32 cz) ei + +let match_z_int (cz: coq_Z) (ei: int) = + check_eq "match_z_int" (z_int32 cz) (int_int32 ei) + +(* [m] is interpreted as a bitmask, and checked against [ei]. *) +let match_mask (m: coq_Z) (ei: int32) = + check_eq + ("match_mask " ^ string_of_int32 (z_int32_lax m) ^ " and " ^ + string_of_int32 ei) + (z_int32_lax m) ei + +(** Checks that the special register referred to in [spr] is [r]. *) +let match_spr (str: string) (r: int) (spr: bitstring) + : f_framework -> f_framework = + bitmatch spr with + | { v:5; 0:5 } when v = r -> id + | { _ } -> ff_ef ^%= (add_log (ERROR(str))) + +let match_xer = match_spr "match_xer" 1 +let match_lr = match_spr "match_lr" 8 +let match_ctr = match_spr "match_ctr" 9 + +(** Read a n-bits bitstring as a signed integer, two's complement representation + (n < 32). +*) +let exts (bs: bitstring): int32 = + let signif_bits = Bitstring.bitstring_length bs - 1 in + bitmatch bs with + | { sign : 1 ; + rest : signif_bits : int } -> + Int64.( + to_int32 ( + if sign + then logor rest (lognot (sub (shift_left one signif_bits) one)) + else rest + ) + ) + +(** Creates a bitmask from bits mb to me, according to the specification in + "4.2.1.4 Integer Rotate and Shift Instructions" of the PowerPC manual. +*) +let rec bitmask mb me = + assert (0 <= mb); assert (0 <= me); assert (mb < 32); assert (me < 32); + if (mb, me) = (0, 31) + then -1l (* this case does not compute correctly otherwise *) + else if mb <= me + (* 0 ... mb ... me ... 31 + 0 0 0 1 1 1 1 1 0 0 0 + *) + then Int32.(shift_left + (sub (shift_left 1l (me - mb + 1)) 1l) + (31 - me) + ) + (* + 0 ... me ... mb ... 31 + 1 1 1 1 0 0 0 1 1 1 1 + == + 1 1 1 1 1 1 1 1 1 1 1 -1l + - + 0 0 0 0 1 1 1 0 0 0 0 bitmask (me + 1) (mb - 1) + *) + else if mb = me + 1 + then (-1l) + else Int32.(sub (-1l) (bitmask (me + 1) (mb - 1))) + +(** Checks that a label did not occur twice in the same function. *) +let check_label_unicity ffw = + let rec check_label_unicity_aux l ffw = + match l with + | [] -> ffw + | h::t -> + ffw + >>> ( + if List.mem h t + then ( + ff_ef ^%= + (add_log (ERROR("Duplicate label: " ^ string_of_positive h))) + ) + else id + ) + >>> check_label_unicity_aux t + in + check_label_unicity_aux ffw.label_list ffw + +(** Checks that all the labels that have been referred to in instructions + actually appear in the code. *) +let check_label_existence ffw = + PosMap.fold + (fun k v -> + if List.mem k ffw.label_list + then id + else ( + ff_ef ^%= + (add_log (ERROR("Missing label: " ^ string_of_positive k))) + ) + ) + ffw.label_to_vaddr + ffw + +(** Matches the segment at virtual address [vaddr] with the jumptable expected + from label list [lbllist]. Then checks whether the matched chunk of the code + had the expected [size]. +*) +let rec match_jmptbl lbllist vaddr size ffw = + let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in + let jmptbl_section = + match atom.a_sections with + | [_; _; j] -> j + | _ -> Section_jumptable + in + let rec match_jmptbl_aux lbllist bs ffw = + match lbllist with + | [] -> OK ffw + | lbl :: lbls -> ( + bitmatch bs with + | { vaddr : 32 : int; + rest : -1 : bitstring } -> + ffw + >>> lblmap_unify lbl vaddr + >>= match_jmptbl_aux lbls rest + | { _ } -> + print_endline "Ill-formed jump table"; + ERR("Ill-formed jump table") + ) + in + let elf = ffw.sf.ef.elf in + let cur_sym_ndx = elf.e_symtab.(ffw.this_sym_ndx).st_shndx in + let bs = bitstring_at_vaddr elf cur_sym_ndx vaddr size in + match section_at_vaddr elf vaddr with + | None -> ERR("Jumptable's virtual address is out of any section") + | Some(sndx) -> + let ofs = physical_offset_of_vaddr elf sndx vaddr in + ffw + >>> (ff_sf ^%= + match_sections_name jmptbl_section elf.e_shdra.(sndx).sh_name + ) + >>> match_jmptbl_aux lbllist bs + >>? (ff_ef ^%= + add_range ofs (int_int32 (size / 8)) 0 Jumptable) + +(** Matches [ecode] agains the expected code for a small memory copy + pseudo-instruction. Returns a triple containing the updated framework, + the remaining ELF code, and the updated program counter. +*) +let match_memcpy_small ecode pc sz al src dst (fw: f_framework) + : (f_framework * ecode * int32) option = + let rec match_memcpy_small_aux ofs sz ecode pc (fw: f_framework) = + let ofs32 = int_int32 ofs in + if sz >= 8 && al >= 4 + then ( + match ecode with + | LFD (frD0, rA0, d0) :: + STFD(frS1, rA1, d1) :: es -> + fw + >>> match_fregs FPR0 frD0 + >>> match_iregs src rA0 + >>> match_int32s ofs32 (exts d0) + >>> match_fregs FPR0 frS1 + >>> match_iregs dst rA1 + >>> match_int32s ofs32 (exts d1) + >>> match_memcpy_small_aux (ofs + 8) (sz - 8) es (Int32.add 8l pc) + | _ -> None + ) + else if sz >= 4 + then ( + match ecode with + | LWZ(rD0, rA0, d0) :: + STW(rS1, rA1, d1) :: es -> + fw + >>> match_iregs GPR0 rD0 + >>> match_iregs src rA0 + >>> match_int32s ofs32 (exts d0) + >>> match_iregs GPR0 rS1 + >>> match_iregs dst rA1 + >>> match_int32s ofs32 (exts d0) + >>> match_memcpy_small_aux (ofs + 4) (sz - 4) es (Int32.add 8l pc) + | _ -> None + ) + else if sz >= 2 + then ( + match ecode with + | LHZ(rD0, rA0, d0) :: + STH(rS1, rA1, d1) :: es -> + fw + >>> match_iregs GPR0 rD0 + >>> match_iregs src rA0 + >>> match_int32s ofs32 (exts d0) + >>> match_iregs GPR0 rS1 + >>> match_iregs dst rA1 + >>> match_int32s ofs32 (exts d0) + >>> match_memcpy_small_aux (ofs + 2) (sz - 2) es (Int32.add 8l pc) + | _ -> None + ) + else if sz >= 1 + then ( + match ecode with + | LBZ(rD0, rA0, d0) :: + STB(rS1, rA1, d1) :: es -> + fw + >>> match_iregs GPR0 rD0 + >>> match_iregs src rA0 + >>> match_int32s ofs32 (exts d0) + >>> match_iregs GPR0 rS1 + >>> match_iregs dst rA1 + >>> match_int32s ofs32 (exts d0) + >>> match_memcpy_small_aux (ofs + 1) (sz - 1) es (Int32.add 8l pc) + | _ -> None + ) + else Some(fw, ecode, pc) + in match_memcpy_small_aux 0 sz ecode pc fw + +(** Matches [ecode] agains the expected code for a big memory copy + pseudo-instruction. Returns a triple containing the updated framework, + the remaining ELF code, and the updated program counter. +*) +let match_memcpy_big ecode pc sz al src dst fw + : (f_framework * ecode * int32) option = + match ecode with + | ADDI (rD0, rA0, simm0) :: (* pc *) + MTSPR(rS1, spr1) :: + ADDI (rD2, rA2, simm2) :: + ADDI (rD3, rA3, simm3) :: + LWZU (rD4, rA4, d4) :: (* pc + 16 <- *) + STWU (rS5, rA5, d5) :: (* | *) + BCx (bo6, bi6, bd6, aa6, lk6) :: (* pc + 24 -- *) + es -> + let sz' = int_int32 (sz / 4) in + let (s, d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in + let target_vaddr = Int32.(add 16l pc) in + let dest_vaddr = Int32.(add (add 24l pc) (mul 4l (exts bd6))) in + fw + >>> match_iregs GPR0 rD0 + >>> match_iregs GPR0 rA0 + >>> match_int32s sz' (exts simm0) + >>> match_iregs GPR0 rS1 + >>> match_ctr spr1 + >>> match_iregs s rD2 + >>> match_iregs src rA2 + >>> match_int32s (-4l) (exts simm2) + >>> match_iregs d rD3 + >>> match_iregs dst rA3 + >>> match_int32s (-4l) (exts simm3) + >>> match_iregs GPR0 rD4 + >>> match_iregs s rA4 + >>> match_int32s 4l (exts d4) + >>> match_iregs GPR0 rS5 + >>> match_iregs d rA5 + >>> match_int32s 4l (exts d5) + >>> ( + bitmatch bo6 with + | { 16:5:int } -> id + | { _ } -> + ff_ef ^%= add_log (ERROR("bitmatch bo")) + ) + >>> match_ints bi6 0 + >>> match_int32s dest_vaddr target_vaddr + >>> match_bools false aa6 + >>> match_bools false lk6 + >>> (fun fw -> + match sz land 3 with + | 1 -> + begin match es with + | LBZ(rD0, rA0, d0) :: + STB(rS1, rA1, d1) :: es -> + fw + >>> match_iregs GPR0 rD0 + >>> match_iregs s rA0 + >>> match_int32s 4l (exts d0) + >>> match_iregs GPR0 rS1 + >>> match_iregs d rA1 + >>> match_int32s 4l (exts d1) + >>> (fun fw -> Some(fw, es, Int32.add 36l pc)) + | _ -> None + end + | 2 -> + begin match es with + | LHZ(rD0, rA0, d0) :: + STH(rS1, rA1, d1) :: es -> + fw + >>> match_iregs GPR0 rD0 + >>> match_iregs s rA0 + >>> match_int32s 4l (exts d0) + >>> match_iregs GPR0 rS1 + >>> match_iregs d rA1 + >>> match_int32s 4l (exts d1) + >>> (fun fw -> Some(fw, es , Int32.add 36l pc)) + | _ -> None + end + | 3 -> + begin match es with + | LHZ(rD0, rA0, d0) :: + STH(rS1, rA1, d1) :: + LBZ(rD2, rA2, d2) :: + STB(rS3, rA3, d3) :: es -> + fw + >>> match_iregs GPR0 rD0 + >>> match_iregs s rA0 + >>> match_int32s 4l (exts d0) + >>> match_iregs GPR0 rS1 + >>> match_iregs d rA1 + >>> match_int32s 4l (exts d1) + >>> match_iregs GPR0 rD2 + >>> match_iregs s rA2 + >>> match_int32s 6l (exts d2) + >>> match_iregs GPR0 rS3 + >>> match_iregs d rA3 + >>> match_int32s 6l (exts d3) + >>> (fun fw -> Some(fw, es, Int32.add 44l pc)) + | _ -> None + end + | _ -> Some(fw, es, Int32.add 28l pc) + ) + | _ -> None + +(** Compares a whole CompCert function code against an ELF code, starting at + program counter [pc]. +*) +let rec compare_code ccode ecode pc fw: f_framework on_success = + (* + PosMap.iter (fun k v -> print_endline (string_of_positive k ^ " -> " ^ + string_of_int32 v)) i.ident_to_sym_ndx; + *) + let error = ERR("Non-matching instructions") in + match ccode, ecode with + | [], [] -> OK(fw) + | [], _ | _, [] -> ERR("Codes have different lengths") + | c::cs, e::es -> + let recur_simpl = compare_code cs es (Int32.add 4l pc) in + (*let curr_instr = " [" ^ string_of_int32 pc ^ "] " ^ + string_of_instruction c ^ " - " ^ string_of_instr e in + let fw = (ff_ef ^%= add_log (LOG(curr_instr))) fw in*) + match c with + | Padd(rd, r1, r2) -> + begin match ecode with + | ADDx(rD, rA, rB, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Padde(rd, r1, r2) -> + begin match ecode with + | ADDEx(rD, rA, rB, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Paddi(rd, r1, cst) -> + begin match ecode with + | ADDI(rD, rA, simm) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_csts cst (exts simm) + >>> recur_simpl + | _ -> error + end + | Paddic(rd, r1, cst) -> + begin match ecode with + | ADDIC(rD, rA, simm) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_csts cst (exts simm) + >>> recur_simpl + | _ -> error + end + | Paddis(rd, r1, cst) -> + begin match ecode with + | ADDIS(rD, rA, simm) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_csts cst (int_int32 simm) + >>> recur_simpl + | _ -> error + end + | Paddze(rd, r1) -> + begin match ecode with + | ADDZEx(rD, rA, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pallocframe(sz, ofs) -> + begin match ecode with + | STWU(rS, rA, d) :: es -> + fw + >>> match_iregs GPR1 rS + >>> match_iregs GPR1 rA + >>> match_z_int32 sz (Int32.neg (exts d)) + >>> match_z_int32 ofs 0l + >>> recur_simpl + | ADDIS (rD0, rA0, simm0) :: + ORI (rS1, rA1, uimm1) :: + STWUX (rS2, rA2, rB2) :: es -> + fw + >>> ff_ef ^%= + add_log (ERROR("TODO")) + >>> compare_code cs es (Int32.add 12l pc) + | _ -> error + end + | Pandc(rd, r1, r2) -> + begin match ecode with + | ANDCx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pand_(rd, r1, r2) -> + begin match ecode with + | ANDx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools true rc + >>> recur_simpl + | _ -> error + end + | Pandis_(rd, r1, cst) -> + begin match ecode with + | ANDIS_(rS, rA, uimm) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_csts cst (int_int32 uimm) + >>> recur_simpl + | _ -> error + end + | Pandi_(rd, r1, cst) -> + begin match ecode with + | ANDI_(rS, rA, uimm) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_csts cst (int_int32 uimm) + >>> recur_simpl + | _ -> error + end + | Pannot(ef, args) -> + fw + >>> compare_code cs ecode pc + | Pb(lbl) -> + begin match ecode with + | Bx(li, aa, lk) :: es -> + let lblvaddr = Int32.(add pc (mul 4l (exts li))) in + fw + >>> match_bools false aa + >>> match_bools false lk + >>> lblmap_unify lbl lblvaddr + >>= recur_simpl + | _ -> error + end + | Pbctr -> + begin match ecode with + | BCCTRx(bo, bi, lk) :: es -> + fw + >>> (ff_ef ^%= + bitmatch bo with + | { true:1; false:1; true:1; false:1; false:1 } -> id + | { _ } -> add_log (ERROR("bitmatch")) + ) + >>> match_ints 0 bi + >>> match_bools false lk + >>> recur_simpl + | _ -> error + end + | Pbctrl -> + begin match ecode with + | BCCTRx(bo, bi, lk) :: es -> + fw + >>> (ff_ef ^%= + bitmatch bo with + | { true:1; false:1; true:1; false:1; false:1 } -> id + | { _ } -> add_log (ERROR("bitmatch")) + ) + >>> match_ints 0 bi + >>> match_bools true lk + >>> recur_simpl + | _ -> error + end + | Pbf(bit, lbl) -> + begin match ecode with + | BCx(bo, bi, bd, aa, lk) :: es -> + let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in + fw + >>> (ff_ef ^%= + bitmatch bo with + | { false:1; false:1; true:1; false:1; false:1 } -> id + | { _ } -> add_log (ERROR("bitmatch")) + ) + >>> match_crbits bit bi + >>> lblmap_unify lbl lblvaddr + >>? match_bools false aa + >>? match_bools false lk + >>= recur_simpl + | _ -> error + end + | Pbl(ident) -> + begin match ecode with + | Bx(li, aa, lk) :: es -> + let dest = Int32.(add pc (mul 4l (exts li))) in + fw + >>> match_bools false aa + >>> match_bools true lk + >>> (ff_sf ^%=? idmap_unify ident dest) + >>= recur_simpl + | _ -> error + end + | Pblr -> + begin match ecode with + | BCLRx(bo, bi, lk) :: es -> + fw + >>> (ff_ef ^%= + bitmatch bo with + | { true:1; false:1; true:1; false:1; false:1 } -> id + | { _ } -> add_log (ERROR("bitmatch")) + ) + >>> match_ints 0 bi + >>> match_bools false lk + >>> recur_simpl + | _ -> error + end + | Pbs(ident) -> + begin match ecode with + | Bx(li, aa, lk) :: es -> + let dest = Int32.(add pc (mul 4l (exts li))) in + fw + >>> match_bools false aa + >>> match_bools false lk + >>> (ff_sf ^%=? idmap_unify ident dest) + >>= recur_simpl + | _ -> error + end + | Pbt(bit, lbl) -> + begin match ecode with + | BCx(bo, bi, bd, aa, lk) :: es -> + let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in + fw + >>> (ff_ef ^%= + bitmatch bo with + | { false:1; true:1; true:1; false:1; false:1 } -> id + | { _ } -> add_log (ERROR("bitmatch")) + ) + >>> match_crbits bit bi + >>> lblmap_unify lbl lblvaddr + >>? match_bools false aa + >>? match_bools false lk + >>= recur_simpl + | _ -> error + end + | Pbtbl(reg, table) -> + begin match ecode with + | ADDIS (rD0, rA0, simm0) :: + LWZ (rD1, rA1, d1) :: + MTSPR (rS2, spr2) :: + BCCTRx(bo3, bi3, rc3) :: es -> + let tblvaddr = Int32.( + add (shift_left (int_int32 simm0) 16) (exts d1) + ) in + let tblsize = (32 * List.length table) in + fw + >>> match_iregs GPR12 rD0 + >>> match_iregs reg rA0 + >>> match_iregs GPR12 rD1 + >>> match_iregs GPR12 rA1 + >>> match_iregs GPR12 rS2 + >>> match_ctr spr2 + >>> (ff_ef ^%= + bitmatch bo3 with + | { true:1; false:1; true:1; false:1; false:1 } -> id + | { _ } -> add_log (ERROR("bitmatch")) + ) + >>> match_ints 0 bi3 + >>> match_bools false rc3 + >>> match_jmptbl table tblvaddr tblsize + >>= compare_code cs es (Int32.add 16l pc) + | _ -> error + end + | Pbuiltin(ef, args, res) -> + begin match ef with + | EF_builtin(name, sg) -> + begin match Hashtbl.find + (fw |. ff_sf).ident_to_name name, args, res with + | "__builtin_mulhw", [IR a1; IR a2], IR res -> + begin match ecode with + | MULHWx(rD, rA, rB, rc) :: es -> + fw + >>> match_iregs res rD + >>> match_iregs a1 rA + >>> match_iregs a2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_mulhwu", [IR a1; IR a2], IR res -> + begin match ecode with + | MULHWUx(rD, rA, rB, rc) :: es -> + fw + >>> match_iregs res rD + >>> match_iregs a1 rA + >>> match_iregs a2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_cntlz", [IR a1], IR res -> + begin match ecode with + | CNTLZWx(rS, rA, rc) :: es -> + fw + >>> match_iregs a1 rS + >>> match_iregs res rA + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_bswap", [IR a1], IR res -> + begin match ecode with + | STWU (rS0, rA0, d0) :: + LWBRX(rD1, rA1, rB1) :: + ADDI (rD2, rA2, simm2) :: es -> + fw + >>> match_iregs a1 rS0 + >>> match_iregs GPR1 rA0 + >>> match_int32s (-8l) (exts d0) + >>> match_iregs res rD1 + >>> match_iregs GPR0 rA1 + >>> match_iregs GPR1 rB1 + >>> match_iregs GPR1 rD2 + >>> match_iregs GPR1 rA2 + >>> match_int32s 8l (exts simm2) + >>> compare_code cs es (Int32.add 12l pc) + | _ -> error + end + | "__builtin_fmadd", [FR a1; FR a2; FR a3], FR res -> + begin match ecode with + | FMADDx(frD, frA, frB, frC, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frA + >>> match_fregs a3 frB + >>> match_fregs a2 frC + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_fmsub", [FR a1; FR a2; FR a3], FR res -> + begin match ecode with + | FMSUBx(frD, frA, frB, frC, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frA + >>> match_fregs a3 frB + >>> match_fregs a2 frC + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_fnmadd", [FR a1; FR a2; FR a3], FR res -> + begin match ecode with + | FNMADDx(frD, frA, frB, frC, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frA + >>> match_fregs a3 frB + >>> match_fregs a2 frC + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_fnmsub", [FR a1; FR a2; FR a3], FR res -> + begin match ecode with + | FNMSUBx(frD, frA, frB, frC, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frA + >>> match_fregs a3 frB + >>> match_fregs a2 frC + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_fabs", [FR a1], FR res -> + begin match ecode with + | FABSx(frD, frB, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_fsqrt", [FR a1], FR res -> + begin match ecode with + | FSQRTx(frD, frB, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_frsqrte", [FR a1], FR res -> + begin match ecode with + | FRSQRTEx(frD, frB, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_fres", [FR a1], FR res -> + begin match ecode with + | FRESx(frD, frB, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_fsel", [FR a1; FR a2; FR a3], FR res -> + begin match ecode with + | FSELx(frD, frA, frB, frC, rc) :: es -> + fw + >>> match_fregs res frD + >>> match_fregs a1 frA + >>> match_fregs a3 frB + >>> match_fregs a2 frC + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | "__builtin_read16_reversed", [IR a1], IR res -> + begin match ecode with + | LHBRX(rD, rA, rB):: es -> + fw + >>> match_iregs res rD + >>> match_iregs GPR0 rA + >>> match_iregs a1 rB + >>> recur_simpl + | _ -> error + end + | "__builtin_read32_reversed", [IR a1], IR res -> + begin match ecode with + | LWBRX(rD, rA, rB) :: es -> + fw + >>> match_iregs res rD + >>> match_iregs GPR0 rA + >>> match_iregs a1 rB + >>> recur_simpl + | _ -> error + end + | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + begin match ecode with + | STHBRX(rS, rA, rB) :: es -> + fw + >>> match_iregs a2 rS + >>> match_iregs GPR0 rA + >>> match_iregs a1 rB + >>> recur_simpl + | _ -> error + end + | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + begin match ecode with + | STWBRX(rS, rA, rB) :: es -> + fw + >>> match_iregs a2 rS + >>> match_iregs GPR0 rA + >>> match_iregs a1 rB + >>> recur_simpl + | _ -> error + end + | "__builtin_eieio", [], _ -> + begin match ecode with + | EIEIO :: es -> + fw + >>> recur_simpl + | _ -> error + end + | "__builtin_sync", [], _ -> + begin match ecode with + | SYNC :: es -> + fw + >>> recur_simpl + | _ -> error + end + | "__builtin_isync", [], _ -> + begin match ecode with + | ISYNC :: es -> + fw + >>> recur_simpl + | _ -> error + end + | "__builtin_trap", [], _ -> + begin match ecode with + | TW(tO, rA, rB) :: es -> + fw + >>> (ff_ef ^%= + bitmatch tO with + | { 31 : 5 : int } -> id + | { _ } -> add_log (ERROR("bitmatch")) + ) + >>> match_iregs GPR0 rA + >>> match_iregs GPR0 rB + >>> recur_simpl + | _ -> error + end + | _ -> error + end + | EF_vload(chunk) -> + begin match args with + | [IR addr] -> + fw + >>> check_builtin_vload_common + cs ecode pc chunk addr (Cint Integers.Int.zero) res + | _ -> assert false + end + | EF_vstore(chunk) -> + begin match args with + | [IR addr; src] -> + fw + >>> check_builtin_vstore_common + cs ecode pc chunk addr (Cint Integers.Int.zero) src + | _ -> assert false + end + | EF_vload_global(chunk, ident, ofs) -> + begin match ecode with + | ADDIS(rD, rA, simm) :: es -> + let high = Csymbol_high(ident, ofs) in + fw + >>> match_iregs GPR11 rD + >>> match_iregs GPR0 rA + >>> match_csts high (int_int32 simm) + >>> check_builtin_vload_common + cs es (Int32.add pc 4l) chunk GPR11 + (Csymbol_low(ident, ofs)) res + | _ -> error + end + | EF_vstore_global(chunk, ident, ofs) -> + begin match args with + | [src] -> + begin match ecode with + | ADDIS(rD, rA, simm) :: es -> + let tmp = + if src = IR GPR11 + then GPR12 + else GPR11 + in + let high = Csymbol_high(ident, ofs) in + fw + >>> match_iregs tmp rD + >>> match_iregs GPR0 rA + >>> match_csts high (int_int32 simm) + >>> check_builtin_vstore_common + cs es (Int32.add pc 4l) chunk tmp + (Csymbol_low(ident, ofs)) src + | _ -> error + end + | _ -> assert false + end + | EF_memcpy(sz, al) -> + let sz = z_int sz in + let al = z_int al in + begin match args with + | [IR dst; IR src] -> + if sz <= 64 + then ( + match match_memcpy_small ecode pc sz al src dst fw with + | None -> error + | Some(fw, es, pc) -> compare_code cs es pc fw + ) + else ( + match match_memcpy_big ecode pc sz al src dst fw with + | None -> error + | Some(fw, es, pc) -> compare_code cs es pc fw + ) + | _ -> error + end + | EF_annot_val(text, targ) -> + begin match args, res with + | IR src :: _, IR dst -> + if dst <> src + then ( + match ecode with + | ORx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs src rS + >>> match_iregs dst rA + >>> match_iregs src rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + ) + else compare_code cs ecode pc fw + | FR src :: _, FR dst -> + if dst <> src + then ( + match ecode with + | FMRx(frD, frB, rc) :: es -> + fw + >>> match_fregs dst frD + >>> match_fregs src frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + ) + else compare_code cs ecode pc fw + | _ -> error + end + | EF_annot(_, _) -> assert false + | EF_external(_, _) -> assert false + | EF_free -> assert false + | EF_malloc -> assert false + end + | Pcmplw(r1, r2) -> + begin match ecode with + | CMPL(crfD, l, rA, rB) :: es -> + fw + >>> match_crbits CRbit_0 crfD + >>> match_bools false l + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Pcmplwi(r1, cst) -> + begin match ecode with + | CMPLI(crfD, l, rA, uimm) :: es -> + fw + >>> match_iregs r1 rA + >>> match_csts cst (int_int32 uimm) + >>> match_crbits CRbit_0 crfD + >>> match_bools false l + >>> recur_simpl + | _ -> error + end + | Pcmpw(r1, r2) -> + begin match ecode with + | CMP(crfD, l, rA, rB) :: es -> + fw + >>> match_ints crfD 0 + >>> match_bools l false + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Pcmpwi(r1, cst) -> + begin match ecode with + | CMPI(crfD, l, rA, simm) :: es -> + fw + >>> match_ints crfD 0 + >>> match_bools false l + >>> match_iregs r1 rA + >>> match_csts cst (exts simm) + >>> recur_simpl + | _ -> error + end + | Pcror(bd, b1, b2) -> + begin match ecode with + | CROR(crbD, crbA, crbB) :: es -> + fw + >>> match_crbits bd crbD + >>> match_crbits b1 crbA + >>> match_crbits b2 crbB + >>> recur_simpl + | _ -> error + end + | Pdivw(rd, r1, r2) -> + begin match ecode with + | DIVWx(rD, rA, rB, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pdivwu(rd, r1, r2) -> + begin match ecode with + | DIVWUx(rD, rA, rB, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Peqv(rd, r1, r2) -> + begin match ecode with + | EQVx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pextsb(rd, r1) -> + begin match ecode with + | EXTSBx(rS, rA, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pextsh(rd, r1) -> + begin match ecode with + | EXTSHx(rS, rA, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfabs(rd, r1) -> + begin match ecode with + | FABSx(frD, frB, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfadd(rd, r1, r2) -> + begin match ecode with + | FADDx(frD, frA, frB, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frA + >>> match_fregs r2 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfcmpu(r1, r2) -> + begin match ecode with + | FCMPU(crfD, frA, frB) :: es -> + fw + >>> match_crbits CRbit_0 crfD + >>> match_fregs r1 frA + >>> match_fregs r2 frB + >>> recur_simpl + | _ -> error + end + | Pfcti(rd, r1) -> + begin match ecode with + | FCTIWZx(frD0, frB0, rc0) :: + STFDU (frS1, rA1, d1) :: + LWZ (rD2, rA2, d2) :: + ADDI (rD3, rA3, simm3) :: es -> + fw + >>> match_fregs FPR13 frD0 + >>> match_fregs r1 frB0 + >>> match_bools false rc0 + >>> match_fregs FPR13 frS1 + >>> match_iregs GPR1 rA1 + >>> match_int32s (-8l) (exts d1) + >>> match_iregs rd rD2 + >>> match_iregs GPR1 rA2 + >>> match_int32s 4l (exts d2) + >>> match_iregs GPR1 rD3 + >>> match_iregs GPR1 rA3 + >>> match_int32s 8l (exts simm3) + >>> compare_code cs es (Int32.add 16l pc) + | _ -> error + end + | Pfdiv(rd, r1, r2) -> + begin match ecode with + | FDIVx(frD, frA, frB, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frA + >>> match_fregs r2 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfmake(rd, r1, r2) -> + begin match ecode with + | STWU (rS0, rA0, d0) :: + STW (rS1, rA1, d1) :: + LFD (frD2, rA2, d2) :: + ADDI (rD3, rA3, simm3) :: es -> + fw + >>> match_iregs r1 rS0 + >>> match_iregs GPR1 rA0 + >>> match_int32s (-8l) (exts d0) + >>> match_iregs r2 rS1 + >>> match_iregs GPR1 rA1 + >>> match_int32s 4l (exts d1) + >>> match_fregs rd frD2 + >>> match_iregs GPR1 rA2 + >>> match_int32s 0l (exts d2) + >>> match_iregs GPR1 rD3 + >>> match_iregs GPR1 rA3 + >>> match_int32s 8l (exts simm3) + >>> compare_code cs es (Int32.add 16l pc) + | _ -> error + end + | Pfmr(rd, r1) -> + begin match ecode with + | FMRx(frD, frB, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfmul(rd, r1, r2) -> + begin match ecode with + | FMULx(frD, frA, frC, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frA + >>> match_fregs r2 frC + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfneg (rd, r1) -> + begin match ecode with + | FNEGx(frD, frB, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfreeframe(sz, ofs) -> + begin match ecode with + | LWZ(rD, rA, d) :: es -> + fw + >>> match_iregs GPR1 rD + >>> match_iregs GPR1 rA + >>> match_z_int32 ofs (Int32.neg (exts d)) + >>> recur_simpl + | _ -> error + end + | Pfrsp(rd, r1) -> + begin match ecode with + | FRSPx(frD, frB, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pfsub(rd, r1, r2) -> + begin match ecode with + | FSUBx(frD, frA, frB, rc) :: es -> + fw + >>> match_fregs rd frD + >>> match_fregs r1 frA + >>> match_fregs r2 frB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Plabel(lbl) -> + fw + >>> lblmap_unify lbl pc + >>? (fun fw -> {fw with label_list = lbl :: fw.label_list}) + >>= compare_code cs ecode pc + | Plbz(rd, cst, r1) -> + begin match ecode with + | LBZ(rD, rA, d) :: es -> + fw + >>> match_iregs rd rD + >>> match_csts cst (exts d) + >>> match_iregs r1 rA + >>> recur_simpl + | _ -> error + end + | Plbzx(rd, r1, r2) -> + begin match ecode with + | LBZX(rD, rA, rB) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Plfd(rd, cst, r1) -> + begin match ecode with + | LFD(frD, rA, d) :: es -> + fw + >>> match_fregs rd frD + >>> match_csts cst (exts d) + >>> match_iregs r1 rA + >>> recur_simpl + | _ -> error + end + | Plfdx(rd, r1, r2) -> + begin match ecode with + | LFDX(frD, rA, rB) :: es -> + fw + >>> match_fregs rd frD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Plfs(rd, cst, r1) -> + begin match ecode with + | LFS(frD, rA, d) :: es -> + fw + >>> match_fregs rd frD + >>> match_csts cst (exts d) + >>> match_iregs r1 rA + >>> recur_simpl + | _ -> error + end + | Plfsx(rd, r1, r2) -> + begin match ecode with + | LFSX(frD, rA, rB) :: es -> + fw + >>> match_fregs rd frD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Plha(rd, cst, r1) -> + begin match ecode with + | LHA(rD, rA, d) :: es -> + fw + >>> match_iregs rd rD + >>> match_csts cst (exts d) + >>> match_iregs r1 rA + >>> recur_simpl + | _ -> error + end + | Plhax(rd, r1, r2) -> + begin match ecode with + | LHAX(rD, rA, rB) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Plhzx(rd, r1, r2) -> + begin match ecode with + | LHZX(rD, rA, rB) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Plfi(r1, c) -> + begin match ecode with + | ADDIS(rD0, rA0, simm0) :: + LFD (frD1, rA1, d1) :: es -> + let vaddr = Int32.( + add (shift_left (int_int32 simm0) 16) (exts d1) + ) in + if Int32.rem vaddr 8l <> 0l + then ERR("Float constants should be 8-byte aligned") + else + let elf = fw.sf.ef.elf in + let atom = Hashtbl.find fw.sf.atoms fw.this_ident in + let literal_section = + begin match atom.a_sections with + | [_; l; _] -> l + | _ -> Section_literal + end + in + begin match section_at_vaddr elf vaddr with + | None -> + ERR("Float literal's virtual address out of any section") + | Some(sndx) -> + let section_bitstring = bitstring_at_vaddr elf sndx in + let f = ( + bitmatch (section_bitstring vaddr 64) with + | { f : 64 : int } -> Int64.float_of_bits f + ) in + let ofs = physical_offset_of_vaddr elf sndx vaddr in + fw + >>> (ff_sf ^%= + match_sections_name + literal_section + elf.e_shdra.(sndx).sh_name + ) + >>> match_iregs GPR12 rD0 + >>> match_iregs GPR0 rA0 + >>> match_fregs r1 frD1 + >>> match_floats c f + >>> (ff_ef ^%= add_range ofs 8l 8 (Float_literal(f))) + >>> match_iregs GPR12 rA1 + >>> compare_code cs es (Int32.add 8l pc) + end + | _ -> error + end + | Plhz(rd, cst, r1) -> + begin match ecode with + | LHZ(rD, rA, d) :: es -> + fw + >>> match_iregs rd rD + >>> match_csts cst (exts d) + >>> match_iregs r1 rA + >>> recur_simpl + | _ -> error + end + | Plwz(rd, cst, r1) -> + begin match ecode with + | LWZ(rD, rA, d) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_csts cst (exts d) + >>> recur_simpl + | _ -> error + end + | Plwzx(rd, r1, r2) -> + begin match ecode with + | LWZX(rD, rA, rB) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Pmfcrbit(rd, bit) -> + begin match ecode with + | MFCR (rD0) :: + RLWINMx(rS1, rA1, sh1, mb1, me1, rc1) :: es -> + fw + >>> match_iregs rd rD0 + >>> match_iregs rd rS1 + >>> match_iregs rd rA1 + >>> match_crbits bit (sh1 - 1) + >>> match_ints 31 mb1 + >>> match_ints 31 me1 + >>> match_bools false rc1 + >>> compare_code cs es (Int32.add 8l pc) + | _ -> error + end + | Pmflr(r) -> + begin match ecode with + | MFSPR(rD, spr) :: es -> + fw + >>> match_iregs r rD + >>> match_lr spr + >>> recur_simpl + | _ -> error + end + | Pmr(rd, r1) -> + begin match ecode with + | ORx(rS, rA, rB, rc) :: es when (rB = rS) -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pmtctr(r1) -> + begin match ecode with + | MTSPR(rS, spr) :: es -> + fw + >>> match_iregs r1 rS + >>> match_ctr spr + >>> recur_simpl + | _ -> error + end + | Pmtlr(r1) -> + begin match ecode with + | MTSPR(rS, spr) :: es -> + fw + >>> match_iregs r1 rS + >>> match_lr spr + >>> recur_simpl + | _ -> error + end + | Pmulli(rd, r1, cst) -> + begin match ecode with + | MULLI(rD, rA, simm) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_csts cst (exts simm) + >>> recur_simpl + | _ -> error + end + | Pmullw(rd, r1, r2) -> + begin match ecode with + | MULLWx(rD, rA, rB, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pnand(rd, r1, r2) -> + begin match ecode with + | NANDx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pnor(rd, r1, r2) -> + begin match ecode with + | NORx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Por(rd, r1, r2) -> + begin match ecode with + | ORx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Porc(rd, r1, r2) -> + begin match ecode with + | ORCx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pori(rd, r1, cst) -> + begin match ecode with + | ORI(rS, rA, uimm) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_csts cst (int_int32 uimm) + >>> recur_simpl + | _ -> error + end + | Poris(rd, r1, cst) -> + begin match ecode with + | ORIS(rS, rA, uimm) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_csts cst (int_int32 uimm) + >>> recur_simpl + | _ -> error + end + | Prlwimi(rd, r1, amount, mask) -> + begin match ecode with + | RLWIMIx(rS, rA, sh, mb, me, rc) :: es -> + fw + >>> match_iregs r1 rS + >>> match_iregs rd rA + >>> match_z_int amount sh + >>> match_mask mask (bitmask mb me) + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Prlwinm(rd, r1, amount, mask) -> + begin match ecode with + | RLWINMx(rS, rA, sh, mb, me, rc) :: es -> + fw + >>> match_iregs r1 rS + >>> match_iregs rd rA + >>> match_z_int amount sh + >>> match_mask mask (bitmask mb me) + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pslw(rd, r1, r2) -> + begin match ecode with + | SLWx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Psraw(rd, r1, r2) -> + begin match ecode with + | SRAWx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Psrawi(rd, r1, n) -> + begin match ecode with + | SRAWIx(rS, rA, sh, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_z_int n sh + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Psrw(rd, r1, r2) -> + begin match ecode with + | SRWx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pstb(rd, cst, r1) -> + begin match ecode with + | STB(rS, rA, d) :: es -> + fw + >>> match_iregs rd rS + >>> match_iregs r1 rA + >>> match_csts cst (exts d) + >>> recur_simpl + | _ -> error + end + | Pstbx(rd, r1, r2) -> + begin match ecode with + | STBX(rS, rA, rB) :: es -> + fw + >>> match_iregs rd rS + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Pstfd(rd, cst, r1) -> + begin match ecode with + | STFD(frS, rA, d) :: es -> + fw + >>> match_fregs rd frS + >>> match_iregs r1 rA + >>> match_csts cst (exts d) + >>> recur_simpl + | _ -> error + end + | Pstfdx(rd, r1, r2) -> + begin match ecode with + | STFDX(frS, rA, rB) :: es -> + fw + >>> match_fregs rd frS + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Pstfs(rd, cst, r1) -> + begin match ecode with + | FRSPx(frD0, frB0, rc0) :: + STFS (frS1, rA1, d1) :: es -> + fw + >>> match_fregs FPR13 frD0 + >>> match_fregs rd frB0 + >>> match_bools false rc0 + >>> match_fregs FPR13 frS1 + >>> match_iregs r1 rA1 + >>> match_csts cst (exts d1) + >>> compare_code cs es (Int32.add 8l pc) + | _ -> error + end + | Pstfsx(rd, r1, r2) -> + begin match ecode with + | FRSPx(frD0, frB0, rc0) :: + STFSX(frS1, rA1, rB1) :: es -> + fw + >>> match_fregs FPR13 frD0 + >>> match_fregs rd frB0 + >>> match_bools false rc0 + >>> match_fregs FPR13 frS1 + >>> match_iregs r1 rA1 + >>> match_iregs r2 rB1 + >>> compare_code cs es (Int32.add 8l pc) + | _ -> error + end + | Psth(rd, cst, r1) -> + begin match ecode with + | STH(rS, rA, d) :: es -> + fw + >>> match_iregs rd rS + >>> match_iregs r1 rA + >>> match_csts cst (exts d) + >>> recur_simpl + | _ -> error + end + | Psthx(rd, r1, r2) -> + begin match ecode with + | STHX(rS, rA, rB) :: es -> + fw + >>> match_iregs rd rS + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Pstw(rd, cst, r1) -> + begin match ecode with + | STW(rS, rA, d) :: es -> + fw + >>> match_iregs rd rS + >>> match_iregs r1 rA + >>> match_csts cst (exts d) + >>> recur_simpl + | _ -> error + end + | Pstwx(rd, r1, r2) -> + begin match ecode with + | STWX(rS, rA, rB) :: es -> + fw + >>> match_iregs rd rS + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> recur_simpl + | _ -> error + end + | Psubfc(rd, r1, r2) -> + begin match ecode with + | SUBFCx(rD, rA, rB, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Psubfe(rd, r1, r2) -> + begin match ecode with + | SUBFEx(rD, rA, rB, oe, rc) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_iregs r2 rB + >>> match_bools false oe + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Psubfic(rd, r1, cst) -> + begin match ecode with + | SUBFIC(rD, rA, simm) :: es -> + fw + >>> match_iregs rd rD + >>> match_iregs r1 rA + >>> match_csts cst (exts simm) + >>> recur_simpl + | _ -> error + end + | Pxor(rd, r1, r2) -> + begin match ecode with + | XORx(rS, rA, rB, rc) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_iregs r2 rB + >>> match_bools false rc + >>> recur_simpl + | _ -> error + end + | Pxori(rd, r1, cst) -> + begin match ecode with + | XORI(rS, rA, uimm) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_csts cst (int_int32 uimm) + >>> recur_simpl + | _ -> error + end + | Pxoris(rd, r1, cst) -> + begin match ecode with + | XORIS(rS, rA, uimm) :: es -> + fw + >>> match_iregs rd rA + >>> match_iregs r1 rS + >>> match_csts cst (int_int32 uimm) + >>> recur_simpl + | _ -> error + end +and check_builtin_vload_common ccode ecode pc chunk addr offset res fw = + let error = ERR("Non-matching instructions") in + let recur_simpl = compare_code ccode (List.tl ecode) (Int32.add pc 4l) in + begin match chunk, res with + | Mint8unsigned, IR res -> + begin match ecode with + | LBZ(rD, rA, d) :: es -> + fw + >>> match_iregs res rD + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | Mint8signed, IR res -> + begin match ecode with + | LBZ (rD0, rA0, d0) :: + EXTSBx(rS1, rA1, rc1) :: es -> + fw + >>> match_iregs res rD0 + >>> match_iregs addr rA0 + >>> match_csts offset (exts d0) + >>> match_iregs res rS1 + >>> match_iregs res rA1 + >>> match_bools false rc1 + >>> compare_code ccode es (Int32.add 8l pc) + | _ -> error + end + | Mint16unsigned, IR res -> + begin match ecode with + | LHZ(rD, rA, d) :: es -> + fw + >>> match_iregs res rD + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | Mint16signed, IR res -> + begin match ecode with + | LHA(rD, rA, d) :: es -> + fw + >>> match_iregs res rD + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | Mint32, IR res -> + begin match ecode with + | LWZ(rD, rA, d) :: es -> + fw + >>> match_iregs res rD + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | Mfloat32, FR res -> + begin match ecode with + | LFS(frD, rA, d) :: es -> + fw + >>> match_fregs res frD + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | Mfloat64, FR res -> + begin match ecode with + | LFD(frD, rA, d) :: es -> + fw + >>> match_fregs res frD + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | _ -> error + end +and check_builtin_vstore_common ccode ecode pc chunk addr offset src fw = + let recur_simpl = compare_code ccode (List.tl ecode) (Int32.add pc 4l) in + let error = ERR("Non-matching instructions") in + begin match chunk, src with + | (Mint8signed | Mint8unsigned), IR src -> + begin match ecode with + | STB(rS, rA, d) :: es -> + fw + >>> match_iregs src rS + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | (Mint16signed | Mint16unsigned), IR src -> + begin match ecode with + | STH(rS, rA, d) :: es -> + fw + >>> match_iregs src rS + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | Mint32, IR src -> + begin match ecode with + | STW(rS, rA, d) :: es -> + fw + >>> match_iregs src rS + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | Mfloat32, FR src -> + begin match ecode with + | FRSPx(frD0, frB0, rc0) :: + STFS (frS1, rA1, d1) :: es -> + fw + >>> match_fregs FPR13 frD0 + >>> match_fregs src frB0 + >>> match_bools false rc0 + >>> match_fregs FPR13 frS1 + >>> match_iregs addr rA1 + >>> match_csts offset (exts d1) + >>> compare_code ccode es (Int32.add pc 8l) + | _ -> error + end + | Mfloat64, FR src -> + begin match ecode with + | STFD(frS, rA, d) :: es -> + fw + >>> match_fregs src frS + >>> match_iregs addr rA + >>> match_csts offset (exts d) + >>> recur_simpl + | _ -> error + end + | _ -> error + end + +(** A work element is a triple giving a CompCert ident for the function to + analyze, its name as a string, and the actual code. It is not obvious how + to recover one of the three components given the other two. +*) +type worklist = (ident * string * ccode) list + +(** Pops a work element from the worklist, ensuring that fully-determined idents + (i.e. those for which the possible virtual address have been narrowed to one + candidate) are picked first. + When the first element is not fully-determined, the whole list is sorted so + that hopefully several fully-determined idents are brought at the beginning + at the same time. +*) +let worklist_pop fw wl = + match wl with + | [] -> None + | h::t -> + let (i, _, _) = h in + let candidates = + try PosMap.find i fw.ident_to_sym_ndx + with Not_found -> [] + in + match candidates with + | [] | [_] -> Some (h, t, candidates) + | _ -> + let wl = List.fast_sort + (fun (i1, _, _) (i2, _, _) -> + compare + (List.length (PosMap.find i1 fw.ident_to_sym_ndx)) + (List.length (PosMap.find i2 fw.ident_to_sym_ndx))) + wl in + let winner = List.hd wl in + let (i, _, _) = winner in + Some (winner, List.tl wl, PosMap.find i fw.ident_to_sym_ndx) + +(** Processes a worklist, threading in the framework. +*) +let rec worklist_process (wl: worklist) sfw: s_framework = + match worklist_pop sfw wl with + | None -> sfw (*done*) + | Some ((ident, name, ccode), wl, candidates) -> + let process_ndx ndx = ( + let elf = (sfw |. sf_ef).elf in + let pc = elf.e_symtab.(ndx).st_value in + match code_of_sym_ndx elf ndx with + | None -> assert false + | Some ecode -> + sfw + >>> sf_ef ^%= + add_log (LOG(" Processing function: " ^ name)) + >>> (fun sfw -> + { + sf = sfw; + this_sym_ndx = ndx; + this_ident = ident; + label_to_vaddr = PosMap.empty; + label_list = []; + } + ) + >>> compare_code ccode ecode pc + >>? mark_covered_fun_sym_ndx ndx + ) in + begin match candidates with + | [] -> + sfw + >>> sf_ef ^%= add_log (ERROR("Skipping missing symbol " ^ name)) + >>> worklist_process wl + | [ndx] -> + begin match process_ndx ndx with + | OK(ffw) -> + ffw + >>> check_label_existence + >>> check_label_unicity + >>> (fun ffw -> + worklist_process wl ffw.sf + ) + | ERR(s) -> + sfw + >>> sf_ef ^%= + add_log (ERROR( + "Unique candidate did not match: " ^ s + )) + >>> worklist_process wl + end + | ndxes -> + (* Multiple candidates for one symbol *) + let fws = filter_ok (List.map process_ndx ndxes) in + begin match fws with + | [] -> + sfw + >>> sf_ef ^%= + add_log (ERROR("No matching candidate")) + >>> worklist_process wl + | [ffw] -> + worklist_process wl ffw.sf + | fws -> + sfw + >>> sf_ef ^%= + add_log (ERROR( + "Multiple matching candidates for symbol: " ^ name + )) + >>> worklist_process wl + end + end + +(** This variant helps representing big empty bitstrings without allocating + memory. It is useful to create a bitstring for an STT_NOBITS symbol, for + instance. +*) +type maybe_bitstring = + | Empty of int + | NonEmpty of bitstring + +(** Compares a data symbol with its expected contents. Returns the updated + framework as well as the size of the data matched. +**) +let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framework) + : (s_framework * int) on_success = + let error = ERR("Reached end of data bitstring too soon") in + let rec compare_data_aux l bs s (sfw: s_framework): + (s_framework * int) on_success = + match l with + | [] -> OK(sfw, s) + | d::l -> + begin match d with + | Init_int8(i) -> ( + bitmatch bs with + | { j : 8 : int; bs : -1 : bitstring } -> + if (z_int_lax i) land 0xFF = j + then compare_data_aux l bs (s + 1) sfw + else ERR("Wrong int8") + | { _ } -> error + ) + | Init_int16(i) -> ( + bitmatch bs with + | { j : 16 : int; bs : -1 : bitstring } -> + if (z_int_lax i) land 0xFFFF = j + then compare_data_aux l bs (s + 2) sfw + else ERR("Wrong int16") + | { _ } -> error + ) + | Init_int32(i) -> ( + bitmatch bs with + | { j : 32 : int; bs : -1 : bitstring } -> + if z_int32_lax i = j + then compare_data_aux l bs (s + 4) sfw + else ERR("Wrong int32") + | { _ } -> error + ) + | Init_float32(f) -> ( + bitmatch bs with + | { j : 32 : int; bs : -1 : bitstring } -> + if f = Int32.float_of_bits j + then compare_data_aux l bs (s + 4) sfw + else ERR("Wrong float32") + | { _ } -> error + ) + | Init_float64(f) -> ( + bitmatch bs with + | { j : 64 : int; bs : -1 : bitstring } -> + if f = Int64.float_of_bits j + then compare_data_aux l bs (s + 8) sfw + else ERR("Wrong float64") + | { _ } -> error + ) + | Init_space(z) -> ( + let space_size = z_int z in + bitmatch bs with + | { space : space_size * 8 : bitstring; bs : -1 : bitstring } -> + if is_zeros space (space_size * 8) + then compare_data_aux l bs (s + space_size) sfw + else ERR("Wrong space " ^ + string_of_int (z_int z) ^ " " ^ + string_of_bitstring space) + | { _ } -> error + ) + | Init_addrof(ident, ofs) -> ( + bitmatch bs with + | { vaddr : 32 : int; bs : -1 : bitstring } -> + sfw + >>> idmap_unify ident (Int32.sub vaddr (z_int32 ofs)) + >>= compare_data_aux l bs (s + 4) + | { _ } -> error + ) + end + in + let rec compare_data_empty l s (sfw: s_framework): + (s_framework * int) on_success = + match l with + | [] -> OK(sfw, s) + | d::l -> + begin match d with + | Init_space(z) -> compare_data_empty l (s + z_int z) sfw + | _ -> ERR("Expected empty data") + end + in + match maybebs with + | Empty(_) -> compare_data_empty l 0 sfw + | NonEmpty(bs) -> compare_data_aux l bs 0 sfw + +(** Checks the data symbol table. +*) +let check_data_symtab ident sym_ndx size sfw = + let elf = sfw.ef.elf in + let symtab_ent_start = Int32.( + add + elf.e_shdra.(elf.e_symtab_sndx).sh_offset + (int_int32 (16 * sym_ndx)) + ) in + let sym = sfw.ef.elf.e_symtab.(sym_ndx) in + let atom = Hashtbl.find sfw.atoms ident in + let section = + match atom.a_sections with + | [s] -> s + | _ -> Section_data true + in + sfw + >>> ( + if sym.st_size = int_int32 size + then id + else ( + sf_ef ^%= + add_log (ERROR( + "Incorrect symbol size (" ^ sym.st_name ^ + "): expected " ^ string_of_int32i sym.st_size ^ + ", counted: " ^ string_of_int size + )) + ) + ) + >>> check_st_bind atom sym + >>> ( + match sym.st_type with + | STT_OBJECT -> id + | STT_NOTYPE -> (sf_ef ^%= + add_log (WARNING("Missing type for symbol")) + ) + | _ -> (sf_ef ^%= + add_log (ERROR("Symbol should have type STT_OBJECT")) + ) + ) + >>> ( + if sym.st_other = 0 + then id + else (sf_ef ^%= + add_log (ERROR("Symbol should have st_other set to 0")) + ) + ) + >>> match_sections_name section elf.e_shdra.(sym.st_shndx).sh_name + >>> (sf_ef ^%= + add_range symtab_ent_start 16l 4 (Symtab_data(sym)) + ) + +(** Checks all the program variables. +*) +let check_data (pv: (ident * unit globvar) list) (sfw: s_framework) + : s_framework = + let process_ndx ident ldata sfw ndx = + let elf = (sfw |. sf_ef).elf in + let sym = elf.e_symtab.(ndx) in + let sym_vaddr = sym.st_value in + let sym_size = sym.st_size in + let sym_sndx = sym.st_shndx in + let sym_bs = + match elf.e_shdra.(sym_sndx).sh_type with + | SHT_NOBITS -> + Empty(int32_int sym.st_size * 8) + | SHT_PROGBITS -> + NonEmpty(bitstring_at_vaddr_nosize elf sym_sndx sym_vaddr) + | _ -> assert false + in + let res = + sfw + >>> (sf_ef ^%= add_log (LOG(" Processing data: " ^ sym.st_name))) + >>> compare_data ldata sym_bs in + match res with + | ERR(s) -> ERR(s) + | OK(sfw, size) -> + let sym_shdr = (sfw |. sf_ef).elf.e_shdra.(sym_sndx) in + let sym_ofs_local = Int32.sub sym_vaddr sym_shdr.sh_addr in + let sxn_ofs = sym_shdr.sh_offset in + let sym_begin = Int32.add sxn_ofs sym_ofs_local in + let align = + begin match (Hashtbl.find sfw.atoms ident).a_alignment with + | None -> 0 + | Some(a) -> a + end + in + sfw + >>> ( + begin match sym_shdr.sh_type with + | SHT_NOBITS -> + id + | _ -> + sf_ef ^%= + add_range sym_begin sym_size align (Data_symbol(sym)) + end + ) + (*>>> ((sf_ef |-- chkd_syms) ^%= (SymCoverage.add ndx))*) + >>> ( + if not (is_well_aligned sym_ofs_local align) + then ( + sf_ef ^%= add_log (ERROR( + "Symbol not correctly aligned in the ELF file" + )) + ) + else id + ) + >>> check_data_symtab ident ndx size + >>> (fun sfw -> OK(sfw)) + in + let check_data_aux sfw ig = + let (ident, gv) = ig in + let init_data = gv.gvar_init in + let ident_ndxes = PosMap.find ident sfw.ident_to_sym_ndx in + (*print_endline ("Candidates: " ^ string_of_list id ", " + (List.map + (fun ndx -> fw.elf.e_symtab.(ndx).st_name) + ident_ndxes));*) + let results = List.map (process_ndx ident init_data sfw) ident_ndxes in + let successes = filter_ok results in + match successes with + | [] -> + sfw + >>> sf_ef ^%= add_log (ERROR( + "No matching data segment among candidates [" ^ + (string_of_list + (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_name) + ", " + ident_ndxes + ) ^ + "]\nErrors:\n" ^ + string_of_list + (fun x -> + match x with + | OK(_) -> "" + | ERR(s) -> s ^ "\n" + ) + "" + results + )) + | [sfw] -> sfw + | fws -> + sfw + >>> sf_ef ^%= add_log (ERROR("Multiple matching data segments!")) + in + List.fold_left check_data_aux sfw + (* Empty lists mean the symbol is external, no need for check *) + (List.filter (fun (_, gv) -> gv.gvar_init <> []) pv) + +(** Checks that everything that has been assimiled as a stub during checks + indeed looks like a stub. +*) +let check_stubs sfw = + let check cond msg sfw = + sfw + >>> (if cond then id else (sf_ef ^%= add_log (ERROR(msg)))) + in + let check_eq msg a b = check (a = b) msg in + let match_bools = check_eq "match_bools" in + let match_ints = check_eq "match_ints" in + let check_stub ident vaddr sfw = + let fundef = List.find (fun (i, _) -> i = ident) sfw.program.prog_funct + in + let elf = sfw.ef.elf in + let stub_ecode = from_some (code_at_vaddr elf vaddr 2) in + let stub_sndx = from_some (section_at_vaddr elf vaddr) in + let stub_offset = physical_offset_of_vaddr elf stub_sndx vaddr in + begin match fundef with + | (_, External(EF_external(dest_ident, _) as ef)) -> + let args = (ef_sig ef).sig_args in + if List.mem Tfloat args + then + begin match stub_ecode with + | CREQV(crbD, crbA, crbB) :: (* vaddr *) + Bx(li, aa, lk) :: (* vaddr + 4 *) + [] -> + let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in + begin match idmap_unify dest_ident dest_vaddr sfw with + | ERR(s) -> + sfw + >>> (sf_ef ^%= add_log (ERROR( + "Couldn't match stub, " ^ s + ))) + | OK(sfw) -> + sfw + >>> match_ints 6 crbD + >>> match_ints 6 crbA + >>> match_ints 6 crbB + >>> match_bools false aa + >>> match_bools false lk + >>> (sf_ef ^%= + add_range stub_offset 8l 4 + (Stub(Hashtbl.find sfw.ident_to_name ident)) + ) + end + | _ -> + sfw + >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub"))) + end + else + begin match stub_ecode with + | CRXOR(crbD, crbA, crbB) :: (* vaddr *) + Bx(li, aa, lk) :: (* vaddr + 4 *) + [] -> + let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in + begin match idmap_unify dest_ident dest_vaddr sfw with + | ERR(s) -> + sfw + >>> (sf_ef ^%= add_log (ERROR( + "Couldn't match stub, " ^ s + ))) + | OK(sfw) -> + sfw + >>> match_ints 6 crbD + >>> match_ints 6 crbA + >>> match_ints 6 crbB + >>> match_bools false aa + >>> match_bools false lk + >>> (sf_ef ^%= + add_range stub_offset 8l 4 + (Stub(Hashtbl.find sfw.ident_to_name ident)) + ) + end + | _ -> + sfw + >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub"))) + end + | _ -> assert false + end + in + PosMap.fold check_stub sfw.stub_ident_to_vaddr sfw + +(** Read a .sdump file *) + +let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version + +let read_sdump file = + let ic = open_in_bin file in + try + let magic = String.create (String.length sdump_magic_number) in + really_input ic magic 0 (String.length sdump_magic_number); + if magic <> sdump_magic_number then failwith "bad magic number"; + let prog = (input_value ic: Asm.program) in + let names = (input_value ic: (ident, string) Hashtbl.t) in + let atoms = (input_value ic: (ident, C2C.atom_info) Hashtbl.t) in + close_in ic; + (prog, names, atoms) + with + | End_of_file -> + close_in ic; Printf.eprintf "Truncated file %s\n" file; exit 2 + | Failure msg -> + close_in ic; Printf.eprintf "Corrupted file %s: %s\n" file msg; exit 2 + +(** Processes a .sdump file. +*) +let process_sdump efw sdump: e_framework = + let (prog, names, atoms) = read_sdump sdump in + let ident_to_sym_ndx = + Hashtbl.fold + (fun ident name m -> + match ndxes_of_sym_name efw.elf name with + | [] -> m (* skip if missing *) + | ndxes -> PosMap.add ident ndxes m + ) + names + PosMap.empty + in + let worklist_fundefs = + List.filter + (fun f -> + match snd f with + | Internal _ -> true + | External _ -> false + ) + prog.prog_funct + in + let wl = + List.map + (fun f -> + match f with + | ident, Internal ccode -> (ident, Hashtbl.find names ident, ccode) + | _, External _ -> assert false + ) + worklist_fundefs + in + efw + >>> (fun efw -> + { + ef = efw; + program = prog; + ident_to_name = names; + ident_to_sym_ndx = ident_to_sym_ndx; + stub_ident_to_vaddr = PosMap.empty; + atoms = atoms; + } + ) + >>> worklist_process wl + >>> check_stubs + >>> check_data prog.prog_vars + >>> (fun sfw -> sfw.ef) + +(** Builds the list [0; 1; ...; n - 1]. *) +let list_n (n: int): int list = + let rec list_n_aux x l = + if x < 0 + then l + else list_n_aux (x - 1) (x :: l) + in list_n_aux (n - 1) [] + +(** Returns true if [a, b] intersects [ofs, ofs + size - 1]. *) +let intersect (a, b) ofs size: bool = + let within (a, b) x = (a <= x) && (x <= b) in + (within (a, b) ofs) || (within (ofs, Int32.(sub (add ofs size) 1l)) a) + +let string_of_range a b = "[0x" ^ Printf.sprintf "%08lx" a ^ " - 0x" ^ + Printf.sprintf "%08lx" b ^ "]" + +(** Checks that the bits from [start] to [stop] in [bs] are zeroed. *) +let is_padding bs start stop = + let bs_start = start * 8 in + let bs_length = (stop - start + 1) * 8 in + is_zeros (Bitstring.subbitstring bs bs_start bs_length) bs_length + +(** This functions goes through the list of checked bytes, and tries to find + padding in it. That is, it takes pairs of chunks in order, and adds a + padding chunk in between if these conditions are met: + + - the second chunk needs to be aligned. + + - the difference between the two chunks is strictly less than the alignment. + + - the data in this space is zeroed. + + Otherwise, it fills holes with an Unknown chunk. + Returns a framework where [chkd_bytes_list] is sorted and full. +*) +let check_padding efw = + (*let elf = efw.elf in + let sndxes = list_n elf.e_hdr.e_shnum in + let matching_sections x y = + string_of_list + id + ", " + List.(map + (fun ndx -> elf.e_shdra.(ndx).sh_name) + (List.filter + (fun ndx -> + let shdr = elf.e_shdra.(ndx) in + intersect (x, y) shdr.sh_offset shdr.sh_size + ) + sndxes + ) + ) + in*) + (*let matching_symbols x y = + string_of_list + id + ", " + List.(map + (fun sym -> sym.st_name) + (List.filter + (fun sym -> + if sym.st_shndx >= Array.length elf.e_shdra + then false (* special section *) + else + let offset = + physical_offset_of_vaddr elf sym.st_shndx sym.st_value + in + intersect (x, y) offset sym.st_size + ) + (Array.to_list elf.e_symtab) + ) + ) + in*) + let unknown x y = Unknown("" + (*^ "Sections: " ^ matching_sections x y*) + (*^ "\nSymbols: " ^ matching_symbols x y*) + ) + in + (* check_padding_aux assumes a sorted list *) + let rec check_padding_aux efw accu l = + match l with + | [] -> assert false + (* if there is only one chunk left, we add an unknown space between it and + the end. *) + | [(_, e, _, _) as h] -> + let elf_size = + int_int32 ((Bitstring.bitstring_length efw.elf.e_bitstring) / 8) in + let elf_end = Int32.sub elf_size 1l in + if e = elf_end + then { efw with + chkd_bytes_list = List.rev (h :: accu); + } + else ( + let start = Int32.add e 1l in + { efw with + chkd_bytes_list = List.rev + ((start, elf_end, 0, unknown start elf_end) :: h :: accu); + } + ) + | ((b1, e1, a1, n1) as h1) :: ((b2, e2, a2, n2) as h2) :: rest -> + (*print_endline ( + "\n1: [" ^ string_of_int32 b1 ^ " - " ^ string_of_int32 e1 ^ "]" + ); + print_endline ( + "2: [" ^ string_of_int32 b2 ^ " - " ^ string_of_int32 e2 ^ "]" + );*) + let pad_start = Int32.add e1 1l in + let pad_stop = Int32.sub b2 1l in + if + pad_start = b2 (* if they are directly consecutive *) + || int32_int (Int32.sub b2 e1) > a2 (* or if they are too far away *) + || not (is_padding efw.elf.e_bitstring + (int32_int pad_start) (int32_int pad_stop)) + then (* not padding *) + if pad_start <= pad_stop + then check_padding_aux efw + ((pad_start, pad_stop, 0, unknown pad_start pad_stop) :: h1 :: accu) + (h2 :: rest) + else check_padding_aux efw (h1 :: accu) (h2 :: rest) + else ( (* this is padding! *) + (* let efw = + { efw with + chkd_bytes_diet = + ELFCoverage.r_add pad_start pad_stop efw.chkd_bytes_diet; + } + in*) + check_padding_aux efw + ((pad_start, pad_stop, 0, Padding) :: h1 :: accu) + (h2 :: rest) + ) + in + let sorted_chkd_bytes_list = + List.fast_sort + (fun (a, _, _, _) (b, _, _, _) -> Int32.compare a b) + efw.chkd_bytes_list + in check_padding_aux efw [] sorted_chkd_bytes_list + +(** Checks a boolean. *) +let ef_checkb b msg = + if b then id else add_log(ERROR(msg)) + +let check_elf_identification efw = + let ei = efw.elf.e_hdr.e_ident in + efw + >>> ef_checkb (ei.ei_class = ELFCLASS32) "ELF class should be ELFCLASS32" + >>> ef_checkb (ei.ei_data = ELFDATA2MSB || ei.ei_data = ELFDATA2LSB) + "ELF should be MSB or LSB" + >>> ef_checkb (ei.ei_version = EV_CURRENT) + "ELF identificatin version should be EV_CURRENT" + +let check_elf_header efw: e_framework = + let eh = efw.elf.e_hdr in + efw + >>> check_elf_identification + >>> ef_checkb (eh.e_type = ET_EXEC) "ELF type should be ET_EXEC" + >>> ef_checkb (eh.e_machine = EM_PPC) "ELF machine should be PPC" + >>> ef_checkb (eh.e_version = EV_CURRENT) "ELF version should be EV_CURRENT" + >>> add_range 0l 52l 0 ELF_header (* Header is always 52-bytes long *) + +(** Checks the index 0 of the symbol table. This index is reserved to hold + special values. *) +let check_sym_tab_zero efw = + let elf = efw.elf in + let sym0 = efw.elf.e_symtab.(0) in + efw + >>> ( + if sym0.st_name = "" + then id + else add_log (ERROR("Symbol 0 should not have a name")) + ) + >>> ( + if sym0.st_value = 0l + then id + else add_log (ERROR("Symbol 0 should have st_value = 0")) + ) + >>> ( + if sym0.st_size = 0l + then id + else add_log (ERROR("Symbol 0 should have st_size = 0")) + ) + >>> ( + if sym0.st_bind = STB_LOCAL + then id + else add_log (ERROR("Symbol 0 should have STB_LOCAL binding")) + ) + >>> ( + if sym0.st_type = STT_NOTYPE + then id + else add_log (ERROR("Symbol 0 should have STT_NOTYPE type")) + ) + >>> ( + if sym0.st_other = 0 + then id + else add_log (ERROR("Symbol 0 should have st_other = 0")) + ) + >>> ( + if sym0.st_shndx = shn_UNDEF + then id + else add_log (ERROR("Symbol 0 should have st_shndx = SHN_UNDEF")) + ) + >>> add_range elf.e_shdra.(elf.e_symtab_sndx).sh_offset 16l 4 Zero_symbol + +(** Checks a whole ELF file according to a list of .sdump files. *) +let check_elf elf sdumps = + let eh = elf.e_hdr in + let section_strtab = elf.e_shdra.(eh.e_shstrndx) in + let symtab_shdr = elf.e_shdra.(elf.e_symtab_sndx) in + let symbol_strtab = elf.e_shdra.(int32_int symtab_shdr.sh_link) in + let efw = + { + elf = elf; + log = []; + (*chkd_syms = SymCoverage.empty; + chkd_bytes_diet = ELFCoverage.empty;*) + chkd_bytes_list = []; + } + >>> check_elf_header + >>> add_range + eh.e_phoff + (int_int32 (eh.e_phnum * eh.e_phentsize)) + 4 + ELF_progtab + >>> add_range + eh.e_shoff + (int_int32 (eh.e_shnum * eh.e_shentsize)) + 4 + ELF_shtab + >>> add_range + section_strtab.sh_offset + section_strtab.sh_size + 0 + ELF_section_strtab + >>> add_range + symbol_strtab.sh_offset + symbol_strtab.sh_size + 0 + ELF_symbol_strtab + >>> check_sym_tab_zero + in + List.fold_left process_sdump efw sdumps + >>> check_padding + (* + print_endline "UNCOVERED SYMBOLS:"; + let sym_range = SymCoverage.r_singleton 0 ((Array.length e.e_symtab) - 1) in + print_endline + (string_of_list + (fun ndx -> "(" ^ string_of_int ndx ^ "): " ^ + e.e_symtab.(ndx).st_name) + "\n" + SymCoverage.(elements (diff sym_range efw.chkd_syms)) + ); + *) + >>> add_log (LOG("ELF map:")) + >>> (fun efw -> + efw + >>> add_log (LOG( + string_of_list + (fun (a, b, align, r) -> string_of_range a b ^ " (" ^ + string_of_int align ^ ") " ^ string_of_byte_chunk_desc r) + "\n" + efw.chkd_bytes_list + )) + ) + +(** Checks a whole ELF file according to .sdump files. + If requested, dump the calculated bytes mapping, so that it can be + reused by the fuzzer. *) +let check_and_dump elffilename sdumps = + let elf = read_elf elffilename in + check_elf elf sdumps + >>> (fun efw -> + if !dump_elfmap then begin + (* dump the elf map for fuzz-testing *) + let oc = open_out (elffilename ^ ".elfmap") in + output_value oc efw.chkd_bytes_list; + close_out oc + end; + efw + ) + >>> (fun efw -> + if not !debug + then List.( + iter + (fun e -> + print_endline (string_of_log_entry e) + ) + (rev efw.log) + ) + ) + diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml new file mode 100644 index 0000000..c71ff00 --- /dev/null +++ b/checklink/ELF_parsers.ml @@ -0,0 +1,322 @@ +open Bitstring_utils +open ELF_types +open ELF_printers +open ELF_utils +open Library +open PPC_parsers + +exception Unknown_endianness + +(** Converts an elf endian into a bitstring endian *) +let elfdata_to_endian (e: elfdata): Bitstring.endian = + match e with + | ELFDATA2LSB -> Bitstring.LittleEndian + | ELFDATA2MSB -> Bitstring.BigEndian + | _ -> raise Unknown_endianness + +(** Parses an elf32 header *) +let read_elf32_ehdr (bs: bitstring): elf32_ehdr = + bitmatch bs with + | { e_ident : 16*8 : bitstring ; + rest : -1 : bitstring } -> + ( + bitmatch e_ident with + | { 0x7F : 8 ; + "ELF" : 24 : string ; + ei_class : 8 : int ; + ei_data : 8 : int ; + ei_version : 8 : int ; + padding : 72 : bitstring } -> + assert (is_zeros padding 72); + let ei_data = ( + match ei_data with + | 0 -> ELFDATANONE + | 1 -> ELFDATA2LSB + | 2 -> ELFDATA2MSB + | _ -> ELFDATAUNKNOWN + ) + in + let e = elfdata_to_endian ei_data in + ( + bitmatch rest with + | { e_type : 16 : int, endian(e) ; + e_machine : 16 : int, endian(e) ; + e_version : 32 : int, endian(e) ; + e_entry : 32 : int, endian(e) ; + e_phoff : 32 : int, endian(e) ; + e_shoff : 32 : int, endian(e) ; + e_flags : 32 : bitstring ; + e_ehsize : 16 : int, endian(e) ; + e_phentsize : 16 : int, endian(e) ; + e_phnum : 16 : int, endian(e) ; + e_shentsize : 16 : int, endian(e) ; + e_shnum : 16 : int, endian(e) ; + e_shstrndx : 16 : int, endian(e) } -> + (* These shouldn't be different than this... *) + assert (e_ehsize = 52); + assert (e_phentsize = 32); + assert (e_shentsize = 40); + { + e_ident = + { + ei_class = ( + match ei_class with + | 0 -> ELFCLASSNONE + | 1 -> ELFCLASS32 + | 2 -> ELFCLASS64 + | _ -> ELFCLASSUNKNOWN + ); + ei_data = ei_data; + ei_version = ( + match ei_version with + | 0 -> EV_NONE + | 1 -> EV_CURRENT + | _ -> EV_UNKNOWN + ); + }; + e_type = ( + match e_type with + | 0 -> ET_NONE + | 1 -> ET_REL + | 2 -> ET_EXEC + | 3 -> ET_DYN + | 4 -> ET_CORE + | _ -> ET_UNKNOWN + ); + e_machine = ( + match e_machine with + | 0 -> EM_NONE + | 1 -> EM_M32 + | 2 -> EM_SPARC + | 3 -> EM_386 + | 4 -> EM_68K + | 5 -> EM_88K + | 7 -> EM_860 + | 8 -> EM_MIPS + | 10 -> EM_MIPS_RS4_BE + | 20 -> EM_PPC + | _ -> EM_UNKNOWN + ); + e_version = ( + match e_version with + | 0l -> EV_NONE + | 1l -> EV_CURRENT + | _ -> EV_UNKNOWN + ); + e_entry = e_entry; + e_phoff = e_phoff; + e_shoff = e_shoff; + e_flags = e_flags; + e_ehsize = e_ehsize; + e_phentsize = e_phentsize; + e_phnum = e_phnum; + e_shentsize = e_shentsize; + e_shnum = e_shnum; + e_shstrndx = e_shstrndx; + } + ) + ) + +(** Returns the file offset of the section header indexed *) +let section_header_offset (e_hdr: elf32_ehdr) (sndx: int): int = + int32_int e_hdr.e_shoff + sndx * e_hdr.e_shentsize + +(** Returns the ndx-th string in the provided bitstring, according to null + characters *) +let strtab_string (bs: bitstring) (ndx: int): string = + let (str, ofs, _) = bs in + let start = (ofs/8 + ndx) in + String.sub str start (String.index_from str start '\000' - start) + +(** Reads an ELF section header *) +let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) + (num: int): elf32_shdr = + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let byte_ofs = section_header_offset e_hdr num in + bitmatch bs with + | { sh_name : 32 : endian(e), offset(byte_ofs*8) ; + sh_type : 32 : endian(e) ; + sh_flags : 32 : endian(e) ; + sh_addr : 32 : endian(e) ; + sh_offset : 32 : endian(e) ; + sh_size : 32 : endian(e) ; + sh_link : 32 : endian(e) ; + sh_info : 32 : endian(e) ; + sh_addralign : 32 : endian(e) ; + sh_entsize : 32 : endian(e) } -> + { + sh_name = strtab_string strtab (int32_int sh_name); + sh_type = ( + match sh_type with + | 0l -> SHT_NULL + | 1l -> SHT_PROGBITS + | 2l -> SHT_SYMTAB + | 3l -> SHT_STRTAB + | 4l -> SHT_RELA + | 5l -> SHT_HASH + | 6l -> SHT_DYNAMIC + | 7l -> SHT_NOTE + | 8l -> SHT_NOBITS + | 9l -> SHT_REL + | 10l -> SHT_SHLIB + | 11l -> SHT_DYNSYM + | _ -> SHT_UNKNOWN + ); + sh_flags = sh_flags ; + sh_addr = sh_addr ; + sh_offset = sh_offset ; + sh_size = sh_size ; + sh_link = sh_link ; + sh_info = sh_info ; + sh_addralign = sh_addralign ; + sh_entsize = sh_entsize ; + } + +(** Reads an elf program header *) +let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) + : elf32_phdr = + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let phdr_ofs = int32_int e_hdr.e_phoff + ndx * e_hdr.e_phentsize in + bitmatch bs with + | { p_type : 32 : endian(e), offset(phdr_ofs*8) ; + p_offset : 32 : endian(e) ; + p_vaddr : 32 : endian(e) ; + p_paddr : 32 : endian(e) ; + p_filesz : 32 : endian(e) ; + p_memsz : 32 : endian(e) ; + p_flags : 32 : bitstring ; + p_align : 32 : endian(e) } -> + { + p_type = ( + match p_type with + | 0l -> PT_NULL + | 1l -> PT_LOAD + | 2l -> PT_DYNAMIC + | 3l -> PT_INTERP + | 4l -> PT_NOTE + | 5l -> PT_SHLIB + | 6l -> PT_PHDR + | _ -> PT_UNKNOWN + ); + p_offset = p_offset ; + p_vaddr = p_vaddr ; + p_paddr = p_paddr ; + p_filesz = p_filesz ; + p_memsz = p_memsz ; + p_flags = p_flags ; + p_align = p_align ; + } + +(** Reads an ELF symbol *) +let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring) + (num: int): elf32_sym = + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + bitmatch symtab with + | { st_name : 32 : endian(e), offset(num*16*8) ; + st_value : 32 : endian(e) ; + st_size : 32 : endian(e) ; + st_bind : 4 ; + st_type : 4 ; + st_other : 8 ; + st_shndx : 16 : endian(e) } -> + { + st_name = strtab_string strtab (int32_int st_name) ; + st_value = st_value ; + st_size = st_size ; + st_bind = ( + match st_bind with + | 0 -> STB_LOCAL + | 1 -> STB_GLOBAL + | 2 -> STB_WEAK + | _ -> STB_UNKNOWN + ); + st_type = ( + match st_type with + | 0 -> STT_NOTYPE + | 1 -> STT_OBJECT + | 2 -> STT_FUNC + | 3 -> STT_SECTION + | 4 -> STT_FILE + | _ -> STT_UNKNOWN + ); + st_other = st_other ; + st_shndx = st_shndx ; + } + +(** Aborts if two sections overlap *) +let check_overlaps (shdra: elf32_shdr array) (ehdr: elf32_ehdr): unit = + let intersect a asize b bsize = + asize <> 0l && bsize <> 0l && + ( + let last x xsize = Int32.(sub (add x xsize) 1l) in + let alast = last a asize in + let blast = last b bsize in + let within (a, b) x = (a <= x) && (x <= b) in + (within (a, alast) b) || (within (b, blast) a) + ) + in + Array.iteri + (fun i ai -> + if ai.sh_type <> SHT_NOBITS + then + let ai_intersects = intersect ai.sh_offset ai.sh_size in + if + ai_intersects 0l 52l (* ELF header *) + || ai_intersects ehdr.e_phoff + (int_int32 (ehdr.e_phnum * ehdr.e_phentsize)) + || ai_intersects ehdr.e_shoff + (int_int32 (ehdr.e_shnum * ehdr.e_shentsize)) + then assert false + else + Array.iteri + (fun j aj -> + if + i <> j + && aj.sh_type <> SHT_NOBITS + && ai_intersects aj.sh_offset aj.sh_size + then assert false + ) + shdra + ) + shdra + +(** Reads a whole ELF file from a bitstring *) +let read_elf_bs (bs: bitstring): elf = + let e_hdr = read_elf32_ehdr bs in + (* To initialize section names we need the string table *) + let strtab = ( + let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let strtab_sndx = e_hdr.e_shstrndx in + let strtab_shofs = section_header_offset e_hdr strtab_sndx in + bitmatch bs with + | { ofs : 32 : endian(e), offset(strtab_shofs * 8 + 128) ; + size : 32 : endian(e) } -> + Bitstring.subbitstring bs (int32_int ofs * 8) (int32_int size * 8) + ) + in + let e_shdra = + Array.init e_hdr.e_shnum (read_elf32_shdr e_hdr bs strtab) + in + check_overlaps e_shdra e_hdr; + let symtab_sndx = section_ndx_by_name_noelf e_shdra ".symtab" in + { + e_bitstring = bs ; + e_hdr = e_hdr ; + e_shdra = e_shdra ; + e_phdra = Array.init e_hdr.e_phnum (read_elf32_phdr e_hdr bs) ; + e_symtab = ( + let symtab_shdr = e_shdra.(symtab_sndx) in + let symtab_strtab_sndx = symtab_shdr.sh_link in + let symtab_nb_ent = (int32_int symtab_shdr.sh_size / 16) in + Array.init symtab_nb_ent + (read_elf32_sym e_hdr + (section_bitstring_noelf bs e_shdra symtab_sndx) + (section_bitstring_noelf bs e_shdra (int32_int symtab_strtab_sndx))) + ); + e_symtab_sndx = symtab_sndx; + } + +(** Reads a whole ELF file from a file name *) +let read_elf (elffilename: string): elf = + let bs = Bitstring.bitstring_of_file elffilename in + read_elf_bs bs diff --git a/checklink/ELF_printers.ml b/checklink/ELF_printers.ml new file mode 100644 index 0000000..f0f154e --- /dev/null +++ b/checklink/ELF_printers.ml @@ -0,0 +1,151 @@ +open ELF_types +open Library + +let string_of_elf32_half = string_of_int +let string_of_elf32_addr = string_of_int32 +let string_of_elf32_off = string_of_int32 +let string_of_elf32_word = string_of_int32 + +let string_of_elfclass = function +| ELFCLASSNONE -> "ELFCLASSNONE" +| ELFCLASS32 -> "ELFCLASS32" +| ELFCLASS64 -> "ELFCLASS64" +| ELFCLASSUNKNOWN -> "ELFCLASSUNKNOWN" + +let string_of_elfdata = function +| ELFDATANONE -> "ELFDATANONE" +| ELFDATA2LSB -> "ELFDATA2LSB" +| ELFDATA2MSB -> "ELFDATA2MSB" +| ELFDATAUNKNOWN -> "ELFDATAUNKNOWN" + +let string_of_ev = function +| EV_NONE -> "EV_NONE" +| EV_CURRENT -> "EV_CURRENT" +| EV_UNKNOWN -> "EV_UNKNOWN" + +let string_of_elf_identification ei = + "{\nei_class = " ^ string_of_elfclass ei.ei_class ^ + ";\nei_data = " ^ string_of_elfdata ei.ei_data ^ + ";\nei_version = " ^ string_of_ev ei.ei_version ^ + ";\n}" + +let string_of_et = function +| ET_NONE -> "ET_NONE" +| ET_REL -> "ET_REL" +| ET_EXEC -> "ET_EXEC" +| ET_DYN -> "ET_DYN" +| ET_CORE -> "ET_CORE" +| ET_UNKNOWN -> "ET_UNKNOWN" + +let string_of_em = function +| EM_NONE -> "EM_NONE" +| EM_M32 -> "EM_M32" +| EM_SPARC -> "EM_SPARC" +| EM_386 -> "EM_386" +| EM_68K -> "EM_68K" +| EM_88K -> "EM_88K" +| EM_860 -> "EM_860" +| EM_MIPS -> "EM_MIPS" +| EM_MIPS_RS4_BE -> "EM_MIPS_RS4_BE" +| EM_PPC -> "EM_PPC" +| EM_UNKNOWN -> "EM_UNKNOWN" + +let string_of_elf32_ehdr eh = + "{\ne_ident = " ^ string_of_elf_identification eh.e_ident ^ + ";\ne_type = " ^ string_of_et eh.e_type ^ + ";\ne_machine = " ^ string_of_em eh.e_machine ^ + ";\ne_version = " ^ string_of_ev eh.e_version ^ + ";\ne_entry = " ^ string_of_elf32_addr eh.e_entry ^ + ";\ne_phoff = " ^ string_of_elf32_off eh.e_phoff ^ + ";\ne_shoff = " ^ string_of_elf32_off eh.e_shoff ^ + ";\ne_flags = " ^ string_of_bitstring eh.e_flags ^ + ";\ne_ehsize = " ^ string_of_elf32_half eh.e_ehsize ^ + ";\ne_phentsize = " ^ string_of_elf32_half eh.e_phentsize ^ + ";\ne_phnum = " ^ string_of_elf32_half eh.e_phnum ^ + ";\ne_shentsize = " ^ string_of_elf32_half eh.e_shentsize ^ + ";\ne_shnum = " ^ string_of_elf32_half eh.e_shnum ^ + ";\ne_shstrndx = " ^ string_of_elf32_half eh.e_shstrndx ^ + ";\n}" + +let string_of_sht = function +| SHT_NULL -> "SHT_NULL" +| SHT_PROGBITS -> "SHT_PROGBITS" +| SHT_SYMTAB -> "SHT_SYMTAB" +| SHT_STRTAB -> "SHT_STRTAB" +| SHT_RELA -> "SHT_RELA" +| SHT_HASH -> "SHT_HASH" +| SHT_DYNAMIC -> "SHT_DYNAMIC" +| SHT_NOTE -> "SHT_NOTE" +| SHT_NOBITS -> "SHT_NOBITS" +| SHT_REL -> "SHT_REL" +| SHT_SHLIB -> "SHT_SHLIB" +| SHT_DYNSYM -> "SHT_DYNSYM" +| SHT_UNKNOWN -> "SHT_UNKNOWN" + +let string_of_elf32_shdr sh = + "{\nsh_name = " ^ sh.sh_name ^ + ";\nsh_type = " ^ string_of_sht sh.sh_type ^ + ";\nsh_flags = " ^ string_of_elf32_word sh.sh_flags ^ + ";\nsh_addr = " ^ string_of_elf32_addr sh.sh_addr ^ + ";\nsh_offset = " ^ string_of_elf32_off sh.sh_offset ^ + ";\nsh_size = " ^ string_of_elf32_word sh.sh_size ^ + ";\nsh_link = " ^ string_of_elf32_word sh.sh_link ^ + ";\nsh_info = " ^ string_of_elf32_word sh.sh_info ^ + ";\nsh_addralign = " ^ string_of_elf32_word sh.sh_addralign ^ + ";\nsh_entsize = " ^ string_of_elf32_word sh.sh_entsize ^ + ";\n}" + +let string_of_p_type = function +| PT_NULL -> "PT_NULL" +| PT_LOAD -> "PT_LOAD" +| PT_DYNAMIC -> "PT_DYNAMIC" +| PT_INTERP -> "PT_INTERP" +| PT_NOTE -> "PT_NOTE" +| PT_SHLIB -> "PT_SHLIB" +| PT_PHDR -> "PT_PHDR" +| PT_UNKNOWN -> "PT_UNKNOWN" + +let string_of_elf32_phdr ph = + "{\np_type = " ^ string_of_p_type ph.p_type ^ + ";\np_offset = " ^ string_of_elf32_off ph.p_offset ^ + ";\np_vaddr = " ^ string_of_elf32_addr ph.p_vaddr ^ + ";\np_paddr = " ^ string_of_elf32_addr ph.p_paddr ^ + ";\np_filesz = " ^ string_of_elf32_word ph.p_filesz ^ + ";\np_memsz = " ^ string_of_elf32_word ph.p_memsz ^ + ";\np_flags = " ^ string_of_bitstring ph.p_flags ^ + ";\np_align = " ^ string_of_elf32_word ph.p_align ^ + ";\n}" + +let string_of_elf32_st_bind = function +| STB_LOCAL -> "STB_LOCAL" +| STB_GLOBAL -> "STB_GLOBAL" +| STB_WEAK -> "STB_WEAK" +| STB_UNKNOWN -> "STB_UNKNOWN" + +let string_of_elf32_st_type = function +| STT_NOTYPE -> "STT_NOTYPE" +| STT_OBJECT -> "STT_OBJECT" +| STT_FUNC -> "STT_FUNC" +| STT_SECTION -> "STT_SECTION" +| STT_FILE -> "STT_FILE" +| STT_UNKNOWN -> "STT_UNKNOWN" + +let string_of_elf32_sym s = + "{\nst_name = " ^ s.st_name ^ + ";\nst_value = " ^ string_of_elf32_addr s.st_value ^ + ";\nst_size = " ^ string_of_elf32_word s.st_size ^ + ";\nst_bind = " ^ string_of_elf32_st_bind s.st_bind ^ + ";\nst_type = " ^ string_of_elf32_st_type s.st_type ^ + ";\nst_other = " ^ string_of_int s.st_other ^ + ";\nst_shndx = " ^ string_of_elf32_half s.st_shndx ^ + ";\n}" + +let string_of_elf e = + "{\ne_header = " ^ string_of_elf32_ehdr e.e_hdr ^ + ";\ne_sections = " ^ + string_of_array string_of_elf32_shdr ",\n" e.e_shdra ^ + ";\ne_programs = " ^ + string_of_array string_of_elf32_phdr ",\n" e.e_phdra ^ + ";\ne_symtab = " ^ + string_of_array string_of_elf32_sym ",\n" e.e_symtab ^ + ";\n}" diff --git a/checklink/ELF_types.ml b/checklink/ELF_types.ml new file mode 100644 index 0000000..a58b1eb --- /dev/null +++ b/checklink/ELF_types.ml @@ -0,0 +1,168 @@ +open Library + +type elf32_addr = int32 +type elf32_half = int +type elf32_off = int32 +type elf32_sword = int32 +type elf32_word = int32 +type byte = int + +(** ELF identification *) + +type elfclass = + | ELFCLASSNONE + | ELFCLASS32 + | ELFCLASS64 + | ELFCLASSUNKNOWN + +type elfdata = + | ELFDATANONE + | ELFDATA2LSB + | ELFDATA2MSB + | ELFDATAUNKNOWN + +type ev = + | EV_NONE + | EV_CURRENT + | EV_UNKNOWN + +type elf_identification = { + ei_class: elfclass; (* 32/64 bit *) + ei_data: elfdata; (* endianness *) + ei_version: ev; (* ELF header version *) +} + +(** ELF header *) + +type et = + | ET_NONE + | ET_REL + | ET_EXEC + | ET_DYN + | ET_CORE + | ET_UNKNOWN + +type em = + | EM_NONE + | EM_M32 + | EM_SPARC + | EM_386 + | EM_68K + | EM_88K + | EM_860 + | EM_MIPS + | EM_MIPS_RS4_BE + | EM_PPC + | EM_UNKNOWN + +let shn_UNDEF = 0 +let shn_ABS = 0xFFF1 +let shn_COMMON = 0xFFF2 + +type elf32_ehdr = { + e_ident: elf_identification; (* Machine-independent data *) + e_type: et; (* Object file type *) + e_machine: em; (* Required architecture *) + e_version: ev; (* Object file version *) + e_entry: elf32_addr; (* Entry point virtual address *) + e_phoff: elf32_off; (* Program header table's offset *) + e_shoff: elf32_off; (* Section header table's offset *) + e_flags: Bitstring.bitstring; (* Processor-specific flags *) + e_ehsize: elf32_half; (* ELF header size *) + e_phentsize: elf32_half; (* Size of a program header's entry *) + e_phnum: elf32_half; (* Number of program header entries *) + e_shentsize: elf32_half; (* Size of a section header's entry *) + e_shnum: elf32_half; (* Number of section header entries *) + e_shstrndx: elf32_half; (* Section name string table index *) +} + +(** ELF section header *) + +type sht = + | SHT_NULL + | SHT_PROGBITS + | SHT_SYMTAB + | SHT_STRTAB + | SHT_RELA + | SHT_HASH + | SHT_DYNAMIC + | SHT_NOTE + | SHT_NOBITS + | SHT_REL + | SHT_SHLIB + | SHT_DYNSYM + | SHT_UNKNOWN + +type elf32_shdr = { + sh_name: string; + sh_type: sht; + sh_flags: elf32_word; + sh_addr: elf32_addr; + sh_offset: elf32_off; + sh_size: elf32_word; + sh_link: elf32_word; + sh_info: elf32_word; + sh_addralign: elf32_word; + sh_entsize: elf32_word; +} + +let shf_WRITE = 0x1l +let shf_ALLOC = 0x2l +let shf_EXECINSTR = 0x4l + +type elf32_st_bind = + | STB_LOCAL + | STB_GLOBAL + | STB_WEAK + | STB_UNKNOWN + +type elf32_st_type = + | STT_NOTYPE + | STT_OBJECT + | STT_FUNC + | STT_SECTION + | STT_FILE + | STT_UNKNOWN + +type elf32_sym = { + st_name: string; + st_value: elf32_addr; + st_size: elf32_word; + st_bind: elf32_st_bind; + st_type: elf32_st_type; + st_other: byte; + st_shndx: elf32_half; +} + +(** ELF program header *) + +type p_type = + | PT_NULL + | PT_LOAD + | PT_DYNAMIC + | PT_INTERP + | PT_NOTE + | PT_SHLIB + | PT_PHDR + | PT_UNKNOWN + +type elf32_phdr = { + p_type: p_type ; + p_offset: elf32_off ; + p_vaddr: elf32_addr ; + p_paddr: elf32_addr ; + p_filesz: elf32_word ; + p_memsz: elf32_word ; + p_flags: bitstring ; + p_align: elf32_word ; +} + +(** ELF *) +type elf = { + e_bitstring: bitstring; + e_hdr: elf32_ehdr; + e_shdra: elf32_shdr array; + e_phdra: elf32_phdr array; + e_symtab: elf32_sym array; + e_symtab_sndx: int; (* to avoid having to find it again when needed *) +} diff --git a/checklink/ELF_utils.ml b/checklink/ELF_utils.ml new file mode 100644 index 0000000..f860e3f --- /dev/null +++ b/checklink/ELF_utils.ml @@ -0,0 +1,85 @@ +open ELF_types +open Library + +let section_ndx_by_name_noelf (eshdra: elf32_shdr array)(name: string): int = + match array_exists (fun eshdr -> eshdr.sh_name = name) eshdra with + | Some sndx -> sndx + | None -> assert false + +let section_ndx_by_name (e: elf)(name: string): int option = + array_exists (fun eshdr -> eshdr.sh_name = name) e.e_shdra + +let section_bitstring_noelf + (bs: bitstring)(eshdra: elf32_shdr array)(sndx: int): bitstring = + let sofs = int32_int eshdra.(sndx).sh_offset in + let size = int32_int eshdra.(sndx).sh_size in + Bitstring.subbitstring bs (sofs * 8) (size * 8) + +let section_bitstring (e: elf): int -> bitstring = + section_bitstring_noelf e.e_bitstring e.e_shdra + +let physical_offset_of_vaddr (e: elf)(sndx: int)(vaddr: int32): int32 = + let shdr = e.e_shdra.(sndx) in + Int32.(add shdr.sh_offset (sub vaddr shdr.sh_addr)) + +let section_at_vaddr (e: elf)(vaddr: int32): int option = + array_exists + (fun shdr -> + shdr.sh_addr <= vaddr && vaddr < Int32.add shdr.sh_addr shdr.sh_size + ) + e.e_shdra + +(** + Returns the entire bitstring that begins at the specified virtual address + within the specified section and ends at the end of the file. This is useful + when you don't know the sections size yet. +*) +let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring = + let shdr = e.e_shdra.(sndx) in + let bs = section_bitstring e sndx in + let ofs = int32_int (Int32.sub vaddr shdr.sh_addr) in + bitmatch bs with + | { subbs : -1 : bitstring, offset(8*ofs) } -> subbs + +(** + Returns the bitstring of the specified size beginning at the specified + virtual address within the specified section. +*) +let bitstring_at_vaddr e sndx vaddr size = + let shdr = e.e_shdra.(sndx) in + let bs = section_bitstring e sndx in + let ofs = int32_int (Int32.sub vaddr shdr.sh_addr) in + bitmatch bs with + | { subbs : size : bitstring, offset(8*ofs) } -> subbs + +(** + Removes symbol version for GCC's symbols. +*) +let strip_versioning (s: string): string = + try String.sub s 0 (String.index s '@') + with Not_found -> s + +(** + Removes CompCert's mangling of variadic functions +*) +let strip_mangling (s: string): string = + try String.sub s 0 (String.index s '$') + with Not_found -> s + +(** + Returns the index of the first symbol matching the specified name, if it + exists. +*) +let ndx_of_sym_name (e: elf) (name: string): int option = + array_exists + (fun x -> strip_versioning x.st_name = strip_mangling name) + e.e_symtab + +(** + Returns the list of all symbols matching the specified name. +*) +let ndxes_of_sym_name (e: elf) (name: string): int list = + List.map fst + (List.filter + (fun (_, x) -> strip_versioning x.st_name = strip_mangling name) + (Array.to_list (Array.mapi (fun a b -> (a, b)) e.e_symtab))) diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml new file mode 100644 index 0000000..b6d4d4b --- /dev/null +++ b/checklink/Frameworks.ml @@ -0,0 +1,194 @@ +open Asm +open AST +open BinPos +open ELF_types +open Lens +open Library + +type log_entry = + | LOG of string + | ERROR of string + | WARNING of string + | DEBUG of string + +type byte_chunk_desc = + | ELF_header + | ELF_progtab + | ELF_shtab + | ELF_section_strtab + | ELF_symbol_strtab + | Symtab_data of elf32_sym + | Symtab_function of elf32_sym + | Data_symbol of elf32_sym + | Function_symbol of elf32_sym + | Zero_symbol + | Stub of string + | Jumptable + | Float_literal of float + | Padding + | Unknown of string + +(** This framework is carried along while analyzing the whole ELF file. +*) +type e_framework = { + elf: elf; + log: log_entry list; + (* + chkd_syms: SymCoverage.t; + chkd_bytes_diet: ELFCoverage.t; + *) + (** Every time a chunk of the ELF file is checked, it is added to this list. + The first two fields are the start and stop offsets, the third is an + alignment constraint, the last is a description. *) + chkd_bytes_list: (int32 * int32 * int * byte_chunk_desc) list; +} + +module PosOT = struct + type t = positive + let compare = Pervasives.compare +end + +module PosMap = Map.Make(PosOT) + +(** This framework is carried along while analyzing one .sdump file, which + may contain multiple functions. *) +type s_framework = { + ef: e_framework; + program: Asm.program; + (** Maps every CompCert ident to a string. This will not be the exact name of + the symbol in the ELF file though: CompCert does some mangling for + variadic functions, and some linkers do some versioning in their symbols. + *) + ident_to_name: (ident, string) Hashtbl.t; + (** Maps a CompCert ident to a list of candidates symbol indices. We can only + try to match symbols by name until we begin the analysis, so multiple + static symbols might match a given name. The list will be narrowed down + as we learn more about the contents of the symbol. + *) + ident_to_sym_ndx: (int list) PosMap.t; + (** CompCert generates stubs for some functions, which we will aggregate as we + discover them. *) + stub_ident_to_vaddr: int32 PosMap.t; + (** This structure is imported from CompCert's .sdump, and describes each + atom. *) + atoms: (ident, C2C.atom_info) Hashtbl.t; +} + +(** This framework is carried while analyzing a single function. *) +type f_framework = { + sf: s_framework; + (** The symbol index of the current function. *) + this_sym_ndx: int; + (** The CompCert ident of the current function. *) + this_ident: ident; + (** A mapping from local labels to virtual addresses. *) + label_to_vaddr: int32 PosMap.t; + (** A list of all the labels encountered while processing the body. *) + label_list: label list; +} + +(** A few lenses that prove useful for manipulating frameworks. +*) + +let sf_ef: (s_framework, e_framework) Lens.t = { + get = (fun sf -> sf.ef); + set = (fun ef sf -> { sf with ef = ef }); +} + +let ff_sf: (f_framework, s_framework) Lens.t = { + get = (fun ff -> ff.sf); + set = (fun sf ff -> { ff with sf = sf }); +} + +let ff_ef = ff_sf |-- sf_ef + +let log = { + get = (fun ef -> ef.log); + set = (fun l ef -> { ef with log = l }); +} +(* +let chkd_syms = { + get = (fun ef -> ef.chkd_syms); + set = (fun s ef -> { ef with chkd_syms = s }); +} +*) + +let ident_to_sym_ndx = { + get = (fun sf -> sf.ident_to_sym_ndx); + set = (fun i sf -> { sf with ident_to_sym_ndx = i }); +} + +let stub_ident_to_vaddr = { + get = (fun sf -> sf.stub_ident_to_vaddr); + set = (fun i sf -> { sf with stub_ident_to_vaddr = i }); +} + +(** Adds a range to the checked bytes list. +*) +let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc) + (efw: e_framework): e_framework = + assert (0l <= start && 0l < length); + let stop = Int32.(sub (add start length) 1l) in + { + efw with + (*chkd_bytes_diet = ELFCoverage.r_add start stop efw.chkd_bytes_diet;*) + chkd_bytes_list = + (* Float constants can appear several times in the code, we don't + want to add them multiple times *) + if (List.exists + (fun (a, b, _, _) -> a = start && b = stop) + efw.chkd_bytes_list) + then efw.chkd_bytes_list + else (start, stop, align, bcd) :: efw.chkd_bytes_list; + } + +(** Some useful combinators to make it all work. +*) + +(* external ( >>> ) : 'a -> ('a -> 'b) -> 'b = "%revapply" *) +let ( >>> ) (a: 'a) (f: 'a -> 'b): 'b = f a + +let ( >>? ) (a: 'a on_success) (f: 'a -> 'b): 'b on_success = + match a with + | ERR(s) -> ERR(s) + | OK(x) -> OK(f x) + +let ( >>= ) (a: 'a on_success) (f: 'a -> 'b on_success): 'b on_success = + match a with + | ERR(s) -> ERR(s) + | OK(x) -> f x + +let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b on_success) + (arg: 'a): 'a on_success = + let focus = arg |. lens in + match transf focus with + | OK(res) -> OK((lens ^= res) arg) + | ERR(s) -> ERR(s) + +(** Finally, some printers. +*) + +let string_of_log_entry = function +| LOG(s) -> s +| ERROR(s) -> "ERROR: " ^ s +| WARNING(s) -> "WARNING: " ^ s +| DEBUG(s) -> "DEBUG: " ^ s + +let string_of_byte_chunk_desc = function +| ELF_header -> "ELF header" +| ELF_progtab -> "ELF program header table" +| ELF_shtab -> "ELF section header table" +| ELF_section_strtab -> "ELF section string table" +| ELF_symbol_strtab -> "ELF symbol string table" +| Symtab_data(s) -> "Data symbol table entry: " ^ s.st_name +| Symtab_function(s) -> "Function symbol table entry: " ^ s.st_name +| Data_symbol(s) -> "Data symbol: " ^ s.st_name +| Function_symbol(s) -> "Function symbol: " ^ s.st_name +| Zero_symbol -> "Symbol 0" +| Stub(s) -> "Stub for: " ^ s +| Jumptable -> "Jump table" +| Float_literal(f) -> "Float literal: " ^ string_of_float f +| Padding -> "Padding" +| Unknown(s) -> " ??? " ^ s + + diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml new file mode 100644 index 0000000..2fe29b0 --- /dev/null +++ b/checklink/Fuzz.ml @@ -0,0 +1,155 @@ +open Check +open ELF_parsers +open ELF_types +open Frameworks +open Library + +let string_of_byte = Printf.sprintf "0x%02x" + +let full_range_of_byte elfmap byte = + let byte = int_int32 byte in + List.find (fun (a, b, _, _) -> a <= byte && byte <= b) elfmap + +let range_of_byte elfmap byte = + let (_, _, _, r) = full_range_of_byte elfmap byte in + r + +let fuzz_check elfmap bs byte old sdumps = + let (str, _, _) = bs in + try ( + let elf = read_elf_bs bs in + try ( + let efw = check_elf elf sdumps in + try ( + let _ = List.find (function ERROR(s) -> true | _ -> false) efw.log in + () + ) with + | Not_found -> + print_endline ( + string_of_int32 (int_int32 byte) ^ " <- " ^ + string_of_byte (Char.code str.[byte]) ^ " (was " ^ + string_of_byte (Char.code old) ^ ") - " ^ + string_of_byte_chunk_desc (range_of_byte elfmap byte) + ) + ) with + | e -> () + ) with + | e -> () + +let ok_fuzz elfmap str byte fuzz = + let (a, b, _, r) = full_range_of_byte elfmap byte in + let a = int32_int a in + let b = int32_int b in + let old = Char.code str.[byte] in + let fuz = Char.code fuzz in + match r with + | ELF_header -> + not (List.mem byte + [ + 0x18; 0x19; 0x1a; 0x1b; (* e_entry *) + 0x1c; 0x1d; 0x1e; 0x1f; (* e_phoff *) + 0x24; 0x25; 0x26; 0x27; (* e_flags *) + 0x2c; 0x2d (* e_phnum *) + ] + ) + | ELF_progtab -> false + | ELF_shtab -> false + | ELF_section_strtab -> false + | ELF_symbol_strtab -> false + | Symtab_data(_) -> + (* False positive: switching from/to STT_NOTYPE *) + not (byte = a + 12 + && ((old land 0xf = 0) || (fuz land 0xf = 0)) + ) + | Symtab_function(_) -> true + | Data_symbol(_) -> + (* False positive: 0. becomes -0. *) + not ( + (byte + 7 <= b) + && (fuz = 0x80) + && (Char.code str.[byte + 0] = 0x00) + && (Char.code str.[byte + 1] = 0x00) + && (Char.code str.[byte + 2] = 0x00) + && (Char.code str.[byte + 3] = 0x00) + && (Char.code str.[byte + 4] = 0x00) + && (Char.code str.[byte + 5] = 0x00) + && (Char.code str.[byte + 6] = 0x00) + && (Char.code str.[byte + 7] = 0x00) + ) + | Function_symbol(_) -> + let opcode = Char.code str.[byte - 3] in + (* False positive: rlwinm with bitmask 0 31 = bitmask n (n - 1) *) + not (0x54 <= opcode && opcode <= 0x57 && old = 0x3E + && (fuz = 0x40 || fuz = 0x82 || fuz = 0xc4)) + | Zero_symbol -> false + | Stub(_) -> true + | Jumptable -> true + | Float_literal(_) -> + (* False positive: 0. becomes -0. *) + not ( + (byte = a) + && (fuz = 0x80) + && (Char.code str.[byte + 0] = 0x00) + && (Char.code str.[byte + 1] = 0x00) + && (Char.code str.[byte + 2] = 0x00) + && (Char.code str.[byte + 3] = 0x00) + && (Char.code str.[byte + 4] = 0x00) + && (Char.code str.[byte + 5] = 0x00) + && (Char.code str.[byte + 6] = 0x00) + && (Char.code str.[byte + 7] = 0x00) + ) + | Padding -> false (* padding may be non-null *) + | Unknown(_) -> false + +let fuzz_byte str byte_ndx = + let rand = Char.chr (Random.int 255) in (* [0 - 254] *) + if rand = str.[byte_ndx] (* if we picked a byte equal to the current *) + then Char.chr 255 (* then replace with byte 255 *) + else rand (* else replace with the byte we picked *) + +let rec find_byte_to_fuzz elfmap str byterange = + let byte = Random.int byterange in + let fuzz = fuzz_byte str byte in + if ok_fuzz elfmap str byte fuzz + then (byte, fuzz) + else find_byte_to_fuzz elfmap str byterange + +let get_elfmap elffilename = + let ic = open_in (elffilename ^ ".elfmap") in + let elfmap = input_value ic in + close_in ic; + elfmap + +let fuzz_loop elffilename sdumps = + let elfmap = get_elfmap elffilename in + let (str, ofs, len) = Bitstring.bitstring_of_file elffilename in + let rec fuzz_loop_aux () = + let (byte, fuzz) = find_byte_to_fuzz elfmap str (len/8) in + let str' = String.copy str in + str'.[byte] <- fuzz; + fuzz_check elfmap (str', ofs, len) byte str.[byte] sdumps; + fuzz_loop_aux () + in fuzz_loop_aux () +(* + let fuzz_all elffilename sdumps = + let elfmap = get_elfmap elffilename in + let (str, ofs, len) = Bitstring.bitstring_of_file elffilename in + let rec fuzz_all_aux current limit = + if current = limit + then () + else ( + if ok_fuzz elfmap current + then ( + let str' = String.copy str in + fuzz_byte str' current; + let msg = string_of_int32 (int_int32 current) ^ " <- " ^ + string_of_byte (Char.code str'.[current]) ^ " (was " ^ + string_of_byte (Char.code str.[current]) ^ ") - " ^ + string_of_elf_range (range_of_byte elfmap current) + in + fuzz_check msg (str', ofs, len) sdumps + ); + fuzz_all_aux (current + 1) limit + ) + in fuzz_all_aux 0 (len/8) +*) diff --git a/checklink/Lens.ml b/checklink/Lens.ml new file mode 100644 index 0000000..4335933 --- /dev/null +++ b/checklink/Lens.ml @@ -0,0 +1,32 @@ +type ('a, 'b) t = { + get: 'a -> 'b; + set: 'b -> 'a -> 'a; +} + +let ( |- ) f g x = g (f x) + +let modify l f a = + let oldval = l.get a in + let newval = f oldval in + l.set newval a + +let compose l1 l2 = { + get = l2.get |- l1.get; + set = l1.set |- modify l2 +} + +let _get a l = l.get a + +let _set v a l = l.set v a + +let _modify f l = modify l f + +let (|.) = _get + +let (^=) l v = fun a -> _set v a l + +let (^%=) l f = _modify f l + +let (|--) l1 l2 = compose l2 l1 + +let (--|) = compose diff --git a/checklink/Library.ml b/checklink/Library.ml new file mode 100644 index 0000000..dbe7b46 --- /dev/null +++ b/checklink/Library.ml @@ -0,0 +1,127 @@ +open BinInt +open BinPos + +type bitstring = Bitstring.bitstring + +let from_some = function +| Some(x) -> x +| None -> raise Not_found + +type 'a on_success = + | OK of 'a + | ERR of string + +let is_ok: 'a on_success -> bool = function +| OK(_) -> true +| ERR(_) -> false + +let from_ok = function +| OK(x) -> x +| ERR(_) -> raise Not_found + +let filter_ok l = List.(map from_ok (filter is_ok l)) + +external id : 'a -> 'a = "%identity" + +(** Checks for existence of an array element satisfying a condition, and returns + its index if it exists. +*) +let array_exists (cond: 'a -> bool) (arr: 'a array): int option = + let rec array_exists_aux ndx = + if ndx < 0 + then None + else if cond arr.(ndx) + then Some ndx + else array_exists_aux (ndx - 1) + in array_exists_aux (Array.length arr - 1) + +(* Functions for safely converting between numeric types *) + +exception Integer_overflow + +let int32_int (i32: int32): int = + let i = Int32.to_int i32 in + if i32 = Int32.of_int i + then i + else raise Integer_overflow + +let int_int32 = Int32.of_int + +(* Can only return positive numbers 0 <= res < 2^31 *) +let positive_int32 p = + let rec positive_int32_unsafe = function + | Coq_xI(p) -> Int32.(add (shift_left (positive_int32_unsafe p) 1) 1l) + | Coq_xO(p) -> Int32.(shift_left (positive_int32_unsafe p) 1) + | Coq_xH -> 1l + in + let res = positive_int32_unsafe p in + if res >= 0l + then res + else raise Integer_overflow + +(* This allows for 1 bit of overflow, effectively returning a negative *) +let rec positive_int32_lax = function +| Coq_xI(p) -> + let acc = positive_int32_lax p in + if acc < 0l + then raise Integer_overflow + else Int32.(add (shift_left acc 1) 1l) +| Coq_xO(p) -> + let acc = positive_int32_lax p in + if acc < 0l + then raise Integer_overflow + else Int32.shift_left acc 1 +| Coq_xH -> 1l + +let z_int32 = function +| Z0 -> 0l +| Zpos(p) -> positive_int32 p +| Zneg(p) -> Int32.neg (positive_int32 p) + +let z_int32_lax = function +| Z0 -> 0l +| Zpos(p) -> positive_int32_lax p +| Zneg(p) -> raise Integer_overflow + +let z_int z = int32_int (z_int32 z) + +let z_int_lax z = int32_int (z_int32_lax z) + +(* Some more printers *) + +let string_of_array string_of_elt sep a = + "[\n" ^ + fst ( + Array.fold_left + ( + fun accu elt -> + let (str, ndx) = accu in + (str ^ (if ndx > 0 then sep else "") ^ string_of_int ndx ^ ": " ^ + string_of_elt elt, ndx + 1) + ) + ("", 0) a + ) ^ + "\n]" + +let string_of_list string_of_elt sep l = + String.concat sep (List.map string_of_elt l) + +let string_of_bitstring bs = + let rec string_of_bitset_aux bs = + bitmatch bs with + | { bit : 1 : int ; + rest : -1 : bitstring } -> + (if bit + then "1" + else "0") ^ (string_of_bitset_aux rest) + | { _ } -> "" + in string_of_bitset_aux bs + +(* To print addresses/offsets *) +let string_of_int32 = Printf.sprintf "0x%08lx" +(* To print counts/indices *) +let string_of_int32i = Int32.to_string + +let string_of_positive p = string_of_int32i (positive_int32 p) + +let string_of_z z = string_of_int32 (z_int32 z) diff --git a/checklink/PPC_parsers.ml b/checklink/PPC_parsers.ml new file mode 100644 index 0000000..ffbbc2f --- /dev/null +++ b/checklink/PPC_parsers.ml @@ -0,0 +1,399 @@ +open Library +open PPC_types + +let parse_instr bs = + bitmatch bs with + | { 31:6; d:5; a:5; b:5; oe:1; 266:9; rc:1 } + -> ADDx(d, a, b, oe, rc) + | { 31:6; d:5; a:5; b:5; oe:1; 10:9; rc:1 } + -> ADDCx(d, a, b, oe, rc) + | { 31:6; d:5; a:5; b:5; oe:1; 138:9; rc:1 } + -> ADDEx(d, a, b, oe, rc) + | { 14:6; d:5; a:5; simm:16:bitstring } + -> ADDI(d, a, simm) + | { 12:6; d:5; a:5; simm:16:bitstring } + -> ADDIC(d, a, simm) + | { 13:6; d:5; a:5; simm:16:bitstring } + -> ADDIC_(d, a, simm) + | { 15:6; d:5; a:5; simm:16 } + -> ADDIS(d, a, simm) + | { 31:6; d:5; a:5; 0:5; oe:1; 234:9; rc:1 } + -> ADDMEx(d, a, oe, rc) + | { 31:6; d:5; a:5; 0:5; oe:1; 202:9; rc:1 } + -> ADDZEx(d, a, oe, rc) + | { 31:6; s:5; a:5; b:5; 28:10; rc:1 } + -> ANDx(s, a, b, rc) + | { 31:6; s:5; a:5; b:5; 60:10; rc:1 } + -> ANDCx(s, a, b, rc) + | { 28:6; s:5; a:5; uimm:16 } + -> ANDI_(s, a, uimm) + | { 29:6; s:5; a:5; uimm:16 } + -> ANDIS_(s, a, uimm) + | { 18:6; li:24:bitstring; aa:1; lk:1 } + -> Bx(li, aa, lk) + | { 16:6; bo:5:bitstring; bi:5; bd:14:bitstring; aa:1; lk:1 } + -> BCx(bo, bi, bd, aa, lk) + | { 19:6; bo:5:bitstring; bi:5; 0:5; 528:10; lk:1 } + -> BCCTRx(bo, bi, lk) + | { 19:6; bo:5:bitstring; bi:5; 0:5; 16:10; lk:1 } + -> BCLRx(bo, bi, lk) + | { 31:6; crfD:3; false:1; l:1; a:5; b:5; 0:10; false:1 } + -> CMP(crfD, l, a, b) + | { 11:6; crfD:3; false:1; l:1; a:5; simm:16:bitstring } + -> CMPI(crfD, l, a, simm) + | { 31:6; crfD:3; false:1; l:1; a:5; b:5; 32:10; false:1 } + -> CMPL(crfD, l, a, b) + | { 10:6; crfD:3; false:1; l:1; a:5; uimm:16 } + -> CMPLI(crfD, l, a, uimm) + | { 31:6; s:5; a:5; 0:5; 26:10; rc:1 } + -> CNTLZWx(s, a, rc) + | { 19:6; crbD:5; crbA:5; crbB:5; 257:10; false:1 } + -> CRAND(crbD, crbA, crbB) + | { 19:6; crbD:5; crbA:5; crbB:5; 129:10; false:1 } + -> CRANDC(crbD, crbA, crbB) + | { 19:6; crbD:5; crbA:5; crbB:5; 289:10; false:1 } + -> CREQV(crbD, crbA, crbB) + | { 19:6; crbD:5; crbA:5; crbB:5; 225:10; false:1 } + -> CRNAND(crbD, crbA, crbB) + | { 19:6; crbD:5; crbA:5; crbB:5; 33:10; false:1 } + -> CRNOR(crbD, crbA, crbB) + | { 19:6; crbD:5; crbA:5; crbB:5; 449:10; false:1 } + -> CROR(crbD, crbA, crbB) + | { 19:6; crbD:5; crbA:5; crbB:5; 417:10; false:1 } + -> CRORC(crbD, crbA, crbB) + | { 19:6; crbD:5; crbA:5; crbB:5; 193:10; false:1 } + -> CRXOR(crbD, crbA, crbB) + | { 31:6; 0:5; a:5; b:5; 758:10; false:1 } + -> DCBA(a, b) + | { 31:6; 0:5; a:5; b:5; 86:10; false:1 } + -> DCBF(a, b) + | { 31:6; 0:5; a:5; b:5; 470:10; false:1 } + -> DCBI(a, b) + | { 31:6; 0:5; a:5; b:5; 54:10; false:1 } + -> DCBST(a, b) + | { 31:6; 0:5; a:5; b:5; 278:10; false:1 } + -> DCBT(a, b) + | { 31:6; 0:5; a:5; b:5; 246:10; false:1 } + -> DCBTST(a, b) + | { 31:6; 0:5; a:5; b:5; 1014:10; false:1 } + -> DCBZ(a, b) + | { 31:6; d:5; a:5; b:5; oe:1; 491:9; rc:1 } + -> DIVWx(d, a, b, oe, rc) + | { 31:6; d:5; a:5; b:5; oe:1; 459:9; rc:1 } + -> DIVWUx(d, a, b, oe, rc) + | { 31:6; d:5; a:5; b:5; 310:10; false:1 } + -> ECIWX(d, a, b) + | { 31:6; s:5; a:5; b:5; 438:10; false:1 } + -> ECOWX(s, a, b) + | { 31:6; 0:5; 0:5; 0:5; 854:10; false:1 } + -> EIEIO + | { 31:6; s:5; a:5; b:5; 284:10; rc:1 } + -> EQVx(s, a, b, rc) + | { 31:6; s:5; a:5; 0:5; 954:10; rc:1 } + -> EXTSBx(s, a, rc) + | { 31:6; s:5; a:5; 0:5; 922:10; rc:1 } + -> EXTSHx(s, a, rc) + | { 63:6; d:5; 0:5; b:5; 264:10; rc:1 } + -> FABSx(d, b, rc) + | { 63:6; d:5; a:5; b:5; 0:5; 21:5; rc:1 } + -> FADDx(d, a, b, rc) + | { 59:6; d:5; a:5; b:5; 0:5; 21:5; rc:1 } + -> FADDSx(d, a, b, rc) + | { 63:6; crfD:3; 0:2; a:5; b:5; 32:10; false:1 } + -> FCMPO(crfD, a, b) + | { 63:6; crfD:3; 0:2; a:5; b:5; 0:10; false:1 } + -> FCMPU(crfD, a, b) + | { 63:6; d:5; 0:5; b:5; 14:10; rc:1 } + -> FCTIWx(d, b, rc) + | { 63:6; d:5; 0:5; b:5; 15:10; rc:1 } + -> FCTIWZx(d, b, rc) + | { 63:6; d:5; a:5; b:5; 0:5; 18:5; rc:1 } + -> FDIVx(d, a, b, rc) + | { 59:6; d:5; a:5; b:5; 0:5; 18:5; rc:1 } + -> FDIVSx(d, a, b, rc) + | { 63:6; d:5; a:5; b:5; c:5; 29:5; rc:1 } + -> FMADDx(d, a, b, c, rc) + | { 59:6; d:5; a:5; b:5; c:5; 29:5; rc:1 } + -> FMADDSx(d, a, b, c, rc) + | { 63:6; d:5; 0:5; b:5; 72:10; rc:1 } + -> FMRx(d, b, rc) + | { 63:6; d:5; a:5; b:5; c:5; 28:5; rc:1 } + -> FMSUBx(d, a, b, c, rc) + | { 59:6; d:5; a:5; b:5; c:5; 28:5; rc:1 } + -> FMSUBSx(d, a, b, c, rc) + | { 63:6; d:5; a:5; 0:5; c:5; 25:5; rc:1 } + -> FMULx(d, a, c, rc) + | { 59:6; d:5; a:5; 0:5; c:5; 25:5; rc:1 } + -> FMULSx(d, a, c, rc) + | { 63:6; d:5; 0:5; b:5; 136:10; rc:1 } + -> FNABSx(d, b, rc) + | { 63:6; d:5; 0:5; b:5; 40:10; rc:1 } + -> FNEGx(d, b, rc) + | { 63:6; d:5; a:5; b:5; c:5; 31:5; rc:1 } + -> FNMADDx(d, a, b, c, rc) + | { 59:6; d:5; a:5; b:5; c:5; 31:5; rc:1 } + -> FNMADDSx(d, a, b, c, rc) + | { 63:6; d:5; a:5; b:5; c:5; 30:5; rc:1 } + -> FNMSUBx(d, a, b, c, rc) + | { 59:6; d:5; a:5; b:5; c:5; 30:5; rc:1 } + -> FNMSUBSx(d, a, b, c, rc) + | { 59:6; d:5; 0:5; b:5; 0:5; 24:5; rc:1 } + -> FRESx(d, b, rc) + | { 63:6; d:5; 0:5; b:5; 12:10; rc:1 } + -> FRSPx(d, b, rc) + | { 63:6; d:5; 0:5; b:5; 0:5; 22:5; rc:1 } + -> FRSQRTEx(d, b, rc) + | { 63:6; d:5; a:5; b:5; c:5; 23:5; rc:1 } + -> FSELx(d, a, b, c, rc) + | { 63:6; d:5; 0:5; b:5; 0:5; 22:5; rc:1 } + -> FSQRTx(d, b, rc) + | { 59:6; d:5; 0:5; b:5; 0:5; 22:5; rc:1 } + -> FSQRTSx(d, b, rc) + | { 63:6; d:5; a:5; b:5; 0:5; 20:5; rc:1 } + -> FSUBx(d, a, b, rc) + | { 59:6; d:5; a:5; b:5; 0:5; 20:5; rc:1 } + -> FSUBSx(d, a, b, rc) + | { 31:6; 0:5; a:5; b:5; 982:10; false:1 } + -> ICBI(a, b) + | { 19:6; 0:5; 0:5; 0:5; 150:10; false:1 } + -> ISYNC + | { 34:6; d:5; a:5; dd:16:bitstring } + -> LBZ(d, a, dd) + | { 35:6; d:5; a:5; dd:16:bitstring } + -> LBZU(d, a, dd) + | { 31:6; d:5; a:5; b:5; 119:10; false:1 } + -> LBZUX(d, a, b) + | { 31:6; d:5; a:5; b:5; 87:10; false:1 } + -> LBZX(d, a, b) + | { 50:6; d:5; a:5; dd:16:bitstring } + -> LFD(d, a, dd) + | { 51:6; d:5; a:5; dd:16:bitstring } + -> LFDU(d, a, dd) + | { 31:6; d:5; a:5; b:5; 631:10; false:1 } + -> LFDUX(d, a, b) + | { 31:6; d:5; a:5; b:5; 599:10; false:1 } + -> LFDX(d, a, b) + | { 48:6; d:5; a:5; dd:16:bitstring } + -> LFS(d, a, dd) + | { 49:6; d:5; a:5; dd:16:bitstring } + -> LFSU(d, a, dd) + | { 31:6; d:5; a:5; b:5; 567:10; false:1 } + -> LFSUX(d, a, b) + | { 31:6; d:5; a:5; b:5; 535:10; false:1 } + -> LFSX(d, a, b) + | { 42:6; d:5; a:5; dd:16:bitstring } + -> LHA(d, a, dd) + | { 43:6; d:5; a:5; dd:16:bitstring } + -> LHAU(d, a, dd) + | { 31:6; d:5; a:5; b:5; 375:10; false:1 } + -> LHAUX(d, a, b) + | { 31:6; d:5; a:5; b:5; 343:10; false:1 } + -> LHAX(d, a, b) + | { 31:6; d:5; a:5; b:5; 790:10; false:1 } + -> LHBRX(d, a, b) + | { 40:6; d:5; a:5; dd:16:bitstring } + -> LHZ(d, a, dd) + | { 41:6; d:5; a:5; dd:16:bitstring } + -> LHZU(d, a, dd) + | { 31:6; d:5; a:5; b:5; 311:10; false:1 } + -> LHZUX(d, a, b) + | { 31:6; d:5; a:5; b:5; 279:10; false:1 } + -> LHZX(d, a, b) + | { 46:6; d:5; a:5; dd:16 } + -> LMW(d, a, dd) + | { 31:6; d:5; a:5; nb:5; 597:10; false:1 } + -> LSWI(d, a, nb) + | { 31:6; d:5; a:5; b:5; 533:10; false:1 } + -> LSWX(d, a, b) + | { 31:6; d:5; a:5; b:5; 20:10; false:1 } + -> LWARX(d, a, b) + | { 31:6; d:5; a:5; b:5; 534:10; false:1 } + -> LWBRX(d, a, b) + | { 32:6; d:5; a:5; dd:16:bitstring } + -> LWZ(d, a, dd) + | { 33:6; d:5; a:5; dd:16:bitstring } + -> LWZU(d, a, dd) + | { 31:6; d:5; a:5; b:5; 55:10; false:1 } + -> LWZUX(d, a, b) + | { 31:6; d:5; a:5; b:5; 23:10; false:1 } + -> LWZX(d, a, b) + | { 19:6; crfD:3; 0:2; crfS:3; 0:2; 0:5; 0:10; false:1 } + -> MCRF(crfD, crfS) + | { 63:6; crfD:3; 0:2; crfS:3; 0:2; 0:5; 64:10; false:1 } + -> MCRFS(crfD, crfS) + | { 31:6; crfD:3; 0:2; 0:5; 0:5; 0:10; false:1 } + -> MCRXR(crfD) + | { 31:6; d:5; 0:5; 0:5; 19:10; false:1 } + -> MFCR(d) + | { 63:6; d:5; 0:5; 0:5; 583:10; rc:1 } + -> MFFSx(d, rc) + | { 31:6; d:5; 0:5; 0:5; 83:10; false:1 } + -> MFMSR(d) + | { 31:6; d:5; spr:10:bitstring; 339:10; false:1 } + -> MFSPR(d, spr) + | { 31:6; d:5; false:1; sr:4; 0:5; 595:10; false:1 } + -> MFSR(d, sr) + | { 31:6; d:5; 0:5; b:5; 659:10; false:1 } + -> MFSRIN(d, b) + | { 31:6; d:5; tbr:10; 371:10; false:1 } + -> MFTB(d, tbr) + | { 31:6; s:5; false:1; crm:8; false:1; 144:10; false:1 } + -> MTCRF(s, crm) + | { 63:6; crbD:5; 0:5; 0:5; 70:10; rc:1 } + -> MTFSB0x(crbD, rc) + | { 63:6; crbD:5; 0:5; 0:5; 38:10; rc:1 } + -> MTFSB1x(crbD, rc) + | { 63:6; false:1; fm:8; false:1; b:5; 711:10; rc:1 } + -> MTFSF(fm, b, rc) + | { 63:6; crfD:3; 0:2; 0:5; imm:4; false:1; 134:10; rc:1 } + -> MTFSFIx(crfD, imm, rc) + | { 31:6; s:5; 0:5; 0:5; 146:10; false:1 } + -> MTMSR(s) + | { 31:6; s:5; spr:10:bitstring; 467:10; false:1 } + -> MTSPR(s, spr) + | { 31:6; s:5; false:1; sr:4; 0:5; 210:10; false:1 } + -> MTSR(s, sr) + | { 31:6; s:5; 0:5; b:5; 242:10; false:1 } + -> MTSRIN(s, b) + | { 31:6; d:5; a:5; b:5; false:1; 75:9; rc:1 } + -> MULHWx(d, a, b, rc) + | { 31:6; d:5; a:5; b:5; false:1; 11:9; rc:1 } + -> MULHWUx(d, a, b, rc) + | { 7:6; d:5; a:5; simm:16:bitstring } + -> MULLI(d, a, simm) + | { 31:6; id:5; a:5; b:5; oe:1; 235:9; rc:1 } + -> MULLWx(id, a, b, oe, rc) + | { 31:6; s:5; a:5; b:5; 476:10; rc:1 } + -> NANDx(s, a, b, rc) + | { 31:6; d:5; a:5; 0:5; oe:1; 104:9; rc:1 } + -> NEGx(d, a, oe, rc) + | { 31:6; s:5; a:5; b:5; 124:10; rc:1 } + -> NORx(s, a, b, rc) + | { 31:6; s:5; a:5; b:5; 444:10; rc:1 } + -> ORx(s, a, b, rc) + | { 31:6; s:5; a:5; b:5; 412:10; rc:1 } + -> ORCx(s, a, b, rc) + | { 24:6; s:5; a:5; uimm:16 } + -> ORI(s, a, uimm) + | { 25:6; s:5; a:5; uimm:16 } + -> ORIS(s, a, uimm) + | { 19:6; 0:5; 0:5; 0:5; 50:10; false:1 } + -> RFI + | { 20:6; s:5; a:5; sh:5; mb:5; me:5; rc:1 } + -> RLWIMIx(s, a, sh, mb, me, rc) + | { 21:6; s:5; a:5; sh:5; mb:5; me:5; rc:1 } + -> RLWINMx(s, a, sh, mb, me, rc) + | { 23:6; s:5; a:5; b:5; mb:5; me:5; rc:1 } + -> RLWNMx(s, a, b, mb, me, rc) + | { 17:6; 0:5; 0:5; 0:14; true:1; false:1 } + -> SC + | { 31:6; s:5; a:5; b:5; 24:10; rc:1 } + -> SLWx(s, a, b, rc) + | { 31:6; s:5; a:5; b:5; 792:10; rc:1 } + -> SRAWx(s, a, b, rc) + | { 31:6; s:5; a:5; sh:5; 824:10; rc:1 } + -> SRAWIx(s, a, sh, rc) + | { 31:6; s:5; a:5; b:5; 536:10; rc:1 } + -> SRWx(s, a, b, rc) + | { 38:6; s:5; a:5; dd:16:bitstring } + -> STB(s, a, dd) + | { 39:6; s:5; a:5; dd:16:bitstring } + -> STBU(s, a, dd) + | { 31:6; s:5; a:5; b:5; 247:10; false:1 } + -> STBUX(s, a, b) + | { 31:6; s:5; a:5; b:5; 215:10; false:1 } + -> STBX(s, a, b) + | { 54:6; s:5; a:5; dd:16:bitstring } + -> STFD(s, a, dd) + | { 55:6; s:5; a:5; dd:16:bitstring } + -> STFDU(s, a, dd) + | { 31:6; s:5; a:5; b:5; 759:10; false:1 } + -> STFDUX(s, a, b) + | { 31:6; s:5; a:5; b:5; 727:10; false:1 } + -> STFDX(s, a, b) + | { 31:6; s:5; a:5; b:5; 983:10; false:1 } + -> STFIWX(s, a, b) + | { 52:6; s:5; a:5; dd:16:bitstring } + -> STFS(s, a, dd) + | { 53:6; s:5; a:5; dd:16:bitstring } + -> STFSU(s, a, dd) + | { 31:6; s:5; a:5; b:5; 695:10; false:1 } + -> STFSUX(s, a, b) + | { 31:6; s:5; a:5; b:5; 663:10; false:1 } + -> STFSX(s, a, b) + | { 44:6; s:5; a:5; dd:16:bitstring } + -> STH(s, a, dd) + | { 31:6; s:5; a:5; b:5; 918:10; false:1 } + -> STHBRX(s, a, b) + | { 45:6; s:5; a:5; dd:16:bitstring } + -> STHU(s, a, dd) + | { 31:6; s:5; a:5; b:5; 439:10; false:1 } + -> STHUX(s, a, b) + | { 31:6; s:5; a:5; b:5; 407:10; false:1 } + -> STHX(s, a, b) + | { 47:6; s:5; a:5; dd:16 } + -> STMW(s, a, dd) + | { 31:6; s:5; a:5; nb:5; 725:10; false:1 } + -> STSWI(s, a, nb) + | { 31:6; s:5; a:5; b:5; 661:10; false:1 } + -> STSWX(s, a, b) + | { 36:6; s:5; a:5; dd:16:bitstring } + -> STW(s, a, dd) + | { 31:6; s:5; a:5; b:5; 662:10; false:1 } + -> STWBRX(s, a, b) + | { 31:6; s:5; a:5; b:5; 150:10; false:1 } + -> STWCX_(s, a, b) + | { 37:6; s:5; a:5; dd:16:bitstring } + -> STWU(s, a, dd) + | { 31:6; s:5; a:5; b:5; 183:10; false:1 } + -> STWUX(s, a, b) + | { 31:6; s:5; a:5; b:5; 151:10; false:1 } + -> STWX(s, a, b) + | { 31:6; d:5; a:5; b:5; oe:1; 40:9; rc:1 } + -> SUBFx(d, a, b, oe, rc) + | { 31:6; d:5; a:5; b:5; oe:1; 8:9; rc:1 } + -> SUBFCx(d, a, b, oe, rc) + | { 31:6; d:5; a:5; b:5; oe:1; 136:9; rc:1 } + -> SUBFEx(d, a, b, oe, rc) + | { 8:6; d:5; a:5; simm:16:bitstring } + -> SUBFIC(d, a, simm) + | { 31:6; d:5; a:5; 0:5; oe:1; 232:9; rc:1 } + -> SUBFMEx(d, a, oe, rc) + | { 31:6; d:5; a:5; 0:5; oe:1; 200:9; rc:1 } + -> SUBFZEx(d, a, oe, rc) + | { 31:6; 0:5; 0:5; 0:5; 598:10; false:1 } + -> SYNC + | { 31:6; 0:5; 0:5; 0:5; 370:10; false:1 } + -> TLBIA + | { 31:6; 0:5; 0:5; b:5; 306:10; false:1 } + -> TLBIE(b) + | { 31:6; 0:5; 0:5; 0:5; 566:10; false:1 } + -> TLBSYNC + | { 31:6; t:5:bitstring; a:5; b:5; 4:10; false:1 } + -> TW(t, a, b) + | { 3:6; t:5:bitstring; a:5; simm:16 } + -> TWI(t, a, simm) + | { 31:6; s:5; a:5; b:5; 316:10; rc:1 } + -> XORx(s, a, b, rc) + | { 26:6; s:5; a:5; uimm:16 } + -> XORI(s, a, uimm) + | { 27:6; s:5; a:5; uimm:16 } + -> XORIS(s, a, uimm) + | { bits:32:bitstring } + -> UNKNOWN(bits) + +exception Wrong_code_size + +let rec parse_code_as_list bs = + bitmatch bs with + | { instr:32:bitstring; rest:-1:bitstring } -> + parse_instr instr :: parse_code_as_list rest + | { rest:-1:bitstring } -> + if Bitstring.bitstring_length rest = 0 + then [] + else raise Wrong_code_size + +let parse_nth_instr bs n = parse_instr (Bitstring.subbitstring bs (n * 32) 32) + +let parse_code_as_array (bs: bitstring) (num: int): instr array = + Array.init num (parse_nth_instr bs) diff --git a/checklink/PPC_printers.ml b/checklink/PPC_printers.ml new file mode 100644 index 0000000..5aa9a04 --- /dev/null +++ b/checklink/PPC_printers.ml @@ -0,0 +1,203 @@ +open Library +open PPC_types + +let string_of_eireg r = "r" ^ string_of_int r + +let string_of_efreg f = "fr" ^ string_of_int f + +let string_of_bool b = if b then "1" else "0" + +let string_of_instr = function +| ADDx (r0, r1, r2, b3, b4) -> "ADDx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| ADDCx (r0, r1, r2, b3, b4) -> "ADDCx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| ADDEx (r0, r1, r2, b3, b4) -> "ADDEx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| ADDI (r0, r1, b2) -> "ADDI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| ADDIC (r0, r1, b2) -> "ADDIC(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| ADDIC_ (r0, r1, b2) -> "ADDIC_(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| ADDIS (r0, r1, i2) -> "ADDIS(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| ADDMEx (r0, r1, b2, b3) -> "ADDMEx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ", " ^ string_of_bool b3 ^ ")" +| ADDZEx (r0, r1, b2, b3) -> "ADDZEx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ", " ^ string_of_bool b3 ^ ")" +| ANDx (r0, r1, r2, b3) -> "ANDx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| ANDCx (r0, r1, r2, b3) -> "ANDCx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| ANDI_ (r0, r1, i2) -> "ANDI_(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| ANDIS_ (r0, r1, i2) -> "ANDIS_(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| Bx (b0, b1, b2) -> "Bx(" ^ string_of_bitstring b0 ^ ", " ^ string_of_bool b1 ^ ", " ^ string_of_bool b2 ^ ")" +| BCx (b0, i1, b2, b3, b4) -> "BCx(" ^ string_of_bitstring b0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_bitstring b2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| BCCTRx (b0, i1, b2) -> "BCCTRx(" ^ string_of_bitstring b0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_bool b2 ^ ")" +| BCLRx (b0, i1, b2) -> "BCLRx(" ^ string_of_bitstring b0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_bool b2 ^ ")" +| CMP (i0, b1, r2, r3) -> "CMP(" ^ string_of_int i0 ^ ", " ^ string_of_bool b1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_eireg r3 ^ ")" +| CMPI (i0, b1, r2, b3) -> "CMPI(" ^ string_of_int i0 ^ ", " ^ string_of_bool b1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bitstring b3 ^ ")" +| CMPL (i0, b1, r2, r3) -> "CMPL(" ^ string_of_int i0 ^ ", " ^ string_of_bool b1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_eireg r3 ^ ")" +| CMPLI (i0, b1, r2, i3) -> "CMPLI(" ^ string_of_int i0 ^ ", " ^ string_of_bool b1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_int i3 ^ ")" +| CNTLZWx (r0, r1, b2) -> "CNTLZWx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ")" +| CRAND (i0, i1, i2) -> "CRAND(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| CRANDC (i0, i1, i2) -> "CRANDC(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| CREQV (i0, i1, i2) -> "CREQV(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| CRNAND (i0, i1, i2) -> "CRNAND(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| CRNOR (i0, i1, i2) -> "CRNOR(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| CROR (i0, i1, i2) -> "CROR(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| CRORC (i0, i1, i2) -> "CRORC(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| CRXOR (i0, i1, i2) -> "CRXOR(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ")" +| DCBA (r0, r1) -> "DCBA(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| DCBF (r0, r1) -> "DCBF(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| DCBI (r0, r1) -> "DCBI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| DCBST (r0, r1) -> "DCBST(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| DCBT (r0, r1) -> "DCBT(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| DCBTST (r0, r1) -> "DCBTST(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| DCBZ (r0, r1) -> "DCBZ(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| DIVWx (r0, r1, r2, b3, b4) -> "DIVWx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| DIVWUx (r0, r1, r2, b3, b4) -> "DIVWUx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| ECIWX (r0, r1, r2) -> "ECIWX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| ECOWX (r0, r1, r2) -> "ECOWX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| EIEIO -> "EIEIO" +| EQVx (r0, r1, r2, b3) -> "EQVx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| EXTSBx (r0, r1, b2) -> "EXTSBx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ")" +| EXTSHx (r0, r1, b2) -> "EXTSHx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ")" +| FABSx (f0, f1, b2) -> "FABSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FADDx (f0, f1, f2, b3) -> "FADDx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| FADDSx (f0, f1, f2, b3) -> "FADDSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| FCMPO (i0, f1, f2) -> "FCMPO(" ^ string_of_int i0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ")" +| FCMPU (i0, f1, f2) -> "FCMPU(" ^ string_of_int i0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ")" +| FCTIWx (f0, f1, b2) -> "FCTIWx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FCTIWZx (f0, f1, b2) -> "FCTIWZx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FDIVx (f0, f1, f2, b3) -> "FDIVx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| FDIVSx (f0, f1, f2, b3) -> "FDIVSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| FMADDx (f0, f1, f2, f3, b4) -> "FMADDx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FMADDSx (f0, f1, f2, f3, b4) -> "FMADDSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FMRx (f0, f1, b2) -> "FMRx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FMSUBx (f0, f1, f2, f3, b4) -> "FMSUBx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FMSUBSx (f0, f1, f2, f3, b4) -> "FMSUBSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FMULx (f0, f1, f2, b3) -> "FMULx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| FMULSx (f0, f1, f2, b3) -> "FMULSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| FNABSx (f0, f1, b2) -> "FNABSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FNEGx (f0, f1, b2) -> "FNEGx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FNMADDx (f0, f1, f2, f3, b4) -> "FNMADDx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FNMADDSx (f0, f1, f2, f3, b4) -> "FNMADDSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FNMSUBx (f0, f1, f2, f3, b4) -> "FNMSUBx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FNMSUBSx (f0, f1, f2, f3, b4) -> "FNMSUBSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FRESx (f0, f1, b2) -> "FRESx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FRSPx (f0, f1, b2) -> "FRSPx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FRSQRTEx (f0, f1, b2) -> "FRSQRTEx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FSELx (f0, f1, f2, f3, b4) -> "FSELx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_efreg f3 ^ ", " ^ string_of_bool b4 ^ ")" +| FSQRTx (f0, f1, b2) -> "FSQRTx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FSQRTSx (f0, f1, b2) -> "FSQRTSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| FSUBx (f0, f1, f2, b3) -> "FSUBx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| FSUBSx (f0, f1, f2, b3) -> "FSUBSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_efreg f2 ^ ", " ^ string_of_bool b3 ^ ")" +| ICBI (r0, r1) -> "ICBI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| ISYNC -> "ISYNC" +| LBZ (r0, r1, b2) -> "LBZ(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LBZU (r0, r1, b2) -> "LBZU(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LBZUX (r0, r1, r2) -> "LBZUX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LBZX (r0, r1, r2) -> "LBZX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LFD (f0, r1, b2) -> "LFD(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LFDU (f0, r1, b2) -> "LFDU(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LFDUX (f0, r1, r2) -> "LFDUX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LFDX (f0, r1, r2) -> "LFDX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LFS (f0, r1, b2) -> "LFS(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LFSU (f0, r1, b2) -> "LFSU(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LFSUX (f0, r1, r2) -> "LFSUX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LFSX (f0, r1, r2) -> "LFSX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LHA (r0, r1, b2) -> "LHA(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LHAU (r0, r1, b2) -> "LHAU(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LHAUX (r0, r1, r2) -> "LHAUX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LHAX (r0, r1, r2) -> "LHAX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LHBRX (r0, r1, r2) -> "LHBRX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LHZ (r0, r1, b2) -> "LHZ(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LHZU (r0, r1, b2) -> "LHZU(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LHZUX (r0, r1, r2) -> "LHZUX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LHZX (r0, r1, r2) -> "LHZX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LMW (r0, r1, i2) -> "LMW(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| LSWI (r0, r1, r2) -> "LSWI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LSWX (r0, r1, r2) -> "LSWX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LWARX (r0, r1, r2) -> "LWARX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LWBRX (r0, r1, r2) -> "LWBRX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LWZ (r0, r1, b2) -> "LWZ(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LWZU (r0, r1, b2) -> "LWZU(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| LWZUX (r0, r1, r2) -> "LWZUX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| LWZX (r0, r1, r2) -> "LWZX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| MCRF (i0, i1) -> "MCRF(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ")" +| MCRFS (i0, i1) -> "MCRFS(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ")" +| MCRXR (i0) -> "MCRXR(" ^ string_of_int i0 ^ ")" +| MFCR (r0) -> "MFCR(" ^ string_of_eireg r0 ^ ")" +| MFFSx (f0, b1) -> "MFFSx(" ^ string_of_efreg f0 ^ ", " ^ string_of_bool b1 ^ ")" +| MFMSR (r0) -> "MFMSR(" ^ string_of_eireg r0 ^ ")" +| MFSPR (r0, b1) -> "MFSPR(" ^ string_of_eireg r0 ^ ", " ^ string_of_bitstring b1 ^ ")" +| MFSR (r0, i1) -> "MFSR(" ^ string_of_eireg r0 ^ ", " ^ string_of_int i1 ^ ")" +| MFSRIN (r0, r1) -> "MFSRIN(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| MFTB (r0, i1) -> "MFTB(" ^ string_of_eireg r0 ^ ", " ^ string_of_int i1 ^ ")" +| MTCRF (r0, i1) -> "MTCRF(" ^ string_of_eireg r0 ^ ", " ^ string_of_int i1 ^ ")" +| MTFSB0x (i0, b1) -> "MTFSB0x(" ^ string_of_int i0 ^ ", " ^ string_of_bool b1 ^ ")" +| MTFSB1x (i0, b1) -> "MTFSB1x(" ^ string_of_int i0 ^ ", " ^ string_of_bool b1 ^ ")" +| MTFSF (i0, f1, b2) -> "MTFSF(" ^ string_of_int i0 ^ ", " ^ string_of_efreg f1 ^ ", " ^ string_of_bool b2 ^ ")" +| MTFSFIx (i0, i1, b2) -> "MTFSFIx(" ^ string_of_int i0 ^ ", " ^ string_of_int i1 ^ ", " ^ string_of_bool b2 ^ ")" +| MTMSR (r0) -> "MTMSR(" ^ string_of_eireg r0 ^ ")" +| MTSPR (r0, b1) -> "MTSPR(" ^ string_of_eireg r0 ^ ", " ^ string_of_bitstring b1 ^ ")" +| MTSR (r0, i1) -> "MTSR(" ^ string_of_eireg r0 ^ ", " ^ string_of_int i1 ^ ")" +| MTSRIN (r0, r1) -> "MTSRIN(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ")" +| MULHWx (r0, r1, r2, b3) -> "MULHWx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| MULHWUx (r0, r1, r2, b3) -> "MULHWUx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| MULLI (r0, r1, b2) -> "MULLI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| MULLWx (r0, r1, r2, b3, b4) -> "MULLWx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| NANDx (r0, r1, r2, b3) -> "NANDx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| NEGx (r0, r1, b2, b3) -> "NEGx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ", " ^ string_of_bool b3 ^ ")" +| NORx (r0, r1, r2, b3) -> "NORx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| ORx (r0, r1, r2, b3) -> "ORx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| ORCx (r0, r1, r2, b3) -> "ORCx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| ORI (r0, r1, i2) -> "ORI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| ORIS (r0, r1, i2) -> "ORIS(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| RFI -> "RFI" +| RLWIMIx (r0, r1, i2, i3, i4, b5) -> "RLWIMIx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ", " ^ string_of_int i3 ^ ", " ^ string_of_int i4 ^ ", " ^ string_of_bool b5 ^ ")" +| RLWINMx (r0, r1, i2, i3, i4, b5) -> "RLWINMx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ", " ^ string_of_int i3 ^ ", " ^ string_of_int i4 ^ ", " ^ string_of_bool b5 ^ ")" +| RLWNMx (r0, r1, r2, i3, i4, b5) -> "RLWNMx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_int i3 ^ ", " ^ string_of_int i4 ^ ", " ^ string_of_bool b5 ^ ")" +| SC -> "SC" +| SLWx (r0, r1, r2, b3) -> "SLWx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| SRAWx (r0, r1, r2, b3) -> "SRAWx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| SRAWIx (r0, r1, i2, b3) -> "SRAWIx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ", " ^ string_of_bool b3 ^ ")" +| SRWx (r0, r1, r2, b3) -> "SRWx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| STB (r0, r1, b2) -> "STB(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STBU (r0, r1, b2) -> "STBU(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STBUX (r0, r1, r2) -> "STBUX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STBX (r0, r1, r2) -> "STBX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STFD (f0, r1, b2) -> "STFD(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STFDU (f0, r1, b2) -> "STFDU(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STFDUX (f0, r1, r2) -> "STFDUX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STFDX (f0, r1, r2) -> "STFDX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STFIWX (r0, r1, r2) -> "STFIWX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STFS (f0, r1, b2) -> "STFS(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STFSU (f0, r1, b2) -> "STFSU(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STFSUX (f0, r1, r2) -> "STFSUX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STFSX (f0, r1, r2) -> "STFSX(" ^ string_of_efreg f0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STH (r0, r1, b2) -> "STH(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STHBRX (r0, r1, r2) -> "STHBRX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STHU (r0, r1, b2) -> "STHU(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STHUX (r0, r1, r2) -> "STHUX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STHX (r0, r1, r2) -> "STHX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STMW (r0, r1, i2) -> "STMW(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| STSWI (r0, r1, r2) -> "STSWI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STSWX (r0, r1, r2) -> "STSWX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STW (r0, r1, b2) -> "STW(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STWBRX (r0, r1, r2) -> "STWBRX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STWCX_ (r0, r1, r2) -> "STWCX_(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STWU (r0, r1, b2) -> "STWU(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| STWUX (r0, r1, r2) -> "STWUX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| STWX (r0, r1, r2) -> "STWX(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| SUBFx (r0, r1, r2, b3, b4) -> "SUBFx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| SUBFCx (r0, r1, r2, b3, b4) -> "SUBFCx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| SUBFEx (r0, r1, r2, b3, b4) -> "SUBFEx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ", " ^ string_of_bool b4 ^ ")" +| SUBFIC (r0, r1, b2) -> "SUBFIC(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bitstring b2 ^ ")" +| SUBFMEx (r0, r1, b2, b3) -> "SUBFMEx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ", " ^ string_of_bool b3 ^ ")" +| SUBFZEx (r0, r1, b2, b3) -> "SUBFZEx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_bool b2 ^ ", " ^ string_of_bool b3 ^ ")" +| SYNC -> "SYNC" +| TLBIA -> "TLBIA" +| TLBIE (r0) -> "TLBIE(" ^ string_of_eireg r0 ^ ")" +| TLBSYNC -> "TLBSYNC" +| TW (b0, r1, r2) -> "TW(" ^ string_of_bitstring b0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ")" +| TWI (b0, r1, i2) -> "TWI(" ^ string_of_bitstring b0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| XORx (r0, r1, r2, b3) -> "XORx(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_eireg r2 ^ ", " ^ string_of_bool b3 ^ ")" +| XORI (r0, r1, i2) -> "XORI(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| XORIS (r0, r1, i2) -> "XORIS(" ^ string_of_eireg r0 ^ ", " ^ string_of_eireg r1 ^ ", " ^ string_of_int i2 ^ ")" +| UNKNOWN (b0) -> "UNKNOWN(" ^ string_of_bitstring b0 ^ ")" + +let string_of_instr_list = string_of_list string_of_instr "\n" + +let string_of_instr_array = string_of_array string_of_instr "\n" diff --git a/checklink/PPC_types.ml b/checklink/PPC_types.ml new file mode 100644 index 0000000..b3419db --- /dev/null +++ b/checklink/PPC_types.ml @@ -0,0 +1,198 @@ +open Library + +type eireg = int +type efreg = int + +type instr = +| ADDx of eireg * eireg * eireg * bool * bool +| ADDCx of eireg * eireg * eireg * bool * bool +| ADDEx of eireg * eireg * eireg * bool * bool +| ADDI of eireg * eireg * bitstring +| ADDIC of eireg * eireg * bitstring +| ADDIC_ of eireg * eireg * bitstring +| ADDIS of eireg * eireg * int +| ADDMEx of eireg * eireg * bool * bool +| ADDZEx of eireg * eireg * bool * bool +| ANDx of eireg * eireg * eireg * bool +| ANDCx of eireg * eireg * eireg * bool +| ANDI_ of eireg * eireg * int +| ANDIS_ of eireg * eireg * int +| Bx of bitstring * bool * bool +| BCx of bitstring * int * bitstring * bool * bool +| BCCTRx of bitstring * int * bool +| BCLRx of bitstring * int * bool +| CMP of int * bool * eireg * eireg +| CMPI of int * bool * eireg * bitstring +| CMPL of int * bool * eireg * eireg +| CMPLI of int * bool * eireg * int +| CNTLZWx of eireg * eireg * bool +| CRAND of int * int * int +| CRANDC of int * int * int +| CREQV of int * int * int +| CRNAND of int * int * int +| CRNOR of int * int * int +| CROR of int * int * int +| CRORC of int * int * int +| CRXOR of int * int * int +| DCBA of eireg * eireg +| DCBF of eireg * eireg +| DCBI of eireg * eireg +| DCBST of eireg * eireg +| DCBT of eireg * eireg +| DCBTST of eireg * eireg +| DCBZ of eireg * eireg +| DIVWx of eireg * eireg * eireg * bool * bool +| DIVWUx of eireg * eireg * eireg * bool * bool +| ECIWX of eireg * eireg * eireg +| ECOWX of eireg * eireg * eireg +| EIEIO +| EQVx of eireg * eireg * eireg * bool +| EXTSBx of eireg * eireg * bool +| EXTSHx of eireg * eireg * bool +| FABSx of efreg * efreg * bool +| FADDx of efreg * efreg * efreg * bool +| FADDSx of efreg * efreg * efreg * bool +| FCMPO of int * efreg * efreg +| FCMPU of int * efreg * efreg +| FCTIWx of efreg * efreg * bool +| FCTIWZx of efreg * efreg * bool +| FDIVx of efreg * efreg * efreg * bool +| FDIVSx of efreg * efreg * efreg * bool +| FMADDx of efreg * efreg * efreg * efreg * bool +| FMADDSx of efreg * efreg * efreg * efreg * bool +| FMRx of efreg * efreg * bool +| FMSUBx of efreg * efreg * efreg * efreg * bool +| FMSUBSx of efreg * efreg * efreg * efreg * bool +| FMULx of efreg * efreg * efreg * bool +| FMULSx of efreg * efreg * efreg * bool +| FNABSx of efreg * efreg * bool +| FNEGx of efreg * efreg * bool +| FNMADDx of efreg * efreg * efreg * efreg * bool +| FNMADDSx of efreg * efreg * efreg * efreg * bool +| FNMSUBx of efreg * efreg * efreg * efreg * bool +| FNMSUBSx of efreg * efreg * efreg * efreg * bool +| FRESx of efreg * efreg * bool +| FRSPx of efreg * efreg * bool +| FRSQRTEx of efreg * efreg * bool +| FSELx of efreg * efreg * efreg * efreg * bool +| FSQRTx of efreg * efreg * bool +| FSQRTSx of efreg * efreg * bool +| FSUBx of efreg * efreg * efreg * bool +| FSUBSx of efreg * efreg * efreg * bool +| ICBI of eireg * eireg +| ISYNC +| LBZ of eireg * eireg * bitstring +| LBZU of eireg * eireg * bitstring +| LBZUX of eireg * eireg * eireg +| LBZX of eireg * eireg * eireg +| LFD of efreg * eireg * bitstring +| LFDU of efreg * eireg * bitstring +| LFDUX of efreg * eireg * eireg +| LFDX of efreg * eireg * eireg +| LFS of efreg * eireg * bitstring +| LFSU of efreg * eireg * bitstring +| LFSUX of efreg * eireg * eireg +| LFSX of efreg * eireg * eireg +| LHA of eireg * eireg * bitstring +| LHAU of eireg * eireg * bitstring +| LHAUX of eireg * eireg * eireg +| LHAX of eireg * eireg * eireg +| LHBRX of eireg * eireg * eireg +| LHZ of eireg * eireg * bitstring +| LHZU of eireg * eireg * bitstring +| LHZUX of eireg * eireg * eireg +| LHZX of eireg * eireg * eireg +| LMW of eireg * eireg * int +| LSWI of eireg * eireg * eireg +| LSWX of eireg * eireg * eireg +| LWARX of eireg * eireg * eireg +| LWBRX of eireg * eireg * eireg +| LWZ of eireg * eireg * bitstring +| LWZU of eireg * eireg * bitstring +| LWZUX of eireg * eireg * eireg +| LWZX of eireg * eireg * eireg +| MCRF of int * int +| MCRFS of int * int +| MCRXR of int +| MFCR of eireg +| MFFSx of efreg * bool +| MFMSR of eireg +| MFSPR of eireg * bitstring +| MFSR of eireg * int +| MFSRIN of eireg * eireg +| MFTB of eireg * int +| MTCRF of eireg * int +| MTFSB0x of int * bool +| MTFSB1x of int * bool +| MTFSF of int * efreg * bool +| MTFSFIx of int * int * bool +| MTMSR of eireg +| MTSPR of eireg * bitstring +| MTSR of eireg * int +| MTSRIN of eireg * eireg +| MULHWx of eireg * eireg * eireg * bool +| MULHWUx of eireg * eireg * eireg * bool +| MULLI of eireg * eireg * bitstring +| MULLWx of eireg * eireg * eireg * bool * bool +| NANDx of eireg * eireg * eireg * bool +| NEGx of eireg * eireg * bool * bool +| NORx of eireg * eireg * eireg * bool +| ORx of eireg * eireg * eireg * bool +| ORCx of eireg * eireg * eireg * bool +| ORI of eireg * eireg * int +| ORIS of eireg * eireg * int +| RFI +| RLWIMIx of eireg * eireg * int * int * int * bool +| RLWINMx of eireg * eireg * int * int * int * bool +| RLWNMx of eireg * eireg * eireg * int * int * bool +| SC +| SLWx of eireg * eireg * eireg * bool +| SRAWx of eireg * eireg * eireg * bool +| SRAWIx of eireg * eireg * int * bool +| SRWx of eireg * eireg * eireg * bool +| STB of eireg * eireg * bitstring +| STBU of eireg * eireg * bitstring +| STBUX of eireg * eireg * eireg +| STBX of eireg * eireg * eireg +| STFD of efreg * eireg * bitstring +| STFDU of efreg * eireg * bitstring +| STFDUX of efreg * eireg * eireg +| STFDX of efreg * eireg * eireg +| STFIWX of eireg * eireg * eireg +| STFS of efreg * eireg * bitstring +| STFSU of efreg * eireg * bitstring +| STFSUX of efreg * eireg * eireg +| STFSX of efreg * eireg * eireg +| STH of eireg * eireg * bitstring +| STHBRX of eireg * eireg * eireg +| STHU of eireg * eireg * bitstring +| STHUX of eireg * eireg * eireg +| STHX of eireg * eireg * eireg +| STMW of eireg * eireg * int +| STSWI of eireg * eireg * eireg +| STSWX of eireg * eireg * eireg +| STW of eireg * eireg * bitstring +| STWBRX of eireg * eireg * eireg +| STWCX_ of eireg * eireg * eireg +| STWU of eireg * eireg * bitstring +| STWUX of eireg * eireg * eireg +| STWX of eireg * eireg * eireg +| SUBFx of eireg * eireg * eireg * bool * bool +| SUBFCx of eireg * eireg * eireg * bool * bool +| SUBFEx of eireg * eireg * eireg * bool * bool +| SUBFIC of eireg * eireg * bitstring +| SUBFMEx of eireg * eireg * bool * bool +| SUBFZEx of eireg * eireg * bool * bool +| SYNC +| TLBIA +| TLBIE of eireg +| TLBSYNC +| TW of bitstring * eireg * eireg +| TWI of bitstring * eireg * int +| XORx of eireg * eireg * eireg * bool +| XORI of eireg * eireg * int +| XORIS of eireg * eireg * int +| UNKNOWN of bitstring + +(* ELF parsed code *) +type ecode = instr list diff --git a/checklink/PPC_utils.ml b/checklink/PPC_utils.ml new file mode 100644 index 0000000..086d1c2 --- /dev/null +++ b/checklink/PPC_utils.ml @@ -0,0 +1,32 @@ +open ELF_types +open ELF_utils +open Library +open PPC_parsers +open PPC_types + +let code_at_vaddr (e: elf) (vaddr: int32) (nb_instr: int): ecode option = + match section_at_vaddr e vaddr with + | None -> None + | Some(sndx) -> + let code_bs = + bitstring_at_vaddr e sndx vaddr (32 * nb_instr) in + Some (parse_code_as_list code_bs) + +let code_of_sym_ndx (e: elf) (ndx: int): ecode option = + let sym = e.e_symtab.(ndx) in + match sym.st_type with + | STT_FUNC -> + let sym_vaddr = sym.st_value in + let sym_size = 8 * (int32_int sym.st_size) in + let sym_sndx = sym.st_shndx in + let code_bs = + bitstring_at_vaddr e sym_sndx sym_vaddr sym_size in + Some (parse_code_as_list code_bs) + | _ -> None + +let code_of_sym_name (e: elf) (name: string): ecode option = + match ndx_of_sym_name e name with + | Some ndx -> code_of_sym_ndx e ndx + | None -> None + + diff --git a/checklink/Validator.ml b/checklink/Validator.ml new file mode 100644 index 0000000..b27bc4c --- /dev/null +++ b/checklink/Validator.ml @@ -0,0 +1,56 @@ +open Check +open ELF_parsers +open ELF_printers +open Fuzz + +let elf_file = ref (None: string option) +let sdump_files = ref ([] : string list) +let option_fuzz = ref false +let option_dumpelf = ref false + +let set_elf_file s = + match !elf_file with + | None -> elf_file := Some s + | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line") + +let options = [ + "-dumpelf", Arg.Set option_dumpelf, + "Print the contents of the ELF executable"; + "-debug", Arg.Set Check.debug, + "Print a detailed trace of verification"; + "-elfmap", Arg.Set Check.dump_elfmap, + "Dump an ELF map to <exename>.elfmap>, for use with random fuzzing"; + "-exe <filename>", Arg.String set_elf_file, + "Specify the ELF executable file to analyze"; + "-fuzz", Arg.Set option_fuzz, + "Random fuzzing test" +] + +let anonymous arg = + if Filename.check_suffix arg ".sdump" then + sdump_files := arg :: !sdump_files + else + set_elf_file arg + +let usage = +"The CompCert C post-linking validator, version " ^ Configuration.version ^ " +Usage: valink [options] <.sdump files> <ELF executable> +Options are:" + +let _ = + Arg.parse options anonymous usage; + match !elf_file with + | None -> + Arg.usage options usage; + exit 2 + | Some elffilename -> + let sdumps = List.rev !sdump_files in + if !option_fuzz then begin + Random.self_init(); + fuzz_loop elffilename sdumps + end else if !option_dumpelf then begin + let elf = read_elf elffilename in + print_endline (string_of_elf elf) + end else begin + check_and_dump elffilename sdumps + end diff --git a/common/Sections.ml b/common/Sections.ml index 3ee36e8..90ddea7 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -14,7 +14,6 @@ (* *********************************************************************) open Camlcoq -open Cparser (* Handling of linker sections *) diff --git a/common/Sections.mli b/common/Sections.mli index a487f34..8b7c9dc 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -34,8 +34,7 @@ val define_section: -> ?writable:bool -> ?executable:bool -> ?near:bool -> unit -> unit val use_section_for: AST.ident -> string -> bool -val for_variable: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> bool -> +val for_variable: Env.t -> AST.ident -> C.typ -> bool -> section_name * bool -val for_function: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> - section_name list +val for_function: Env.t -> AST.ident -> C.typ -> section_name list val for_stringlit: unit -> section_name diff --git a/cparser/Errors.ml b/cparser/Cerrors.ml index 188531e..188531e 100644 --- a/cparser/Errors.ml +++ b/cparser/Cerrors.ml diff --git a/cparser/Errors.mli b/cparser/Cerrors.mli index 557fb14..557fb14 100644 --- a/cparser/Errors.mli +++ b/cparser/Cerrors.mli diff --git a/cparser/Cparser.mllib b/cparser/Cparser.mllib new file mode 100644 index 0000000..c5dc513 --- /dev/null +++ b/cparser/Cparser.mllib @@ -0,0 +1,21 @@ +Cerrors +Cabs +Cabshelper +Parse_aux +Parser +Lexer +Machine +Env +Cprint +Cutil +Ceval +Cleanup +Builtins +Elab +Rename +Transform +Unblock +StructReturn +Bitfields +PackedStructs +Parse diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index eb3f063..4856c01 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -16,7 +16,7 @@ (* Operations on C types and abstract syntax *) open Printf -open Errors +open Cerrors open C open Env open Machine diff --git a/cparser/Elab.ml b/cparser/Elab.ml index f9b70c4..2473cf2 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -16,7 +16,7 @@ (* Elaboration from Cabs parse tree to C simplified, typed syntax tree *) open Format -open Errors +open Cerrors open Machine open Cabs open Cabshelper @@ -29,13 +29,13 @@ open Env (* Error reporting *) let fatal_error loc fmt = - Errors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + Cerrors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc let error loc fmt = - Errors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + Cerrors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc let warning loc fmt = - Errors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc + Cerrors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc (* Error reporting for Env functions *) diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index f926ece..0dbc7cb 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -20,7 +20,7 @@ open Machine open C open Cutil open Env -open Errors +open Cerrors open Transform type field_info = { diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 0fc85bf..2a144e2 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -39,15 +39,15 @@ let parse_transformations s = !t let preprocessed_file transfs name sourcefile = - Errors.reset(); + Cerrors.reset(); let t = parse_transformations transfs in let ic = open_in sourcefile in let p = try transform_program t (Elab.elab_preprocessed_file name ic) with Parsing.Parse_error -> - Errors.error "Error during parsing"; [] - | Errors.Abort -> + Cerrors.error "Error during parsing"; [] + | Cerrors.Abort -> [] in close_in ic; - if Errors.check_errors() then None else Some p + if Cerrors.check_errors() then None else Some p diff --git a/cparser/Parse_aux.ml b/cparser/Parse_aux.ml index 6592245..0600261 100755 --- a/cparser/Parse_aux.ml +++ b/cparser/Parse_aux.ml @@ -14,7 +14,7 @@ (* *********************************************************************) open Format -open Errors +open Cerrors open Cabshelper (* Report parsing errors *) diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 76c3c12..034df24 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -83,8 +83,8 @@ let ident env id = try IdentMap.find id env.re_id with Not_found -> - Errors.fatal_error "Internal error: Rename: %s__%d unbound" - id.name id.stamp + Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" + id.name id.stamp let rec typ env = function | TPtr(ty, a) -> TPtr(typ env ty, a) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index fa304b7..abdc5d5 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -20,7 +20,7 @@ open C open Cutil -open Errors +open Cerrors (* Convert an initializer to a list of assignments. Prepend those assignments to the given statement. *) diff --git a/cfrontend/libCparser.clib b/cparser/libCparser.clib index 1b55150..1b55150 100644 --- a/cfrontend/libCparser.clib +++ b/cparser/libCparser.clib diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8feac7a..5003e3e 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -35,6 +35,7 @@ let option_dcse = ref false let option_dalloc = ref false let option_dmach = ref false let option_dasm = ref false +let option_sdump = ref false let option_E = ref false let option_S = ref false let option_c = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index c4274da..ff1046d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -84,7 +84,7 @@ let parse_c_file sourcename ifile = in (* Parsing and production of a simplified C AST *) let ast = - match Cparser.Parse.preprocessed_file simplifs sourcename ifile with + match Parse.preprocessed_file simplifs sourcename ifile with | None -> exit 2 | Some p -> p in (* Remove preprocessed file (always a temp file) *) @@ -93,7 +93,7 @@ let parse_c_file sourcename ifile = if !option_dparse then begin let ofile = Filename.chop_suffix sourcename ".c" ^ ".parsed.c" in let oc = open_out ofile in - Cparser.Cprint.program (Format.formatter_of_out_channel oc) ast; + Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc end; (* Conversion to Csyntax *) @@ -111,6 +111,18 @@ let parse_c_file sourcename ifile = end; csyntax +(* Dump Asm code in binary format for the validator *) + +let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version + +let dump_asm asm destfile = + let oc = open_out_bin destfile in + output_string oc sdump_magic_number; + output_value oc asm; + output_value oc Camlcoq.string_of_atom; + output_value oc C2C.decl_atom; + close_out oc + (* From CompCert C AST to asm *) let compile_c_ast sourcename csyntax ofile = @@ -134,7 +146,10 @@ let compile_c_ast sourcename csyntax ofile = | Errors.Error msg -> print_error stderr msg; exit 2 in - (* Save asm *) + (* Dump Asm in binary format *) + if !option_sdump then + dump_asm asm (Filename.chop_suffix sourcename ".c" ^ ".sdump"); + (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm; close_out oc @@ -286,7 +301,7 @@ let rec find_action s = function let parse_cmdline spec usage = let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in let error () = - eprintf "Usage: %s" usage; + eprintf "%s" usage; exit 2 in let rec parse i = if i < Array.length Sys.argv then begin @@ -325,7 +340,8 @@ let parse_cmdline spec usage = in parse 1 let usage_string = -"ccomp [options] <source files> +"The CompCert C verified compiler, version " ^ Configuration.version ^ " +Usage: ccomp [options] <source files> Recognized source files: .c C source file .cm Cminor source file @@ -369,6 +385,7 @@ Tracing options: -dalloc Save LTL after register allocation in <file>.alloc.ltl -dmach Save generated Mach code in <file>.mach -dasm Save generated assembly in <file>.s + -sdump Save info for post-linking validation in <file>.sdump Linking options: -l<lib> Link library <lib> -L<dir> Add <dir> to search path for libraries @@ -414,6 +431,7 @@ let cmdline_actions = "-dalloc$", Set option_dalloc; "-dmach$", Set option_dmach; "-dasm$", Set option_dasm; + "-sdump$", Set option_sdump; "-E$", Set option_E; "-S$", Set option_S; "-c$", Set option_c; @@ -461,14 +479,14 @@ let cmdline_actions = let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 }; - Cparser.Machine.config := + Machine.config := begin match Configuration.arch with - | "powerpc" -> Cparser.Machine.ppc_32_bigendian - | "arm" -> Cparser.Machine.arm_littleendian - | "ia32" -> Cparser.Machine.x86_32 + | "powerpc" -> Machine.ppc_32_bigendian + | "arm" -> Machine.arm_littleendian + | "ia32" -> Machine.x86_32 | _ -> assert false end; - Cparser.Builtins.set C2C.builtins; + Builtins.set C2C.builtins; CPragmas.initialize(); parse_cmdline cmdline_actions usage_string; if !linker_options <> [] diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index c2fd06d..596d291 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -15,7 +15,6 @@ (* Processor-dependent builtin C functions *) -open Cparser open C let builtins = { diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 41b4cfc..c1b3ca8 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -2,16 +2,23 @@ open Ocamlbuild_plugin;; dispatch begin function | After_rules -> (* declare the tags "use_Cparser" and "include_Cparser" *) - ocaml_lib "cfrontend/Cparser"; + ocaml_lib "cparser/Cparser"; (* force linking of libCparser.a when use_Cparser is set *) flag ["link"; "ocaml"; "native"; "use_Cparser"] - (S[A"cfrontend/libCparser.a"]); + (S[A"cparser/libCparser.a"]); flag ["link"; "ocaml"; "byte"; "use_Cparser"] - (S[A"-custom"; A"cfrontend/libCparser.a"]); + (S[A"-custom"; A"cparser/libCparser.a"]); (* make sure libCparser.a is up to date *) - dep ["link"; "ocaml"; "use_Cparser"] ["cfrontend/libCparser.a"]; + dep ["link"; "ocaml"; "use_Cparser"] ["cparser/libCparser.a"]; + + (* ocamlfind libraries *) + flag ["ocaml"; "link"; "pkg_unix"] & S[A"-package"; A "unix"]; + flag ["ocaml"; "link"; "pkg_str"] & S[A"-package"; A "str"]; + flag ["ocaml"; "compile"; "pkg_bitstring"] & S[A"-package"; A"bitstring,bitstring.syntax"; A"-syntax"; A"bitstring.syntax"; A"-syntax"; A"camlp4o"]; + flag ["ocaml"; "ocamldep"; "pkg_bitstring"] & S[A"-package"; A"bitstring,bitstring.syntax"; A"-syntax"; A"bitstring.syntax,camlp4o"]; + flag ["ocaml"; "link"; "pkg_bitstring"] & S[A"-package"; A"bitstring"] | _ -> () end diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 50b9be1..b9fc064 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -15,7 +15,6 @@ (* Processor-dependent builtin C functions *) -open Cparser open C let builtins = { |