From 3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 12 Oct 2015 11:48:36 +0200 Subject: Removal of cchecklink, superseded by AbsInt's Valex tool. --- .gitignore | 2 - Makefile.extr | 56 +- checklink/Asm_printers.ml | 321 ----- checklink/Bitstring_utils.ml | 33 - checklink/Check.ml | 3216 ------------------------------------------ checklink/Disassembler.ml | 15 - checklink/ELF_parsers.ml | 362 ----- checklink/ELF_printers.ml | 206 --- checklink/ELF_types.ml | 170 --- checklink/ELF_utils.ml | 128 -- checklink/Exc.ml | 2 - checklink/Frameworks.ml | 214 --- checklink/Fuzz.ml | 175 --- checklink/Lens.ml | 32 - checklink/Library.ml | 171 --- checklink/Makefile | 52 - checklink/PPC_parsers.ml | 397 ------ checklink/PPC_printers.ml | 203 --- checklink/PPC_types.ml | 198 --- checklink/PPC_utils.ml | 26 - checklink/Safe.ml | 25 - checklink/Safe32.ml | 34 - checklink/Validator.ml | 132 -- configure | 32 +- 24 files changed, 9 insertions(+), 6193 deletions(-) delete mode 100644 checklink/Asm_printers.ml delete mode 100644 checklink/Bitstring_utils.ml delete mode 100644 checklink/Check.ml delete mode 100644 checklink/Disassembler.ml delete mode 100644 checklink/ELF_parsers.ml delete mode 100644 checklink/ELF_printers.ml delete mode 100644 checklink/ELF_types.ml delete mode 100644 checklink/ELF_utils.ml delete mode 100644 checklink/Exc.ml delete mode 100644 checklink/Frameworks.ml delete mode 100644 checklink/Fuzz.ml delete mode 100644 checklink/Lens.ml delete mode 100644 checklink/Library.ml delete mode 100644 checklink/Makefile delete mode 100644 checklink/PPC_parsers.ml delete mode 100644 checklink/PPC_printers.ml delete mode 100644 checklink/PPC_types.ml delete mode 100644 checklink/PPC_utils.ml delete mode 100644 checklink/Safe.ml delete mode 100644 checklink/Safe32.ml delete mode 100644 checklink/Validator.ml diff --git a/.gitignore b/.gitignore index 107dd3a1..1c8ff7d9 100644 --- a/.gitignore +++ b/.gitignore @@ -14,8 +14,6 @@ ccomp ccomp.byte ccomp.prof -cchecklink -cchecklink.byte clightgen clightgen.byte tools/ndfun diff --git a/Makefile.extr b/Makefile.extr index 1bb3eec8..77b6880e 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -17,23 +17,13 @@ include Makefile.config -# Directories containing plain Caml code (no preprocessing) +# Directories containing plain Caml code DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ exportclight debug -# Directories containing Caml code that must be preprocessed by Camlp4 - -ifeq ($(CCHECKLINK),true) -DIRS_P4=checklink -else -DIRS_P4= -endif - -ALLDIRS=$(DIRS) $(DIRS_P4) - -INCLUDES=$(patsubst %,-I %, $(ALLDIRS)) +INCLUDES=$(patsubst %,-I %, $(DIRS)) # Control of warnings: # warning 3 = deprecated feature. Turned off for OCaml 4.02 (bytes vs strings) @@ -45,10 +35,6 @@ extraction/%.cmo: WARNINGS +=-w -20 COMPFLAGS=-g $(INCLUDES) $(WARNINGS) -# Using the bitstring library and syntax extension (for checklink) - -BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o - # Using .opt compilers if available ifeq ($(OCAML_OPT_COMP),true) @@ -57,19 +43,10 @@ else DOTOPT= endif -# Compilers used for non-preprocessed code - OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS) OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS) OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES) -# Compilers used for Camlp4-preprocessed code. Note that we cannot -# use the .opt compilers (because ocamlfind doesn't support them). - -OCAMLC_P4=ocamlfind ocamlc $(COMPFLAGS) $(BITSTRING) -OCAMLOPT_P4=ocamlfind ocamlopt $(COMPFLAGS) $(BITSTRING) -OCAMLDEP_P4=ocamlfind ocamldep $(INCLUDES) $(BITSTRING) - MENHIR=menhir --explain OCAMLLEX=ocamllex -q MODORDER=tools/modorder .depend.extr @@ -98,20 +75,6 @@ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ -ifeq ($(CCHECKLINK),true) - -CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx) - -cchecklink: $(CCHECKLINK_OBJS) - @echo "Linking $@" - @$(OCAMLOPT_P4) -linkpkg -o $@ $(CHECKLINK_LIBS) $+ - -cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo) - @echo "Linking $@" - @$(OCAMLC_P4) -linkpkg -o $@ $(CHECKLINK_LIBS:.cmxa=.cma) $+ - -endif - CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx) clightgen: $(CLIGHTGEN_OBJS) @@ -128,16 +91,6 @@ endif # End of part that assumes .depend.extr already exists -checklink/%.cmi: checklink/%.mli - @echo "OCAMLC $<" - @$(OCAMLC_P4) -c $< -checklink/%.cmo: checklink/%.ml - @echo "OCAMLC $<" - @$(OCAMLC_P4) -c $< -checklink/%.cmx: checklink/%.ml - @echo "OCAMLOPT $<" - @$(OCAMLOPT_P4) -c $< - %.cmi: %.mli @echo "OCAMLC $<" @$(OCAMLC) -c $< @@ -156,15 +109,12 @@ checklink/%.cmx: checklink/%.ml clean: rm -f $(EXECUTABLES) rm -f $(GENERATED) - for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done + for d in $(DIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done # Generation of .depend.extr depend: $(GENERATED) @echo "Analyzing OCaml dependencies" @$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli $(d)/*.ml)) $(GENERATED) >.depend.extr || { rm -f .depend.extr; exit 2; } -ifneq ($(strip $(DIRS_P4)),) - @$(OCAMLDEP_P4) $(foreach d,$(DIRS_P4),$(wildcard $(d)/*.mli $(d)/*.ml)) >>.depend.extr || { rm -f .depend.extr; exit 2; } -endif diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml deleted file mode 100644 index 38a420f6..00000000 --- a/checklink/Asm_printers.ml +++ /dev/null @@ -1,321 +0,0 @@ -open Camlcoq -open Asm -open AST -open Library - -let string_of_pos p = Z.to_string (Z.Zpos p) -let string_of_coq_Z = Z.to_string -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" -| CR1_2 -> "CR1_2" - -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 ^ ")" -| Csymbol_rel_low (i0, i1) -> "Csymbol_rel_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" -| Csymbol_rel_high (i0, i1) -> "Csymbol_rel_high(" ^ 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" -| CRbit_6 -> "CRbit_6" - -let string_of_memory_chunk = function - | Mint8signed -> "int8s" - | Mint8unsigned -> "int8u" - | Mint16signed -> "int16s" - | Mint16unsigned -> "int16u" - | Mint32 -> "int32" - | Mint64 -> "int64" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - | Many32 -> "any32" - | Many64 -> "any64" - -let rec string_of_annot_param sp_reg_name = function - | AA_base x -> string_of_preg x - | AA_int n -> Printf.sprintf "%ld" (camlint_of_coqint n) - | AA_long n -> Printf.sprintf "%Ld" (camlint64_of_coqint n) - | AA_float n -> Printf.sprintf "%.18g" (camlfloat_of_coqfloat n) - | AA_single n -> Printf.sprintf "%.18g" (camlfloat_of_coqfloat32 n) - | AA_loadstack(chunk, ofs) -> - Printf.sprintf "mem(%s + %ld, %s)" - sp_reg_name - (camlint_of_coqint ofs) - ((string_of_memory_chunk chunk)) - | AA_addrstack ofs -> - Printf.sprintf "(%s + %ld)" - sp_reg_name - (camlint_of_coqint ofs) - | AA_loadglobal(chunk, id, ofs) -> - Printf.sprintf "mem(\"%s\" + %ld, %s)" - (extern_atom id) - (camlint_of_coqint ofs) - (string_of_memory_chunk chunk) - | AA_addrglobal(id, ofs) -> - Printf.sprintf "(\"%s\" + %ld)" - (extern_atom id) - (camlint_of_coqint ofs) - | AA_longofwords(hi, lo) -> - Printf.sprintf "(%s * 0x100000000 + %s)" - (string_of_annot_param sp_reg_name hi) - (string_of_annot_param sp_reg_name lo) - -let string_of_instruction = function -| Padd (i0, i1, i2) -> "Padd(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Paddc (i0, i1, i2) -> "Paddc(" ^ 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 sg -> "Pbctr" -| Pbctrl sg -> "Pbctrl" -| Pbdnz (l1) -> "Pbdnz(" ^ string_of_label l1 ^ ")" -| Pbf (c0, l1) -> "Pbf(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" -| Pbl (i0, sg) -> "Pbl(" ^ string_of_ident i0 ^ ")" -| Pbs (i0, sg) -> "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 ^ ")" -| Pcntlzw (i0, i1) -> "Pcntlzw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pcreqv (c0, c1, c2) -> "Pcreqv(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" -| Pcror (c0, c1, c2) -> "Pcror(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" -| Pcrxor (c0, c1, c2) -> "Pcrxor(" ^ 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 ^ ")" -| Peieio -> "Peieio" -| 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 ^ ")" -| Pfabss (f0, f1) -> "Pfabss(" ^ 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 ^ ")" -| Pfadds (f0, f1, f2) -> "Pfadds(" ^ 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 ^ ")" -| Pfctiw (f0, f1) -> "Pfctiw(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfctiwz (f0, f1) -> "Pfctiwz(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfdiv (f0, f1, f2) -> "Pfdiv(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfdivs (f0, f1, f2) -> "Pfdivs(" ^ 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 ^ ")" -| Pfmuls (f0, f1, f2) -> "Pfmuls(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfneg (f0, f1) -> "Pfneg(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfnegs (f0, f1) -> "Pfnegs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfrsp (f0, f1) -> "Pfrsp(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfxdp (f0, f1) -> "Pfxdp(" ^ 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 ^ ")" -| Pfsubs (f0, f1, f2) -> "Pfsubs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfmadd (f0, f1, f2, f3) -> "Pfmadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfmsub (f0, f1, f2, f3) -> "Pfmsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfnmadd (f0, f1, f2, f3) -> "Pfnmadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfnmsub (f0, f1, f2, f3) -> "Pfnmsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfsqrt (f0, f1) -> "Pfsqrt(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfrsqrte (f0, f1) -> "Pfrsqrte(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfres (f0, f1) -> "Pfres(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfsel (f0, f1, f2, f3) -> "Pfsel(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pisync -> "Pisync" -| 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 ^ ")" -| Plfd_a (f0, c1, i2) -> "Plfd_a(" ^ 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 ^ ")" -| Plfdx_a (f0, i1, i2) -> "Plfdx_a(" ^ 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 ^ ")" -| Plhbrx (i0, i1, i2) -> "Plhbrx(" ^ 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_ffloat f1 ^ ")" -| Plfis (f0, f1) -> "Plfis(" ^ string_of_freg f0 ^ ", " ^ string_of_ffloat32 f1 ^ ")" -| Plwarx (i0, i1, i2) -> "Plwarx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwbrx (i0, i1, i2) -> "Plwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwz (i0, c1, i2) -> "Plwz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwzu (i0, c1, i2) -> "Plwzu(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwz_a (i0, c1, i2) -> "Plwz_a(" ^ 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 ^ ")" -| Plwzx_a (i0, i1, i2) -> "Plwzx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pmfcr (i0) -> "Pmfcr(" ^ string_of_ireg i0 ^ ")" -| 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 ^ ")" -| Pmulhw (i0, i1, i2) -> "Pmulhw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pmulhwu (i0, i1, i2) -> "Pmulhwu(" ^ 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 ^ ")" -| Pstfd_a (f0, c1, i2) -> "Pstfd_a(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfdu (f0, c1, i2) -> "Pstfdu(" ^ 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 ^ ")" -| Pstfdx_a (f0, i1, i2) -> "Pstfdx_a(" ^ 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 ^ ")" -| Psthbrx (i0, i1, i2) -> "Psthbrx(" ^ 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 ^ ")" -| Pstw_a (i0, c1, i2) -> "Pstw_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwu (i0, c1, i2) -> "Pstwu(" ^ 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 ^ ")" -| Pstwx_a (i0, i1, i2) -> "Pstwx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwux (i0, i1, i2) -> "Pstwux(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwbrx (i0, i1, i2) -> "Pstwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwcx_ (i0, i1, i2) -> "Pstwcx_(" ^ 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 ^ ")" -| Psubfze (i0, i1) -> "Psubfze(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Psubfic (i0, i1, c2) -> "Psubfic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Psync -> "Psync" -| Ptrap -> "Ptrap" -| 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_list string_of_preg ", " p2 ^ ")" -| Pannot (e0, a1) -> - let sp_reg_name = string_of_external_function e0 in - "Pannot(" ^ string_of_external_function e0 ^ ", " ^ string_of_list (string_of_annot_param sp_reg_name) ", " a1 ^ ")" -| Pcfi_adjust n -> "Pcfi_adjust(" ^ string_of_coq_Z n ^ ")" -| Pcfi_rel_offset n -> "Pcfi_rel_offset(" ^ string_of_coq_Z n ^ ")" - -let string_of_init_data = function -| Init_int8(i) -> "Init_int8(" ^ string_of_int (z_int_lax i) ^ ")" -| Init_int16(i) -> "Init_int16(" ^ string_of_int (z_int_lax i) ^ ")" -| Init_int32(i) -> "Init_int32(" ^ string_of_int32i (z_int32 i) ^ ")" -| Init_int64(i) -> "Init_int64(" ^ string_of_int64i (z_int64 i) ^ ")" -| Init_float32(f) -> "Init_float32(" ^ string_of_ffloat32 f ^ ")" -| Init_float64(f) -> "Init_float64(" ^ string_of_ffloat f ^ ")" -| Init_space(z) -> "Init_space(" ^ string_of_int (z_int z) ^ ")" -| Init_addrof(ident, ofs) -> - "Init_addrof(" ^ string_of_pos ident ^ ", " ^ string_of_int32i (z_int32 ofs) ^ ")" diff --git a/checklink/Bitstring_utils.ml b/checklink/Bitstring_utils.ml deleted file mode 100644 index 3218f898..00000000 --- a/checklink/Bitstring_utils.ml +++ /dev/null @@ -1,33 +0,0 @@ -(** 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 is_zeros (bs: bitstring) (size: int): bool = - Bitstring.bitstring_length bs >= size - && Bitstring.is_zeroes_bitstring (Bitstring.subbitstring bs 0 size) - -(* - -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 deleted file mode 100644 index 0e69ab72..00000000 --- a/checklink/Check.ml +++ /dev/null @@ -1,3216 +0,0 @@ -open Asm -open Asm_printers -open AST -open Bitstring_utils -open C2C -open Camlcoq -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 even when backtracking. -*) -let debug = ref false - -(** Whether to print the ELF map. *) -let print_elfmap = ref false - -(** Whether to dump the ELF map. *) -let dump_elfmap = ref false - -(** Whether to check that all ELF function/data symbols have been matched - against CompCert idents. *) -let exhaustivity = ref true - -(** Whether to print the list of all symbols (function and data) that were not - found in .sdump files. *) -let list_missing = ref false - -(** CompCert Asm *) -type ccode = Asm.coq_function - -let print_debug s = - if !debug then print_endline (string_of_log_entry true (DEBUG(s))) - -(** Adds a log entry into the framework. *) -let add_log (entry: log_entry) (efw: e_framework): e_framework = - if !debug then print_endline ("--DEBUG-- " ^ string_of_log_entry true 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)" - )) - ) - -(** Adapted from CompCert *) -let name_of_section_Linux: section_name -> string = function -| Section_text -> ".text" -| Section_data i -> if i then ".data" else "COMM" -| Section_small_data i -> if i then ".sdata" else ".sbss" -| Section_const i -> if i then ".rodata" else "COMM" -| Section_small_const i -> if i then ".sdata2" else "COMM" -| Section_string -> ".rodata" -| Section_literal -> ".rodata.cst8" -| Section_jumptable -> ".text" -| Section_user(s, wr, ex) -> s -| Section_debug_info -> ".debug_info" -| Section_debug_abbrev -> ".debug_abbrev" - -(** Adapted from CompCert *) -let name_of_section_Diab: section_name -> string = function -| Section_text -> ".text" -| Section_data i -> if i then ".data" else "COMM" -| 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 -| Section_debug_info -> ".debug_info" -| Section_debug_abbrev -> ".debug_abbrev" - -(** Taken from CompCert *) -let name_of_section: section_name -> string = - begin match Configuration.system with - | "linux" -> name_of_section_Linux - | "diab" -> name_of_section_Diab - | _ -> fatal "Unsupported CompCert configuration" - 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 - try - let (value, conflicts) = StringMap.find c_name sfw.ef.section_map in - let expected = from_inferrable value in - if e_name = expected - then sfw - else ( - sfw - >>> (sf_ef |-- section_map) ^%= - StringMap.add c_name (value, StringSet.add e_name conflicts) - ) - with Not_found -> ( - sfw - >>> (sf_ef |-- section_map) ^%= - StringMap.add c_name (Inferred(e_name), StringSet.empty) - ) - -(** 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 - (Safe32.of_int (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 (Safe32.of_int 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.sf.ef.chkd_fun_syms.(ndx) <- true; - ffw - >>> (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) - -(** 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. Otherwise, it filters out all symbols whose virtual - address does not match [vaddr]. -*) -let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework) - : s_framework or_err = - try ( - (* get the list of possible symbols for ident [k] *) - let id_ndxes = PosMap.find k sfw.ident_to_sym_ndx in - (* consider only the ones at the correct virtual address *) - match List.filter - (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_value = vaddr) - id_ndxes - with - | [] -> - (* no symbol has that virtual address *) - ERR( - Printf.sprintf - "Incoherent constraints for ident %s with value %s and candidates [%s]" - (Hashtbl.find sfw.ident_to_name k) - (string_of_int32 vaddr) - (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( - Printf.sprintf - "Missing ident: %s should be at vaddr: %s" - (Hashtbl.find sfw.ident_to_name k) - (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 or_err = - 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 num_crbit = function - | CRbit_0 -> 0 - | CRbit_1 -> 1 - | CRbit_2 -> 2 - | CRbit_3 -> 3 - | CRbit_6 -> 6 - -type checker = f_framework -> f_framework or_err -let check (cond: bool) (msg: string): checker = - fun ffw -> if cond then OK(ffw) else ERR(msg) -let check_eq (msg: string) (a: 'a) (b: 'a): checker = - check (a = b) msg -let match_bools a b = - check_eq ( - Printf.sprintf "match_bools %s %s" (string_of_bool a) (string_of_bool b) - ) a b -let match_ints a b = - check_eq ( - Printf.sprintf "match_ints %s %s" (string_of_int a) (string_of_int b) - ) a b -let match_int32s a b: checker = - check_eq ( - Printf.sprintf "match_int32s %s %s" (string_of_int32 a) (string_of_int32 b) - ) a b -(** We compare floats by their bit representation, so that 0.0 and -0.0 are - different. *) -let match_floats (a: Floats.float) (b: int64): checker = - let a = camlint64_of_coqint (Floats.Float.to_bits a) in - check_eq ( - Printf.sprintf "match_floats %s %s" (string_of_int64 a) (string_of_int64 b) - ) a b -let match_floats32 (a: Floats.float32) (b: int32): checker = - let a = camlint_of_coqint (Floats.Float32.to_bits a) in - check_eq ( - Printf.sprintf "match_floats %s %s" (string_of_int32 a) (string_of_int32 b) - ) a b -let match_crbits cb eb = - let cb = num_crbit cb in - check_eq ( - Printf.sprintf "match_crbits %d %d" cb eb - ) cb eb -let match_iregs cr er = - let er = ireg_arr.(er) in - check_eq ( - Printf.sprintf "match_iregs %s %s" (string_of_ireg cr) (string_of_ireg er) - ) cr er -let match_fregs cr er = - let er = freg_arr.(er) in - check_eq ( - Printf.sprintf "match_fregs %s %s" (string_of_freg cr) (string_of_freg er) - ) cr 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): checker = fun ffw -> - let sfw = ffw |. ff_sf in - let efw = ffw |. ff_ef in - match cc with - | Cint (i) -> - let i = z_int32_lax i in - let msg = - Printf.sprintf "match_csts Cint %s %s" - (string_of_int32 i) - (string_of_int32 ec) - in - check_eq msg ec 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 - ERR("Csymbol_low " ^ string_of_list id ", " sym_names) - | _ -> - if candidates = vaddrs - then OK(ffw) - else OK( - 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 - ERR("Csymbol_high " ^ string_of_list id ", " sym_names) - | _ -> - if candidates = vaddrs - then OK(ffw) - else OK( - ffw - >>> ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) - ) - end - | Csymbol_sda (ident, i) -> - (* sda should be handled separately in places it occurs *) - ERR("Incorrect reference to near-data symbol " - ^ Hashtbl.find ffw.sf.ident_to_name ident) - | Csymbol_rel_low (ident, i) | Csymbol_rel_high (ident, i) -> - (* should be handled separately in places it occurs *) - ERR("Incorrect reference to far-data symbol " - ^ Hashtbl.find ffw.sf.ident_to_name ident) - -let match_z_int32 (cz: Z.t) (ei: int32) = - let cz = z_int32 cz in - check_eq ( - Printf.sprintf "match_z_int32 %s %s" (string_of_int32 cz) (string_of_int32 ei) - ) cz ei - -let match_z_int (cz: Z.t) (ei: int) = - let cz = z_int32 cz in - let ei = Safe32.of_int ei in - check_eq ( - Printf.sprintf "match_z_int %s %s" (string_of_int32i cz) (string_of_int32i ei) - ) cz ei - -(* [m] is interpreted as a bitmask, and checked against [ei]. *) -let match_mask (m: Z.t) (ei: int32) = - let m = z_int32_lax m in - check_eq ( - Printf.sprintf "match_mask %s %s" - (string_of_int32 m) - (string_of_int32 ei) - ) m ei - -(** Checks that the special register referred to in [spr] is [r]. *) -let match_spr (str: string) (r: int) (spr: bitstring): checker = fun ffw -> - bitmatch spr with - | { v:5; 0:5 } when v = r -> OK(ffw) - | { _ } -> ERR(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) (* this needs special handling *) - 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 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 - | { _ } -> - ERR("Ill-formed jump table") - ) - in - let elf = ffw.sf.ef.elf in - begin match bitstring_at_vaddr elf vaddr size with - | None -> ERR("No section for the jumptable") - | Some(bs, pofs, psize) -> - ffw - >>> match_jmptbl_aux lbllist bs - >>^ (ff_ef ^%= - add_range pofs psize 0 Jumptable - ) - end - -let match_bo_bt_bool bo = - bitmatch bo with - | { false:1; true:1; true:1; false:1; false:1 } -> true - | { _ } -> false - -let match_bo_bf_bool bo = - bitmatch bo with - | { false:1; false:1; true:1; false:1; false:1 } -> true - | { _ } -> false - -let match_bo_bdnz_bool bo = - bitmatch bo with - | { true:1; false:1; false:1; false:1; false:1 } -> true - | { _ } -> false - -let match_bo_bt bo: checker = fun ffw -> - bitmatch bo with - | { false:1; true:1; true:1; false:1; false:1 } -> OK(ffw) - | { _ } -> ERR("match_bo_bt") - -let match_bo_bf bo: checker = fun ffw -> - if match_bo_bf_bool bo - then OK(ffw) - else ERR("match_bo_bf") - -let match_bo_ctr bo: checker = fun ffw -> - bitmatch bo with - | { true:1; false:1; true:1; false:1; false:1 } -> OK(ffw) - | { _ } -> ERR("match_bo_ctr") - -(** Checks whether it is feasible that the position at offset [ofs] from the - CompCert symbol [ident] is situated at a relative address [addr] from - the SDA register [r]. This means that the following equation must hold: - [r] + addr = @ident + ofs - This allows us to determine what address [r] has to contain. If it is the - first such guess or if it matches previous expectations, it's fine. - Otherwise, there is a conflict that is reported in sda_map. -*) -let check_sda ident ofs r addr ffw: f_framework or_err = - let ofs = z_int32 ofs in - let check_sda_aux ndx: (int * f_framework) or_err = - let elf = ffw.sf.ef.elf in - let sym = elf.e_symtab.(ndx) in - let expected_addr = Safe32.(sym.st_value + ofs - addr) in - try - let r_addr = from_inferrable (IntMap.find r ffw.sf.ef.sda_map) in - if r_addr = expected_addr - then OK(ndx, ffw) - else ERR( - Printf.sprintf - "SDA register %d is expected to point both at 0x%lx and 0x%lx" - r r_addr expected_addr - ) - with Not_found -> - OK(ndx, - ffw >>> (ff_ef |-- sda_map) ^%= IntMap.add r (Inferred(expected_addr)) - ) - in - (* We might not know yet what symbols is the one for that ident *) - let sym_list = PosMap.find ident ffw.sf.ident_to_sym_ndx in - (* So we test all the candidates *) - let res = List.map check_sda_aux sym_list in - (* For now, we hope at most one matches *) - match filter_ok res with - | [] -> ERR("No satisfying SDA mapping, errors were: " ^ - string_of_list id ", " (filter_err res)) - | [(ndx, ffw)] -> OK( - ffw - (* We instantiate the relationship for that ident to the matching symbol *) - >>> (ff_sf |-- ident_to_sym_ndx) ^%= PosMap.add ident [ndx] - ) - | _ -> fatal "Multiple possible SDA mappings, please report." - -(** Compares a whole CompCert function code against an ELF code, starting at - program counter [pc]. -*) -let rec compare_code ccode ecode pc: checker = fun fw -> - match ccode, ecode with - | [], [] -> OK(fw) - | [], e_rest -> - let rest_str = String.concat "\n" (List.map string_of_instr e_rest) in - ERR("CompCert code exhausted before the end of ELF code, remaining:\n" - ^ rest_str) - | c_rest, [] -> - let rest_str = String.concat "\n" (List.map string_of_instruction c_rest) in - ERR("ELF code exhausted before the end of CompCert code, remaining:\n" - ^ rest_str) - | c::cs, e::es -> - let recur_simpl = compare_code cs es (Int32.add 4l pc) in - let current_instr = - "[" ^ string_of_int32 pc ^ "] " ^ string_of_instruction c ^ " - " ^ string_of_instr e in - let error = ERR("Non-matching instructions: " ^ current_instr) in - let fw = - if !debug - then (ff_ef ^%= add_log (DEBUG(current_instr))) fw - else fw - in - match c with - | Padd(rd, r1, r2) -> - begin match ecode with - | ADDx(rD, rA, rB, oe, rc) :: es -> - OK(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 - | Paddc(rd, r1, r2) -> - begin match ecode with - | ADDCx(rD, rA, rB, oe, rc) :: es -> - OK(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 -> - OK(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, Csymbol_sda(ident, ofs)) -> - begin match ecode with - | ADDI(rD, rA, simm) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= check_sda ident ofs rA (exts simm) - >>= recur_simpl - | _ -> error - end - | Paddi(rd, r1, cst) -> - begin match ecode with - | ADDI(rD, rA, simm) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (exts simm) - >>= recur_simpl - | _ -> error - end - | Paddis(rd, r1, Csymbol_rel_high(id, ofs)) -> - begin match cs with - | Paddi(rd', r1', Csymbol_rel_low(id', ofs')) :: cs - when id' = id && ofs' = ofs -> - begin match ecode with - | ADDIS(rD, rA, simm) :: ADDI(rD', rA', simm') :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1' rA' - >>= match_iregs rd' rD' - >>= check_sda id ofs rA - Int32.(add (shift_left (of_int simm) 16) (exts simm')) - >>= compare_code cs es (Int32.add 8l pc) - | _ -> error - end - | _ -> error - end - | Paddis(rd, r1, cst) -> - begin match ecode with - | ADDIS(rD, rA, simm) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (Safe32.of_int simm) - >>= recur_simpl - | _ -> error - end - | Paddze(rd, r1) -> - begin match ecode with - | ADDZEx(rD, rA, oe, rc) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_bools false oe - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pallocframe(sz, ofs) -> error - | Pandc(rd, r1, r2) -> - begin match ecode with - | ANDCx(rS, rA, rB, rc) :: es -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> error - end - | Pandi_(rd, r1, cst) -> - begin match ecode with - | ANDI_(rS, rA, uimm) :: es -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> error - end - | Pannot(ef, args) -> - OK(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 - OK(fw) - >>= lblmap_unify lbl lblvaddr - >>= match_bools false aa - >>= match_bools false lk - >>= recur_simpl - | _ -> error - end - | Pbctr sg -> - begin match ecode with - | BCCTRx(bo, bi, lk) :: es -> - OK(fw) - >>= match_bo_ctr bo - >>= match_ints 0 bi - >>= match_bools false lk - >>= recur_simpl - | _ -> error - end - | Pbctrl sg -> - begin match ecode with - | BCCTRx(bo, bi, lk) :: es -> - OK(fw) - >>= match_bo_ctr bo - >>= match_ints 0 bi - >>= match_bools true lk - >>= recur_simpl - | _ -> error - end - | Pbdnz(lbl) -> - begin match ecode with - | BCx (bo, bi, bd, aa, lk) :: es when match_bo_bdnz_bool bo -> - let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in - OK(fw) - >>= match_ints 0 bi - >>= lblmap_unify lbl lblvaddr - >>= match_bools false aa - >>= match_bools false lk - >>= recur_simpl - | _ -> error - end - | Pbf(bit, lbl) -> - begin match ecode with - | BCx(bo, bi, bd, aa, lk) :: es when match_bo_bf_bool bo -> - let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in - OK(fw) - (*>>= match_bo_bf bo already done in pattern match *) - >>= match_crbits bit bi - >>= lblmap_unify lbl lblvaddr - >>= match_bools false aa - >>= match_bools false lk - >>= recur_simpl - | BCx(bo0, bi0, bd0, aa0, lk0) :: - Bx (li1, aa1, lk1) :: es -> - let cnext = Int32.add pc 8l in - let enext = Int32.(add pc (mul 4l (exts bd0))) in - let lblvaddr = Int32.(add pc (mul 4l (exts bd0))) in - OK(fw) - >>= match_bo_bt bo0 - >>= match_crbits bit bi0 - >>= match_int32s cnext enext - >>= match_bools false aa0 - >>= match_bools false lk0 - >>= lblmap_unify lbl lblvaddr - >>= match_bools false aa1 - >>= match_bools false lk1 - >>= compare_code cs es (Int32.add 8l pc) - | _ -> error - end - | Pbl(ident, sg) -> - begin match ecode with - | Bx(li, aa, lk) :: es -> - let dest = Int32.(add pc (mul 4l (exts li))) in - OK(fw) - >>= (ff_sf ^%=? idmap_unify ident dest) - >>= match_bools false aa - >>= match_bools true lk - >>= recur_simpl - | _ -> error - end - | Pblr -> - begin match ecode with - | BCLRx(bo, bi, lk) :: es -> - OK(fw) - >>= match_bo_ctr bo - >>= match_ints 0 bi - >>= match_bools false lk - >>= recur_simpl - | _ -> error - end - | Pbs(ident, sg) -> - begin match ecode with - | Bx(li, aa, lk) :: es -> - let dest = Int32.(add pc (mul 4l (exts li))) in - OK(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 when match_bo_bt_bool bo -> - let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in - OK(fw) - (*>>= match_bo_bt bo already done in pattern match *) - >>= match_crbits bit bi - >>= lblmap_unify lbl lblvaddr - >>= match_bools false aa - >>= match_bools false lk - >>= recur_simpl - | BCx(bo0, bi0, bd0, aa0, lk0) :: - Bx (li1, aa1, lk1) :: es -> - let cnext = Int32.add pc 8l in - let enext = Int32.(add pc (mul 4l (exts bd0))) in - let lblvaddr = Int32.(add pc (mul 4l (exts bd0))) in - OK(fw) - >>= match_bo_bf bo0 - >>= match_crbits bit bi0 - >>= match_int32s cnext enext - >>= match_bools false aa0 - >>= match_bools false lk0 - >>= lblmap_unify lbl lblvaddr - >>= match_bools false aa1 - >>= match_bools false lk1 - >>= compare_code cs es (Int32.add 8l pc) - | _ -> error - end - | Pbtbl(reg, table) -> - begin match ecode with - | RLWINMx(rS0, rA0, sh, mb, me, rc0) :: - ADDIS (rD1, rA1, simm1) :: - LWZ (rD2, rA2, d2) :: - MTSPR (rS3, spr3) :: - BCCTRx(bo4, bi4, rc4) :: es -> - let tblvaddr = Int32.( - add (shift_left (Safe32.of_int simm1) 16) (exts d2) - ) in - let tblsize = Safe32.of_int (4 * List.length table) in - OK(fw) - >>= match_iregs GPR12 rA0 - >>= match_iregs reg rS0 - >>= match_ints sh 2 - >>= match_ints mb 0 - >>= match_ints me 29 - >>= match_bools false rc0 - >>= match_iregs GPR12 rA1 - >>= match_iregs GPR12 rD1 - >>= match_iregs GPR12 rA2 - >>= match_iregs GPR12 rD2 - >>= match_iregs GPR12 rS3 - >>= match_ctr spr3 - >>= match_bo_ctr bo4 - >>= match_ints 0 bi4 - >>= match_bools false rc4 - >>= match_jmptbl table tblvaddr tblsize - >>= compare_code cs es (Int32.add 20l pc) - | _ -> error - end - | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_inline_asm(_) -> fatal "Unsupported: inline asm statement." - | _ -> fatal "Unexpected Pbuiltin, please report." - end - | Pcfi_adjust _ | Pcfi_rel_offset _ -> - OK(fw) - >>= compare_code cs ecode pc - | Pcmplw(r1, r2) -> - begin match ecode with - | CMPL(crfD, l, rA, rB) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs r1 rA - >>= match_csts cst (Safe32.of_int 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 -> - OK(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 -> - OK(fw) - >>= match_ints crfD 0 - >>= match_bools false l - >>= match_iregs r1 rA - >>= match_csts cst (exts simm) - >>= recur_simpl - | _ -> error - end - | Pcntlzw(r1, r2) -> - begin match ecode with - | CNTLZWx(rS, rA, rc) :: es -> - OK(fw) - >>= match_iregs r2 rS - >>= match_iregs r1 rA - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pcreqv(bd, b1, b2) -> - begin match ecode with - | CREQV(crbD, crbA, crbB) :: es -> - OK(fw) - >>= match_crbits bd crbD - >>= match_crbits b1 crbA - >>= match_crbits b2 crbB - >>= recur_simpl - | _ -> error - end - | Pcror(bd, b1, b2) -> - begin match ecode with - | CROR(crbD, crbA, crbB) :: es -> - OK(fw) - >>= match_crbits bd crbD - >>= match_crbits b1 crbA - >>= match_crbits b2 crbB - >>= recur_simpl - | _ -> error - end - | Pcrxor(bd, b1, b2) -> - begin match ecode with - | CRXOR(crbD, crbA, crbB) :: es -> - OK(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 -> - OK(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 -> - OK(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 - | Peieio -> - begin match ecode with - | EIEIO :: es -> - OK(fw) - >>= recur_simpl - | _ -> error - end - | Peqv(rd, r1, r2) -> - begin match ecode with - | EQVx(rS, rA, rB, rc) :: es -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfabs(rd, r1) | Pfabss(rd, r1) -> - begin match ecode with - | FABSx(frD, frB, rc) :: es -> - OK(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 -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfadds(rd, r1, r2) -> - begin match ecode with - | FADDSx(frD, frA, frB, rc) :: es -> - OK(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 -> - OK(fw) - >>= match_crbits CRbit_0 crfD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= recur_simpl - | _ -> error - end - | Pfcti(rd, r1) -> - error - | Pfctiw(rd, r1) -> - begin match ecode with - | FCTIWx(frD0, frB0, rc0) :: es -> - OK(fw) - >>= match_fregs rd frD0 - >>= match_fregs r1 frB0 - >>= match_bools false rc0 - >>= recur_simpl - | _ -> error - end - | Pfctiwz(rd, r1) -> - begin match ecode with - | FCTIWZx(frD0, frB0, rc0) :: es -> - OK(fw) - >>= match_fregs rd frD0 - >>= match_fregs r1 frB0 - >>= match_bools false rc0 - >>= recur_simpl - | _ -> error - end - | Pfdiv(rd, r1, r2) -> - begin match ecode with - | FDIVx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfdivs(rd, r1, r2) -> - begin match ecode with - | FDIVSx(frD, frA, frB, rc) :: es -> - OK(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) -> - error - | Pfmr(rd, r1) -> - begin match ecode with - | FMRx(frD, frB, rc) :: es -> - OK(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 -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfmuls(rd, r1, r2) -> - begin match ecode with - | FMULSx(frD, frA, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfneg(rd, r1) | Pfnegs(rd, r1) -> - begin match ecode with - | FNEGx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfreeframe(sz, ofs) -> - error - | Pfrsp(rd, r1) -> - begin match ecode with - | FRSPx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfxdp(rd, r1) -> - error - | Pfsub(rd, r1, r2) -> - begin match ecode with - | FSUBx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfsubs(rd, r1, r2) -> - begin match ecode with - | FSUBSx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfmadd(rd, r1, r2, r3) -> - begin match ecode with - | FMADDx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r3 frB - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfmsub(rd, r1, r2, r3) -> - begin match ecode with - | FMSUBx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r3 frB - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfnmadd(rd, r1, r2, r3) -> - begin match ecode with - | FNMADDx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r3 frB - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfnmsub(rd, r1, r2, r3) -> - begin match ecode with - | FNMSUBx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r3 frB - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfsqrt(rd, r1) -> - begin match ecode with - | FSQRTx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfrsqrte(rd, r1) -> - begin match ecode with - | FRSQRTEx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfres(rd, r1) -> - begin match ecode with - | FRESx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfsel(rd, r1, r2, r3) -> - begin match ecode with - | FSELx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r3 frB - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pisync -> - begin match ecode with - | ISYNC :: es -> - OK(fw) - >>= recur_simpl - | _ -> error - end - | Plabel(lbl) -> - OK(fw) - >>= lblmap_unify lbl pc - >>^ (fun fw -> {fw with label_list = lbl :: fw.label_list}) - >>= compare_code cs ecode pc - | Plbz(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | LBZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plbz(rd, cst, r1) -> - begin match ecode with - | LBZ(rD, rA, d) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plfd(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | LFD(frD, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plfd(rd, cst, r1) | Plfd_a(rd, cst, r1) -> - begin match ecode with - | LFD(frD, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_csts cst (exts d) - >>= match_iregs r1 rA - >>= recur_simpl - | _ -> error - end - | Plfdx(rd, r1, r2) | Plfdx_a(rd, r1, r2) -> - begin match ecode with - | LFDX(frD, rA, rB) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= 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 (Safe32.of_int 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 - let continue = compare_code cs es (Int32.add 8l pc) in - begin match bitstring_at_vaddr elf vaddr 8l with - | None -> - ERR("Floating point constant address is wrong") - | Some(bs, pofs, psize) -> - let f = - bitmatch bs with - | { f : 64 : int } -> f - in - OK(fw) - >>= (fun ffw -> - begin match section_at_vaddr elf vaddr with - | None -> ERR("No section at that virtual address") - | Some(sndx) -> - let section_name = elf.e_shdra.(sndx).sh_name in - OK( - ffw - >>> ( - ff_sf ^%= - match_sections_name literal_section section_name - ) - ) - end - ) - >>= match_iregs GPR12 rD0 - >>= match_iregs GPR0 rA0 - >>= match_fregs r1 frD1 - >>= match_floats c f - >>^ (ff_ef ^%= add_range pofs psize 8 (Float_literal(f))) - >>= match_iregs GPR12 rA1 - >>= continue - end - | _ -> error - end - | Plfis(r1, c) -> - begin match ecode with - | ADDIS(rD0, rA0, simm0) :: - LFS (frD1, rA1, d1) :: es -> - let vaddr = Int32.( - add (shift_left (Safe32.of_int simm0) 16) (exts d1) - ) in - if Int32.rem vaddr 4l <> 0l - then ERR("Float32 constants should be 4-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 - let continue = compare_code cs es (Int32.add 8l pc) in - begin match bitstring_at_vaddr elf vaddr 4l with - | None -> - ERR("Floating point constant address is wrong") - | Some(bs, pofs, psize) -> - let f = - bitmatch bs with - | { f : 32 : int } -> f - in - OK(fw) - >>= (fun ffw -> - begin match section_at_vaddr elf vaddr with - | None -> ERR("No section at that virtual address") - | Some(sndx) -> - let section_name = elf.e_shdra.(sndx).sh_name in - OK( - ffw - >>> ( - ff_sf ^%= - match_sections_name literal_section section_name - ) - ) - end - ) - >>= match_iregs GPR12 rD0 - >>= match_iregs GPR0 rA0 - >>= match_fregs r1 frD1 - >>= match_floats32 c f - >>^ (ff_ef ^%= add_range pofs psize 4 (Float32_literal(f))) - >>= match_iregs GPR12 rA1 - >>= continue - end - | _ -> error - end - | Plfs(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | LFS(frD, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plfs(rd, cst, r1) -> - begin match ecode with - | LFS(frD, rA, d) :: es -> - OK(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 -> - OK(fw) - >>= match_fregs rd frD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plha(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | LHA(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plha(rd, cst, r1) -> - begin match ecode with - | LHA(rD, rA, d) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plhbrx(rd, r1, r2) -> - begin match ecode with - | LHBRX(rD, rA, rB):: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plhz(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | LHZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plhz(rd, cst, r1) -> - begin match ecode with - | LHZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_csts cst (exts d) - >>= match_iregs r1 rA - >>= recur_simpl - | _ -> error - end - | Plhzx(rd, r1, r2) -> - begin match ecode with - | LHZX(rD, rA, rB) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plwarx(rd, r1, r2) -> - begin match ecode with - | LWARX(rD, rA, rB):: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plwbrx(rd, r1, r2) -> - begin match ecode with - | LWBRX(rD, rA, rB):: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plwz(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | LWZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plwz(rd, cst, r1) | Plwz_a(rd, cst, r1) -> - begin match ecode with - | LWZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Plwzu(rd, cst, r1) -> - begin match ecode with - | LWZU(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Plwzx(rd, r1, r2) | Plwzx_a(rd, r1, r2) -> - begin match ecode with - | LWZX(rD, rA, rB) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pmfcr rd -> - begin match ecode with - | MFCR (rD0) :: es -> - OK(fw) - >>= match_iregs rd rD0 - >>= recur_simpl - | _ -> error - end - | Pmfcrbit(rd, bit) -> - error - | Pmflr(r) -> - begin match ecode with - | MFSPR(rD, spr) :: es -> - OK(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) -> - OK(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 -> - OK(fw) - >>= match_iregs r1 rS - >>= match_ctr spr - >>= recur_simpl - | _ -> error - end - | Pmtlr(r1) -> - begin match ecode with - | MTSPR(rS, spr) :: es -> - OK(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 -> - OK(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 -> - OK(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 - | Pmulhw(rd, r1, r2) -> - begin match ecode with - | MULHWx(rD, rA, rB, rc) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pmulhwu(rd, r1, r2) -> - begin match ecode with - | MULHWUx(rD, rA, rB, rc) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pnand(rd, r1, r2) -> - begin match ecode with - | NANDx(rS, rA, rB, rc) :: es -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> error - end - | Poris(rd, r1, cst) -> - begin match ecode with - | ORIS(rS, rA, uimm) :: es -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> error - end - | Prlwimi(rd, r1, amount, mask) -> - begin match ecode with - | RLWIMIx(rS, rA, sh, mb, me, rc) :: es -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_iregs r2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pstb(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STB(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstb(rd, cst, r1) -> - begin match ecode with - | STB(rS, rA, d) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstfd(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STFD(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfd(rd, cst, r1) | Pstfd_a(rd, cst, r1) -> - begin match ecode with - | STFD(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfdu(rd, cst, r1) -> - begin match ecode with - | STFDU(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfdx(rd, r1, r2) | Pstfdx_a(rd, r1, r2) -> - begin match ecode with - | STFDX(frS, rA, rB) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstfs(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STFS(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfs(rd, cst, r1) -> - begin match ecode with - | STFS(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfsx(rd, r1, r2) -> - begin match ecode with - | STFSX(frS, rA, rB) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Psth(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STH(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Psth(rd, cst, r1) -> - begin match ecode with - | STH(rS, rA, d) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Psthbrx(rd, r1, r2) -> - begin match ecode with - | STHBRX(rS, rA, rB) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstw(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STW(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstw(rd, cst, r1) | Pstw_a(rd, cst, r1) -> - begin match ecode with - | STW(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Pstwu(rd, cst, r1) -> - begin match ecode with - | STWU(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Pstwx(rd, r1, r2) | Pstwx_a(rd, r1, r2) -> - begin match ecode with - | STWX(rS, rA, rB) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstwbrx(rd, r1, r2) -> - begin match ecode with - | STWBRX(rS, rA, rB) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstwcx_(rd, r1, r2) -> - begin match ecode with - | STWCX_(rS, rA, rB) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstwux(rd, r1, r2) -> - begin match ecode with - | STWUX(rS, rA, rB) :: es -> - OK(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 -> - OK(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 -> - OK(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 - | Psubfze(rd, r1) -> - begin match ecode with - | SUBFZEx(rD, rA, oe, rc) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= 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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (exts simm) - >>= recur_simpl - | _ -> error - end - | Psync -> - begin match ecode with - | SYNC :: es -> - OK(fw) - >>= recur_simpl - | _ -> error - end - | Ptrap -> - begin match ecode with - | TW(tO, rA, rB) :: es -> - OK(fw) - >>= (fun ffw -> - bitmatch tO with - | { 31 : 5 : int } -> OK(ffw) - | { _ } -> ERR("bitmatch") - ) - >>= match_iregs GPR0 rA - >>= match_iregs GPR0 rB - >>= recur_simpl - | _ -> error - end - | Pxor(rd, r1, r2) -> - begin match ecode with - | XORx(rS, rA, rB, rc) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> error - end - | Pxoris(rd, r1, cst) -> - begin match ecode with - | XORIS(rS, rA, uimm) :: es -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> 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 -> ERR("Could not find symbol data for function symbol " ^ name) - | Some ecode -> - sfw - >>> sf_ef ^%= - add_log (DEBUG("Processing function: " ^ name)) - >>> (fun sfw -> - { - sf = sfw; - this_sym_ndx = ndx; - this_ident = ident; - label_to_vaddr = PosMap.empty; - label_list = []; - } - ) - >>> compare_code ccode.fn_code 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( - Printf.sprintf - "Unique candidate for %s did not match: %s" - name - 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 for: " ^ name)) - >>> worklist_process wl - | [ffw] -> - worklist_process wl ffw.sf - | fws -> - sfw - >>> sf_ef ^%= - add_log (ERROR( - "Multiple matching candidates for: " ^ name - )) - >>> worklist_process wl - end - end - -(** 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) (bs: bitstring) (sfw: s_framework) - : (s_framework * int) or_err = - 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) or_err = - match l with - | [] -> OK(sfw, s) - | d::l -> - let sfw = - if !debug - then ( - (sf_ef ^%= add_log (DEBUG(" " ^ string_of_init_data d))) sfw - ) - else sfw - in - 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 camlint_of_coqint (Floats.Float32.to_bits f) = 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 camlint64_of_coqint (Floats.Float.to_bits f) = j - then compare_data_aux l bs (s + 8) sfw - else ERR("Wrong float64") - | { _ } -> error - ) - | Init_int64(i) -> ( - bitmatch bs with - | { j : 64 : int; bs : -1 : bitstring } -> - if z_int64 i = j - then compare_data_aux l bs (s + 8) sfw - else ERR("Wrong int64") - | { _ } -> 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 - 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 - (Safe32.of_int (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 = Safe32.of_int 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 " ^ sym.st_name)) - ) - | _ -> (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.ef.elf in - let sym = elf.e_symtab.(ndx) in - let sym_vaddr = sym.st_value in - begin match bitstring_at_vaddr_nosize elf sym_vaddr with - | None -> ERR("Could not find symbol data for data symbol " ^ sym.st_name) - | Some(sym_bs, pofs, psize) -> - let res = - sfw - >>> (sf_ef ^%= add_log (DEBUG("Processing data: " ^ sym.st_name))) - >>> compare_data ldata sym_bs - in - begin match res with - | ERR(s) -> ERR(s) - | OK(sfw, size) -> - let align = - begin match (Hashtbl.find sfw.atoms ident).a_alignment with - | None -> 0 - | Some(a) -> a - end - in - sfw.ef.chkd_data_syms.(ndx) <- true; - OK(sfw) - >>= (fun sfw -> - if size = 0 - then OK(sfw) (* These occupy no space, for now we just forget them *) - else OK( - sfw - >>> sf_ef ^%= - add_range pofs (Safe32.of_int size) align (Data_symbol(sym)) - ) - ) - >>= (fun sfw -> - if not (is_well_aligned sym_vaddr align) - then ERR("Symbol not correctly aligned in the ELF file") - else OK(sfw) - ) - >>^ check_data_symtab ident ndx size - end - end - 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 - ) ^ - "], Errors: [" ^ - string_of_list - (function OK(_) -> "" | ERR(s) -> s) - ", " - (List.filter (function ERR(_) -> true | _ -> false) 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) - -(** Read a .sdump file *) - -let sdump_magic_number = "CompCertSDUMP" ^ Version.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 fatal "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 - -(** Split program definitions into functions and variables *) - -let split_prog_defs p = - let rec split fns vars = function - | [] -> (List.rev fns, List.rev vars) - | (id, Gfun fd) :: defs -> split ((id, fd) :: fns) vars defs - | (id, Gvar vd) :: defs -> split fns ((id, vd) :: vars) defs - in split [] [] p.prog_defs - -(** Processes a .sdump file. -*) -let process_sdump efw sdump: e_framework = - print_debug ("Beginning reading " ^ sdump); - let (prog, names, atoms) = read_sdump sdump in - let (prog_funct, prog_vars) = split_prog_defs prog in - print_debug ("Constructing mapping from idents to symbol indices"); - 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 - print_debug("Constructing worklist"); - let worklist_fundefs = - List.filter - (fun f -> - match snd f with - | Internal _ -> true - | External _ -> false - ) - prog_funct - in - let wl = - List.map - (fun f -> - match f with - | ident, Internal ccode -> (ident, Hashtbl.find names ident, ccode) - | _, External _ -> fatal "IMPOSSIBRU!" - ) - worklist_fundefs - in - print_debug("Beginning processing of the worklist"); - efw - >>> (fun efw -> - { ef = efw - ; program = prog - ; ident_to_name = names - ; ident_to_sym_ndx = ident_to_sym_ndx - ; atoms = atoms - } - ) - >>> worklist_process wl - >>> (fun sfw -> - print_debug "Checking data"; - sfw - ) - >>> check_data prog_vars - >>> (fun sfw -> sfw.ef) - -(** 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 - start <= stop && - 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 = - print_debug "Checking padding"; - 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 - match physical_offset_of_vaddr elf sym.st_value with - | None -> false - | Some(ofs) -> intersect (x, y) ofs sym.st_size - ) - (Array.to_list elf.e_symtab) - ) - ) - in - let unknown x y = Unknown( - "\nSections: " ^ 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 - | [] -> efw - (* if there is only one chunk left, we add an unknown space between it and - the end. *) - | [(_, e, _, _) as h] -> - let elf_size = - Safe32.of_int ((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 -> - 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 *) - || Safe.(of_int32 b2 - of_int32 e1) > a2 (* or if they are too far away *) - || not (is_padding efw.elf.e_bitstring - (Safe32.to_int pad_start) (Safe32.to_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! *) - 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 identification 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 - (* First, let's mark it checked as a data symbol, to avoid warnings *) - efw.chkd_data_syms.(0) <- true; - 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 - -(** If CompCert sections have been mapped to an ELF section whose name is - not the same, we warn the user. -*) -let warn_sections_remapping efw = - print_debug "Checking remapped sections"; - StringMap.fold - (fun c_name (e_name, conflicts) efw -> - if c_name = "COMM" then efw else - if StringSet.is_empty conflicts - then - match e_name with - | Provided(e_name) -> - efw - | Inferred(e_name) -> - if c_name = e_name - then efw - else - begin - efw - >>> add_log (WARNING( - Printf.sprintf - "Detected linker script remapping: section %S -> %S" - c_name e_name - )) - end - else (* conflicts not empty *) - match e_name with - | Provided(e_name) -> - efw - >>> add_log (ERROR( - Printf.sprintf " - Conflicting remappings for section %s: - Specified: %s - Expected: %s" - c_name e_name (string_of_list id ", " (StringSet.elements conflicts)) - )) - | Inferred(e_name) -> - efw - >>> add_log (ERROR( - Printf.sprintf " - Conflicting remappings for section %s: - %s" - c_name (string_of_list id ", " (e_name :: (StringSet.elements conflicts))) - )) - ) - efw.section_map - efw - -let warn_sda_mapping efw = - print_debug "Checking SDA mappings"; - if IntMap.is_empty efw.sda_map - then efw - else ( - IntMap.fold - (fun r vaddr efw -> - match vaddr with - | Provided(_) -> efw - | Inferred(vaddr) -> - efw >>> add_log (WARNING( - Printf.sprintf - "This SDA register mapping was inferred: register r%u = 0x%lX" - r vaddr - )) - ) - efw.sda_map - efw - ) - -let (>>=) li f = List.flatten (List.map f li) - -(** Returns the list of all strictly-ordered pairs of [[0; len - 1]] that don't - satisfy f. *) -let forall_sym (len: int) (f: 'a -> 'a -> bool): ('a * 'a) list = - (list_n len) >>= fun x -> - (list_ab (x + 1) (len - 1)) >>= fun y -> - (if f x y then [] else [(x, y)]) - -let check_overlaps efw = - let shdra = efw.elf.e_shdra in - 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 - match - forall_sym (Array.length shdra) - (fun i j -> - let ai = shdra.(i) in - let aj = shdra.(j) in - (ai.sh_type = SHT_NOBITS) - || (aj.sh_type = SHT_NOBITS) - || (not (intersect ai.sh_offset ai.sh_size aj.sh_offset aj.sh_size)) - ) - with - | [] -> efw - | l -> - List.fold_left - (fun efw (i, j) -> - let msg = - Printf.sprintf "Sections %s and %s overlap" shdra.(i).sh_name shdra.(j).sh_name - in - add_log (ERROR(msg)) efw - ) - efw l - -let check_unknown_chunks efw = - if - List.exists - (function (_, _, _, Unknown(_)) -> true | _ -> false) - efw.chkd_bytes_list - then add_log (WARNING( - "Some parts of the ELF file are unknown." ^ - (if !print_elfmap then "" else " Use -print-elfmap to see what was covered.") - )) efw - else efw - -let check_missed_symbols efw = - if not !exhaustivity - then efw - else - let chkd_syms_a = - Array.init - (Array.length efw.elf.e_symtab) - ( - fun ndx -> - match efw.elf.e_symtab.(ndx).st_type with - (* we only care about function and data symbols *) - | STT_SECTION | STT_FILE -> true - | STT_OBJECT | STT_FUNC | STT_NOTYPE | STT_UNKNOWN -> - (* checked as either a function or a data symbol *) - efw.chkd_fun_syms.(ndx) - || efw.chkd_data_syms.(ndx) - (* or part of the symbols we know are mising *) - || StringSet.mem efw.elf.e_symtab.(ndx).st_name efw.missing_syms - ) - in - let missed_syms_l = list_false_indices chkd_syms_a in - match missed_syms_l with - | [] -> efw - | _ -> - let symtab = efw.elf.e_symtab in - let symlist_names = string_of_list (fun ndx -> symtab.(ndx).st_name) " " in - let missed_funs = - List.filter (fun ndx -> symtab.(ndx).st_type = STT_FUNC) missed_syms_l in - let missed_data = - List.filter (fun ndx -> symtab.(ndx).st_type = STT_OBJECT) missed_syms_l in - let missed_unknown = - List.filter (fun ndx -> - match symtab.(ndx).st_type with - | STT_NOTYPE | STT_UNKNOWN -> true - | _ -> false - ) missed_syms_l in - if !list_missing - then - efw - >>> add_log (WARNING( - Printf.sprintf - " - The following function symbol(s) do not appear in .sdump files: - %s - The following data symbols do not appear in .sdump files: - %s - The following unknown type symbols do not appear in .sdump files: - %s" - (symlist_names missed_funs) - (symlist_names missed_data) - (symlist_names missed_unknown) - )) - else - efw - >>> add_log (WARNING( - Printf.sprintf - "%u function symbol(s), %u data symbol(s) and %u unknown type symbol(s) do not appear in .sdump files. Add -list-missing to list them." - (List.length missed_funs) - (List.length missed_data) - (List.length missed_unknown) - )) - -let print_diagnosis efw = - let (nb_err, nb_warn) = List.fold_left - (fun (e, w) -> function - | DEBUG(_) -> (e, w) - | ERROR(_) -> (e + 1, w) - | INFO(_) -> (e, w) - | WARNING(_) -> (e, w + 1) - ) - (0, 0) - efw.log - in - if !debug - then Printf.printf "\n\nFINAL LOG:\n\n"; - List.(iter - (fun e -> - match string_of_log_entry false e with - | "" -> () - | s -> print_endline s - ) - (rev efw.log) - ); - let plural n = if n > 1 then "s" else "" in - Printf.printf " SUMMARY: %d error%s, %d warning%s\n" - nb_err (plural nb_err) nb_warn (plural nb_warn); - efw - -let conf_file = ref (None: string option) - -let parse_conf filename = - let section_map = ref StringMap.empty in - let sda_map = ref IntMap.empty in - let missing_syms = ref StringSet.empty in - let ic = open_in filename in - try - while true - do - let line = input_line ic in - (* Test different patterns one by one, until one of them works *) - let rec match_line = function - | [] -> failwith (Printf.sprintf "Couldn't read configuration line: %s" line) - | try_match::rest -> - try try_match () - with Scanf.Scan_failure(_) -> match_line rest - in - (* an empty line is ignored *) - if line <> "" - then - match_line - (* a comment *) - [ (fun () -> - Scanf.sscanf line - "#%s" - (fun _ -> ()) - ) - (* a section remapping *) - ; (fun () -> - Scanf.sscanf line - "section %S -> %S" - (fun sfrom sto -> - if StringMap.mem sfrom !section_map - then failwith ( - Printf.sprintf - "Your configuration file contains multiple mappings for section %s" - sfrom - ) - else - section_map := - StringMap.add sfrom (Provided(sto), StringSet.empty) !section_map - ) - ) - (* a SDA mapping *) - ; (fun () -> - Scanf.sscanf line - "register r%u = %li" - (fun r addr -> - if IntMap.mem r !sda_map - then failwith ( - Printf.sprintf - "Your configuration file contains multiple SDA mappings for register %u" - r - ) - else - sda_map := IntMap.add r (Provided(addr)) !sda_map) - ) - (* a list of symbols supposed to be missing from the .sdump files *) - ; (fun () -> - Scanf.sscanf line - "external %s@\n" - (fun sym_list_s -> - let sym_list = Str.split (Str.regexp "[ \t]+") sym_list_s in - List.iter - (fun sym -> missing_syms := StringSet.add sym !missing_syms) - sym_list - ) - ) - ] - done; raise End_of_file (* unreachable, just to please the typer *) - with - | End_of_file -> (!section_map, !sda_map, !missing_syms) - -(** Checks a whole ELF file according to a list of .sdump files. This never - dumps anything, so it can be safely used when fuzz-testing even if the - user accidentally enabled dumping options. *) -let check_elf_nodump elf sdumps = - let eh = elf.e_hdr in - let nb_syms = Array.length elf.e_symtab 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.(Safe32.to_int symtab_shdr.sh_link) in - let (section_map, sda_map, missing_syms) = - match !conf_file with - | None -> (StringMap.empty, IntMap.empty, StringSet.empty) - | Some(filename) -> parse_conf filename - in - let efw = - { elf = elf - ; log = [] - ; chkd_bytes_list = [] - ; chkd_fun_syms = Array.make nb_syms false - ; chkd_data_syms = Array.make nb_syms false - ; section_map = section_map - ; sda_map = sda_map - ; missing_syms = missing_syms - } - >>> check_elf_header - >>> add_range - eh.e_phoff - Safe.(to_int32 (eh.e_phnum * eh.e_phentsize)) - 4 - ELF_progtab - >>> add_range - eh.e_shoff - Safe.(to_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 - print_debug "Done checking header, beginning processing of .sdumps"; - (* Thread the framework through the processing of all .sdump files *) - List.fold_left process_sdump efw sdumps - (* check the padding in between identified byte chunks *) - >>> check_padding - (* warn if some CompCert sections have been remapped by the linker script *) - >>> warn_sections_remapping - (* warn if there exists non-empty overlapping sections *) - >>> check_overlaps - (* warn about inferred SDA registers *) - >>> warn_sda_mapping - (* warn about regions of the ELF file that could not be identified *) - >>> check_unknown_chunks - >>> check_missed_symbols - >>> print_diagnosis - -(** 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_elf_dump elffilename sdumps = - print_debug "Beginning ELF parsing"; - let elf = read_elf elffilename in - print_debug "Beginning ELF checking"; - let efw = check_elf_nodump elf sdumps in - (* print the elfmap if requested *) - if !print_elfmap - then - begin - Printf.printf "\n\n%s\n\n\n" - (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 - ) - end; - (* dump the elfmap if requested *) - if !dump_elfmap - then - begin - let oc = open_out (elffilename ^ ".elfmap") in - output_value oc efw.chkd_bytes_list; - close_out oc - end diff --git a/checklink/Disassembler.ml b/checklink/Disassembler.ml deleted file mode 100644 index 0e2c6883..00000000 --- a/checklink/Disassembler.ml +++ /dev/null @@ -1,15 +0,0 @@ -open ELF_parsers -open ELF_types -open PPC_printers -open PPC_utils - -let disassemble elf sym_name = - let sym = - List.find - (fun sym -> sym.st_name = sym_name) - (Array.to_list elf.e_symtab) - in - match code_of_sym elf sym with - | None -> "Couldn't find the code for that symbol name" - | Some(ecode) -> - string_of_instr_list ecode diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml deleted file mode 100644 index 8c2d486c..00000000 --- a/checklink/ELF_parsers.ml +++ /dev/null @@ -1,362 +0,0 @@ -open Bitstring_utils -open ELF_types -open ELF_printers -open ELF_utils -open Library -open PPC_parsers - -(** Allows relaxations of the parser: - - 1. Any segment that has the same p_offset and p_memsz as another segment, - and a null p_filesz, will be considered as having a p_filesz equal to the - other segment. This allow symbol's contents resolution to succeed even in - the presence of a bootstrapping copy mechanism from one segment to the - other. -*) -let relaxed = ref false - -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 = - begin match ei_data with - | 0 -> ELFDATANONE - | 1 -> ELFDATA2LSB - | 2 -> ELFDATA2MSB - | _ -> ELFDATAUNKNOWN - end - 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 = - begin match ei_class with - | 0 -> ELFCLASSNONE - | 1 -> ELFCLASS32 - | 2 -> ELFCLASS64 - | _ -> ELFCLASSUNKNOWN - end; - ei_data = ei_data; - ei_version = - begin match ei_version with - | 0 -> EV_NONE - | 1 -> EV_CURRENT - | _ -> EV_UNKNOWN - end; - }; - e_type = - begin match e_type with - | 0 -> ET_NONE - | 1 -> ET_REL - | 2 -> ET_EXEC - | 3 -> ET_DYN - | 4 -> ET_CORE - | _ -> ET_UNKNOWN - end; - e_machine = - begin 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 - end; - e_version = - begin match e_version with - | 0l -> EV_NONE - | 1l -> EV_CURRENT - | _ -> EV_UNKNOWN - end; - 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 = - Safe.(of_int32 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 bit_ofs = Safe.( - (section_header_offset e_hdr num) * 8 - ) in - bitmatch bs with - | { sh_name : 32 : endian(e), offset(bit_ofs) ; - 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 (Safe32.to_int sh_name); - sh_type = - begin 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 - end; - 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 bit_ofs = Safe.( - ((of_int32 e_hdr.e_phoff) + (ndx * e_hdr.e_phentsize)) * 8 - ) in - bitmatch bs with - | { p_type : 32 : endian(e), offset(bit_ofs) ; - 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 = - begin 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 - end; - 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 - let bit_ofs = Safe.(num * 128) in (* each symbol takes 16 bytes = 128 bits *) - bitmatch symtab with - | { st_name : 32 : endian(e), offset(bit_ofs) ; - 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 (Safe32.to_int st_name) ; - st_value = st_value ; - st_size = st_size ; - st_bind = - begin match st_bind with - | 0 -> STB_LOCAL - | 1 -> STB_GLOBAL - | 2 -> STB_WEAK - | _ -> STB_UNKNOWN - end; - st_type = - begin match st_type with - | 0 -> STT_NOTYPE - | 1 -> STT_OBJECT - | 2 -> STT_FUNC - | 3 -> STT_SECTION - | 4 -> STT_FILE - | _ -> STT_UNKNOWN - end; - st_other = st_other ; - st_shndx = st_shndx ; - } - -(** 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 - let skipped_bits = Safe.(strtab_shofs * 8 + 128) in - bitmatch bs with - | { ofs : 32 : endian(e), offset(skipped_bits) ; - size : 32 : endian(e) } -> - Bitstring.subbitstring bs Safe.(of_int32 ofs * 8) Safe.(of_int32 size * 8) - ) - in - let e_shdra = - Array.init e_hdr.e_shnum (read_elf32_shdr e_hdr bs strtab) - in - let symtab_sndx = section_ndx_by_name_noelf e_shdra ".symtab" in - let e_symtab = ( - let symtab_shdr = e_shdra.(symtab_sndx) in - let symtab_strtab_sndx = symtab_shdr.sh_link in - let symtab_nb_ent = (Safe32.to_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 (Safe32.to_int symtab_strtab_sndx))) - ) in - let e_phdra = - let untweaked = Array.init e_hdr.e_phnum (read_elf32_phdr e_hdr bs) in - if !relaxed - then - Array.mapi - (fun ndx curr -> - if ndx < 1 - then curr - else - let prev = untweaked.(ndx - 1) in - if (curr.p_offset = prev.p_offset) - && (curr.p_memsz = prev.p_memsz) - then { curr with p_filesz = prev.p_filesz } - else curr - ) - untweaked - else untweaked - in - let e_sym_phdr = - let intervals = - Array.mapi - (fun ndx phdr -> (* (ndx, (start, stop), type) *) - (ndx, - (phdr.p_vaddr, Safe32.(phdr.p_vaddr + phdr.p_memsz - 1l)), - phdr.p_type - ) - ) - e_phdra - in - let intervals = Array.of_list ( - List.filter - (function (_, _, PT_LOAD) -> true | _ -> false) - (Array.to_list intervals) - ) in - Array.fast_sort (fun (_, (x, _), _) (_, (y, _), _) -> compare x y) intervals; - let lookup = - sorted_lookup - ( - fun (_, (a, b), _) v -> - if a <= v && v <= b - then 0 - else compare a v - ) - intervals - in - fun vaddr -> - begin match lookup vaddr with - | None -> None - | Some(ndx, (_, _), _) -> Some(ndx) - end - in - let e_syms_by_name = - let m = ref StringMap.empty in - for i = 0 to Array.length e_symtab - 1 do - let name = strip_versioning e_symtab.(i).st_name in - let list = try StringMap.find name !m with Not_found -> [] in - m := StringMap.add name (i :: list) !m - done; - !m - in - { - e_bitstring = bs; - e_hdr = e_hdr; - e_shdra = e_shdra; - e_phdra = e_phdra; - e_symtab = e_symtab; - e_symtab_sndx = symtab_sndx; - e_sym_phdr = e_sym_phdr; - e_syms_by_name = e_syms_by_name; - } - -(** 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 deleted file mode 100644 index 82ba479b..00000000 --- a/checklink/ELF_printers.ml +++ /dev/null @@ -1,206 +0,0 @@ -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 = - Printf.sprintf - "{ -ei_class = %s; -ei_data = %s; -ei_version = %s; -}" - (string_of_elfclass ei.ei_class ) - (string_of_elfdata ei.ei_data ) - (string_of_ev ei.ei_version) - -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 = - Printf.sprintf - "{ -e_ident = %s; -e_type = %s; -e_machine = %s; -e_version = %s; -e_entry = %s; -e_phoff = %s; -e_shoff = %s; -e_flags = %s; -e_ehsize = %s; -e_phentsize = %s; -e_phnum = %s; -e_shentsize = %s; -e_shnum = %s; -e_shstrndx = %s; -}" - (string_of_elf_identification eh.e_ident ) - (string_of_et eh.e_type ) - (string_of_em eh.e_machine ) - (string_of_ev eh.e_version ) - (string_of_elf32_addr eh.e_entry ) - (string_of_elf32_off eh.e_phoff ) - (string_of_elf32_off eh.e_shoff ) - (string_of_bitstring eh.e_flags ) - (string_of_elf32_half eh.e_ehsize ) - (string_of_elf32_half eh.e_phentsize) - (string_of_elf32_half eh.e_phnum ) - (string_of_elf32_half eh.e_shentsize) - (string_of_elf32_half eh.e_shnum ) - (string_of_elf32_half eh.e_shstrndx ) - -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 = - Printf.sprintf - "{ -sh_name = %s; -sh_type = %s; -sh_flags = %s; -sh_addr = %s; -sh_offset = %s; -sh_size = %s; -sh_link = %s; -sh_info = %s; -sh_addralign = %s; -sh_entsize = %s; -}" - (sh.sh_name ) - (string_of_sht sh.sh_type ) - (string_of_elf32_word sh.sh_flags ) - (string_of_elf32_addr sh.sh_addr ) - (string_of_elf32_off sh.sh_offset ) - (string_of_elf32_word sh.sh_size ) - (string_of_elf32_word sh.sh_link ) - (string_of_elf32_word sh.sh_info ) - (string_of_elf32_word sh.sh_addralign) - (string_of_elf32_word sh.sh_entsize ) - -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 = - Printf.sprintf - "{ -p_type = %s; -p_offset = %s; -p_vaddr = %s; -p_paddr = %s; -p_filesz = %s; -p_memsz = %s; -p_flags = %s; -p_align = %s; -}" - (string_of_p_type ph.p_type ) - (string_of_elf32_off ph.p_offset) - (string_of_elf32_addr ph.p_vaddr ) - (string_of_elf32_addr ph.p_paddr ) - (string_of_elf32_word ph.p_filesz) - (string_of_elf32_word ph.p_memsz ) - (string_of_bitstring ph.p_flags ) - (string_of_elf32_word ph.p_align ) - -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 = - Printf.sprintf - "{ -st_name = %s; -st_value = %s; -st_size = %s; -st_bind = %s; -st_type = %s; -st_other = %s; -st_shndx = %s; -}" - (s.st_name ) - (string_of_elf32_addr s.st_value) - (string_of_elf32_word s.st_size ) - (string_of_elf32_st_bind s.st_bind ) - (string_of_elf32_st_type s.st_type ) - (string_of_int s.st_other) - (string_of_elf32_half s.st_shndx) - -let string_of_elf e = - Printf.sprintf - "{ -e_header = %s; -e_sections = %s; -e_programs = %s; -e_symtab = %s; -}" - (string_of_elf32_ehdr e.e_hdr ) - (string_of_array string_of_elf32_shdr ",\n" e.e_shdra) - (string_of_array string_of_elf32_phdr ",\n" e.e_phdra) - (string_of_array string_of_elf32_sym ",\n" e.e_symtab) diff --git a/checklink/ELF_types.ml b/checklink/ELF_types.ml deleted file mode 100644 index f67b91d1..00000000 --- a/checklink/ELF_types.ml +++ /dev/null @@ -1,170 +0,0 @@ -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 (* section index of the symbol table *) - ; e_sym_phdr : int32 -> int option (* fast sym -> phdr lookup *) - ; e_syms_by_name : int list StringMap.t (* fast name -> sym lookup *) - } diff --git a/checklink/ELF_utils.ml b/checklink/ELF_utils.ml deleted file mode 100644 index 898c778d..00000000 --- a/checklink/ELF_utils.ml +++ /dev/null @@ -1,128 +0,0 @@ -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 = Safe32.to_int eshdra.(sndx).sh_offset in - let size = Safe32.to_int eshdra.(sndx).sh_size in - Bitstring.subbitstring bs Safe.(sofs * 8) Safe.(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)(vaddr: int32): int32 option = - begin match e.e_sym_phdr vaddr with - | None -> None - | Some(pndx) -> - let phdr = e.e_phdra.(pndx) in - let vaddr_ofs = Safe32.(vaddr - phdr.p_vaddr) in - Some(Safe32.(phdr.p_offset + vaddr_ofs)) - end - -(* TODO: could make this more efficient, but it's not often called *) -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 bitstring of the specified byte size beginning at the specified - virtual address, along with its physical byte offset and physical byte size, - that is, the space it occupies in the file. -*) -let bitstring_at_vaddr (e: elf)(vaddr: int32)(size:int32): - (bitstring * int32 * int32) option = - match e.e_sym_phdr vaddr with - | None -> None - | Some(pndx) -> - let phdr = e.e_phdra.(pndx) in - let phdr_mem_first = phdr.p_vaddr in - let phdr_mem_last = Safe32.(phdr.p_vaddr + phdr.p_memsz - 1l) in - let vaddr_mem_first = vaddr in - let vaddr_mem_last = Safe32.(vaddr + size - 1l) in - if not (phdr_mem_first <= vaddr_mem_first && vaddr_mem_last <= phdr_mem_last) - then None (* we're overlapping segments *) - else - let vaddr_relative_ofs = Safe32.(vaddr_mem_first - phdr_mem_first) in - let vaddr_file_ofs = Safe32.(phdr.p_offset + vaddr_relative_ofs) in - if phdr.p_filesz = 0l || vaddr_relative_ofs > phdr.p_filesz - then - Some( - Bitstring.create_bitstring Safe32.(to_int (8l * size)), - phdr.p_offset, (* whatever? *) - 0l - ) - else if Safe32.(vaddr_relative_ofs + size) > phdr.p_filesz - then - let bit_start = Safe32.(to_int (8l * vaddr_file_ofs)) in - let vaddr_file_len = Safe32.(phdr.p_filesz - vaddr_relative_ofs) in - let bit_len = Safe32.(to_int (8l * vaddr_file_len)) in - let first = Bitstring.subbitstring e.e_bitstring bit_start bit_len in - let rest = Bitstring.create_bitstring (8 * Safe32.to_int size - bit_len) in - Some( - Bitstring.concat [first; rest], - vaddr_file_ofs, - vaddr_file_len - ) - else - let bit_start = Safe32.(to_int (8l * (phdr.p_offset + vaddr_relative_ofs))) in - let bit_len = Safe.(8 * Safe32.to_int size) in - Some( - Bitstring.subbitstring e.e_bitstring bit_start bit_len, - vaddr_file_ofs, - size - ) - -(** - Returns the entire bitstring that begins at the specified virtual address and - ends at the end of the segment. -*) -let bitstring_at_vaddr_nosize (e: elf)(vaddr: int32): - (bitstring * int32 * int32) option = - match e.e_sym_phdr vaddr with - | None -> None - | Some(pndx) -> - let phdr = e.e_phdra.(pndx) in - let first_byte_vaddr = vaddr in - let last_byte_vaddr = Safe32.(phdr.p_vaddr + phdr.p_memsz - 1l) in - let size = Safe32.(last_byte_vaddr - first_byte_vaddr + 1l) in - bitstring_at_vaddr e vaddr size - -(** - 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 list of all symbols matching the specified name. -*) -let ndxes_of_sym_name (e: elf) (name: string): int list = - try StringMap.find (strip_mangling name) e.e_syms_by_name with Not_found -> [] - -(** - 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 = - match ndxes_of_sym_name e name with - | [] -> None - | h::_ -> Some(h) diff --git a/checklink/Exc.ml b/checklink/Exc.ml deleted file mode 100644 index 101087d2..00000000 --- a/checklink/Exc.ml +++ /dev/null @@ -1,2 +0,0 @@ -exception IntOverflow -exception Int32Overflow diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml deleted file mode 100644 index 30c0b381..00000000 --- a/checklink/Frameworks.ml +++ /dev/null @@ -1,214 +0,0 @@ -open Camlcoq -open Asm -open AST -open ELF_types -open Lens -open Library - -type log_entry = - | DEBUG of string - | ERROR of string - | INFO of string - | WARNING 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 int64 - | Float32_literal of int32 - | Padding - | Unknown of string - -(* This type specifies whether its argument was inferred by the tool or provided - via a config file. *) -type 'a inferrable = - | Inferred of 'a - | Provided of 'a - -let from_inferrable = function -| Inferred(x) -> x -| Provided(x) -> x - -(** This framework is carried along while analyzing the whole ELF file. -*) -type e_framework = { - elf: elf; - log: log_entry list; - (** 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; - chkd_fun_syms: bool array; - chkd_data_syms: bool array; - (** The mapping from CompCert sections to ELF sections will be inferred along - the way. This way, we can check things without prior knowledge of the - linker script. The set holds conflicts for the mapping, if more than one - mapping is inferred. These are reported once, at the end. *) - section_map: (string inferrable * StringSet.t) StringMap.t; - (** We will assign a virtual address to each register that can act as an SDA - base register. *) - sda_map: (int32 inferrable) IntMap.t; - (** Contains the symbols that we expect to be missing from the .sdump files *) - missing_syms: StringSet.t; -} - -module PosOT = struct - type t = P.t - 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; - (** 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 section_map = { - get = (fun ef -> ef.section_map); - set = (fun m ef -> { ef with section_map = m }); -} - -let sda_map = { - get = (fun ef -> ef.sda_map); - set = (fun m ef -> { ef with sda_map = m }); -} - -let ident_to_sym_ndx = { - get = (fun sf -> sf.ident_to_sym_ndx); - set = (fun i sf -> { sf with ident_to_sym_ndx = 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 = Safe32.(start + length - 1l) in - { - efw with - 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 or_err) (f: 'a -> 'b): 'b or_err = - match a with - | ERR(s) -> ERR(s) - | OK(x) -> OK(f x) - -let ( >>= ) (a: 'a or_err) (f: 'a -> 'b or_err): 'b or_err = - match a with - | ERR(s) -> ERR(s) - | OK(x) -> f x - -let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b or_err) - (arg: 'a): 'a or_err = - let focus = arg |. lens in - match transf focus with - | OK(res) -> OK((lens ^= res) arg) - | ERR(s) -> ERR(s) - -(** Finally, some printers. -*) - -let format_logtype = Printf.sprintf "%10s" - -let string_of_log_entry show_debug entry = - match entry with - | DEBUG(s) -> if show_debug then (format_logtype "DEBUG: ") ^ s else "" - | ERROR(s) -> (format_logtype "ERROR: ") ^ s - | INFO(s) -> (format_logtype "INFO: ") ^ s - | WARNING(s) -> (format_logtype "WARNING: ") ^ s - -let fatal s = failwith ((format_logtype "FATAL: ") ^ s) - -let verbose_elfmap = ref false - -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_int64 f -| Float32_literal(f) -> "Float32 literal: " ^ string_of_int32 f -| Padding -> "Padding" -| Unknown(s) -> "???" ^ (if !verbose_elfmap then s else "") diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml deleted file mode 100644 index dc984934..00000000 --- a/checklink/Fuzz.ml +++ /dev/null @@ -1,175 +0,0 @@ -open Check -open ELF_parsers -open ELF_types -open Frameworks -open Library - -let fuzz_debug = ref false - -let string_of_byte = Printf.sprintf "0x%02x" - -let full_range_of_byte elfmap byte = - let byte = Int32.of_int 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 - -(** [fuzz_check] will print what happened on stderr, and report errors (that is, - when the check went fine) to stdout. -*) -let fuzz_check elfmap bs byte old sdumps = - let is_error = function ERROR(_) -> true | _ -> false in - let (str, _, _) = bs in - let fuzz_description = - string_of_int32 (Int32.of_int 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) - in - if !fuzz_debug - then print_endline fuzz_description; - try - (* The point here is to go all the way through the checks, and see whether - the checker returns an ERROR or raises an exception. If not, then we - might be missing a bug! - *) - let elf = read_elf_bs bs in - let efw = check_elf_nodump elf sdumps in - if List.exists is_error efw.log - then (* finding an ERROR is the expected behavior *) - begin - if !fuzz_debug - then print_endline ( - string_of_log_entry false (List.find is_error efw.log) - ) - end - else (* not finding an ERROR is bad thus reported *) - print_endline (fuzz_description ^ " DID NOT CAUSE AN ERROR!") - with - | Assert_failure(s, l, c) -> - if !fuzz_debug - then Printf.printf "fuzz_check failed an assertion at %s (%d, %d)\n" s l c - | Exc.IntOverflow | Exc.Int32Overflow -> - if !fuzz_debug - then Printf.printf "fuzz_check raised an integer overflow exception\n" - | Match_failure(s, l, c) -> - if !fuzz_debug - then Printf.printf "fuzz_check raised a match failure at %s (%d, %d)\n" s l c - | Not_found -> - if !fuzz_debug - then Printf.printf "fuzz_check raised a not found exception\n" - | Invalid_argument(s) -> - if !fuzz_debug - then Printf.printf "fuzz_check raised an invalid argument: %s\n" s - | ELF_parsers.Unknown_endianness -> - if !fuzz_debug - then Printf.printf "fuzz_check raised an unknown endianness exception\n" - -(** Tries to prevent some easy-to-catch false positives. Some known false - positives are however hard to predict. For instance, when the virtual - address of a stub is replaced by the virtual address of another exact - same stub. -*) -let ok_fuzz elfmap str byte fuzz = - let (a, b, _, r) = full_range_of_byte elfmap byte in - let a = Safe32.to_int a 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(_) -> true - | 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(_) -> true - | Float32_literal(_) -> true - (* padding is allowed to be non-null, but won't be recognized as padding, but - as unknown, which is not an ERROR *) - | Padding -> false - | 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 - -(** Randomly fuzz bytes forever *) -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 rec fuzz_every_byte_once_aux elfmap bs sdumps (current: int): unit = - let (str, ofs, len) = bs in - if current = len / 8 (* len is in bits *) - then () - else ( - let fuzz = fuzz_byte str current in - if ok_fuzz elfmap str current fuzz - then ( - let str' = String.copy str in - str'.[current] <- fuzz; - fuzz_check elfmap (str', ofs, len) current str.[current] sdumps - ); - fuzz_every_byte_once_aux elfmap bs sdumps (current + 1) - ) - -(** Fuzz each byte of the file once with a random new value *) -let fuzz_every_byte_once elffilename sdumps = - let elfmap = get_elfmap elffilename in - let bs = Bitstring.bitstring_of_file elffilename in - fuzz_every_byte_once_aux elfmap bs sdumps 0 - -(** Fuzz each byte of the file, then loop *) -let fuzz_every_byte_loop elffilename sdumps = - let elfmap = get_elfmap elffilename in - let bs = Bitstring.bitstring_of_file elffilename in - let rec fuzz_every_byte_loop_aux () = - fuzz_every_byte_once_aux elfmap bs sdumps 0; - fuzz_every_byte_loop_aux () - in fuzz_every_byte_loop_aux () diff --git a/checklink/Lens.ml b/checklink/Lens.ml deleted file mode 100644 index 43359334..00000000 --- a/checklink/Lens.ml +++ /dev/null @@ -1,32 +0,0 @@ -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 deleted file mode 100644 index 54bca411..00000000 --- a/checklink/Library.ml +++ /dev/null @@ -1,171 +0,0 @@ -open Camlcoq - -type bitstring = Bitstring.bitstring - -module IntMap = Map.Make(struct type t = int let compare = compare end) -module StringMap = Map.Make (String) -module StringSet = Set.Make (String) - -let is_some: 'a option -> bool = function -| Some(_) -> true -| None -> false - -let from_some: 'a option -> 'a = function -| Some(x) -> x -| None -> raise Not_found - -let filter_some (l: 'a option list): 'a list = - List.(map from_some (filter is_some l)) - -type 'a or_err = - | OK of 'a - | ERR of string - -let is_ok: 'a or_err -> bool = function -| OK(_) -> true -| ERR(_) -> false - -let is_err x = not (is_ok x) - -let from_ok: 'a or_err -> 'a = function -| OK(x) -> x -| ERR(_) -> assert false - -let from_err: 'a or_err -> string = function -| OK(_) -> assert false -| ERR(s) -> s - -let filter_ok (l: 'a or_err list): 'a list = - List.(map from_ok (filter is_ok l)) - -let filter_err (l: 'a or_err list): string list = - List.(map from_err (filter is_err l)) - -external id : 'a -> 'a = "%identity" - -(** [a; a + 1; ... ; b - 1; b] *) -let list_ab (a: int) (b: int): int list = - let rec list_ab_aux a b res = - if b < a - then res - else list_ab_aux a (b - 1) (b :: res) - in list_ab_aux a b [] - -(** [0; 1; ...; n - 1] *) -let list_n (n: int): int list = - list_ab 0 (n - 1) - -(** 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) - -exception IntOverflow -exception Int32Overflow - -(* Can only return positive numbers 0 <= res < 2^31 *) -let positive_int32 p = - let rec positive_int32_unsafe = function - | P.Coq_xI(p) -> Int32.(add (shift_left (positive_int32_unsafe p) 1) 1l) - | P.Coq_xO(p) -> Int32.(shift_left (positive_int32_unsafe p) 1) - | P.Coq_xH -> 1l - in - let res = positive_int32_unsafe p in - if res >= 0l - then res - else raise IntOverflow - -(* This allows for 1 bit of overflow, effectively returning a negative *) -let rec positive_int32_lax = function -| P.Coq_xI(p) -> - let acc = positive_int32_lax p in - if acc < 0l - then raise Int32Overflow - else Int32.(add (shift_left acc 1) 1l) -| P.Coq_xO(p) -> - let acc = positive_int32_lax p in - if acc < 0l - then raise Int32Overflow - else Int32.shift_left acc 1 -| P.Coq_xH -> 1l - -let z_int32 = function -| Z.Z0 -> 0l -| Z.Zpos(p) -> positive_int32 p -| Z.Zneg(p) -> Int32.neg (positive_int32 p) - -let z_int32_lax = function -| Z.Z0 -> 0l -| Z.Zpos(p) -> positive_int32_lax p -| Z.Zneg(_) -> raise Int32Overflow - -let z_int z = Safe32.to_int (z_int32 z) - -let z_int_lax z = Safe32.to_int (z_int32_lax z) - -let z_int64 = Camlcoq.Z.to_int64 - -(* Some more printers *) - -let string_of_ffloat f = string_of_float (camlfloat_of_coqfloat f) -let string_of_ffloat32 f = string_of_float (camlfloat_of_coqfloat32 f) - -let string_of_array string_of_elt sep a = - let b = Buffer.create 1024 in - Buffer.add_string b "[\n"; - Array.iteri - (fun ndx elt -> - if ndx > 0 then Buffer.add_string b sep; - Buffer.add_string b (string_of_int ndx); - Buffer.add_string b ": "; - Buffer.add_string b (string_of_elt elt) - ) a; - Buffer.add_string b "\n]"; - Buffer.contents b - -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" -let string_of_int64 = Printf.sprintf "0x%08Lx" -(* To print counts/indices *) -let string_of_int32i = Int32.to_string -let string_of_int64i = Int64.to_string - -let string_of_positive p = string_of_int32i (positive_int32 p) - -let string_of_z z = string_of_int32 (z_int32 z) - -let sorted_lookup (compare: 'a -> 'b -> int) (arr: 'a array) (v: 'b): 'a option = - let rec sorted_lookup_aux (i_from: int) (i_to: int): 'a option = - if i_from > i_to - then None - else - let i_mid = (i_from + i_to) / 2 in - let comp = compare arr.(i_mid) v in - if comp < 0 (* v_mid < v *) - then sorted_lookup_aux (i_mid + 1) i_to - else if comp > 0 - then sorted_lookup_aux i_from (i_mid - 1) - else Some(arr.(i_mid)) - in sorted_lookup_aux 0 (Array.length arr - 1) - -let list_false_indices a = - filter_some (Array.(to_list (mapi (fun ndx b -> if b then None else Some(ndx)) a))) diff --git a/checklink/Makefile b/checklink/Makefile deleted file mode 100644 index 1518e2c6..00000000 --- a/checklink/Makefile +++ /dev/null @@ -1,52 +0,0 @@ -TESTS=c arcode lzw lzss raytracer regression spass - -.PHONY: all $(TESTS) - -all: $(TESTS) - -CL=../cchecklink $(ARGS) -TESTDIR=../test - -C=aes almabench binarytrees bisect chomp fannkuch fft fib integr knucleotide \ - lists mandelbrot nbody nsievebits nsieve perlin qsort sha1 spectral vmach - -c: - for x in $(C); do \ - echo $(CL) $(TESTDIR)/c/$$x.compcert $(TESTDIR)/c/$$x.sdump; \ - $(CL) $(TESTDIR)/c/$$x.compcert $(TESTDIR)/c/$$x.sdump; \ - done - -ARCODE=optlist bitfile arcode armain -ARCODE_SDUMP=$(addsuffix .sdump, $(ARCODE)) -arcode: - $(CL) $(addprefix $(TESTDIR)/compression/, arcode $(ARCODE_SDUMP)) - -LZW=optlist bitfile lzwencode lzwdecode lzwmain -LZW_SDUMP=$(addsuffix .sdump, $(LZW)) -lzw: - $(CL) $(addprefix $(TESTDIR)/compression/, lzw $(LZW_SDUMP)) - -LZSS=optlist bitfile lzvars lzhash lzencode lzdecode -LZSS_SDUMP=$(addsuffix .sdump, $(LZSS)) -lzss: - $(CL) $(addprefix $(TESTDIR)/compression/, lzss $(LZSS_SDUMP)) - -RAYTRACER_SDUMP=`ls $(TESTDIR)/raytracer/*.sdump` -raytracer: - $(CL) $(TESTDIR)/raytracer/render $(RAYTRACER_SDUMP) - -SDUMP_COMPCERT=`echo $$x | sed s/sdump/compcert/` -REGRESSION_SDUMP=`ls $(TESTDIR)/regression/*.sdump` -regression: - for x in $(REGRESSION_SDUMP); \ - do \ - if [ -f $(SDUMP_COMPCERT) ] ; \ - then \ - echo $(CL) $(SDUMP_COMPCERT) $$x; \ - $(CL) $(SDUMP_COMPCERT) $$x ; \ - fi ; \ - done - -SPASS_SDUMP=`ls $(TESTDIR)/spass/*.sdump` -spass: - $(CL) $(TESTDIR)/spass/spass $(SPASS_SDUMP) diff --git a/checklink/PPC_parsers.ml b/checklink/PPC_parsers.ml deleted file mode 100644 index 5fb8c2d9..00000000 --- a/checklink/PPC_parsers.ml +++ /dev/null @@ -1,397 +0,0 @@ -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; 26: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) - -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 assert false - -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 deleted file mode 100644 index 5aa9a040..00000000 --- a/checklink/PPC_printers.ml +++ /dev/null @@ -1,203 +0,0 @@ -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 deleted file mode 100644 index b3419db0..00000000 --- a/checklink/PPC_types.ml +++ /dev/null @@ -1,198 +0,0 @@ -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 deleted file mode 100644 index 6c865dd0..00000000 --- a/checklink/PPC_utils.ml +++ /dev/null @@ -1,26 +0,0 @@ -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 = - begin match bitstring_at_vaddr e vaddr (Safe32.of_int (4 * nb_instr)) with - | None -> None - | Some(code_bs, _, _) -> Some (parse_code_as_list code_bs) - end - -let code_of_sym (e: elf) (sym: elf32_sym): ecode option = - begin match bitstring_at_vaddr e sym.st_value sym.st_size with - | None -> None - | Some(bs, _, _) -> Some(parse_code_as_list bs) - end - -let code_of_sym_ndx (e: elf) (ndx: int): ecode option = - code_of_sym e e.e_symtab.(ndx) - -let code_of_sym_name (e: elf) (name: string): ecode option = - begin match ndx_of_sym_name e name with - | Some ndx -> code_of_sym_ndx e ndx - | None -> None - end diff --git a/checklink/Safe.ml b/checklink/Safe.ml deleted file mode 100644 index efcd3bd6..00000000 --- a/checklink/Safe.ml +++ /dev/null @@ -1,25 +0,0 @@ -(* "Hacker's Delight", section 2.12 *) - -let ( + ) x y = - let z = x + y in - (* Overflow occurs iff x and y have same sign and z's sign is different *) - if (z lxor x) land (z lxor y) < 0 - then raise Exc.IntOverflow - else z - -let ( - ) x y = - let z = x - y in - (* Overflow occurs iff x and y have opposite signs and z and x have - opposite signs *) - if (x lxor y) land (z lxor x) < 0 - then raise Exc.IntOverflow - else z - -let ( * ) x y = - let z = x * y in - if (x = min_int && y < 0) || (y <> 0 && z / y <> x) - then raise Exc.IntOverflow - else z - -let of_int32 = Safe32.to_int -let to_int32 = Safe32.of_int diff --git a/checklink/Safe32.ml b/checklink/Safe32.ml deleted file mode 100644 index e72563d7..00000000 --- a/checklink/Safe32.ml +++ /dev/null @@ -1,34 +0,0 @@ -(* "Hacker's Delight", section 2.12 *) - -let ( + ) x y = Int32.( - let z = add x y in - (* Overflow occurs iff x and y have same sign and z's sign is different *) - if logand (logxor z x) (logxor z y) < 0l - then raise Exc.Int32Overflow - else z -) - -let ( - ) x y = Int32.( - let z = sub x y in - (* Overflow occurs iff x and y have opposite signs and z and x have - opposite signs *) - if logand (logxor x y) (logxor z x) < 0l - then raise Exc.Int32Overflow - else z -) - -let ( * ) x y = Int32.( - let z = mul x y in - if (x = min_int && y < 0l) || (y <> 0l && div z y <> x) - then raise Exc.Int32Overflow - else z -) - -let to_int i32 = Int32.( - let i = to_int i32 in - if i32 = of_int i - then i - else raise Exc.IntOverflow -) - -let of_int = Int32.of_int diff --git a/checklink/Validator.ml b/checklink/Validator.ml deleted file mode 100644 index f9ca0edb..00000000 --- a/checklink/Validator.ml +++ /dev/null @@ -1,132 +0,0 @@ -open Check -open Disassembler -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_bytefuzz = ref false -let option_printelf = ref false - -let set_elf_file s = - begin match !elf_file with - | None -> elf_file := Some s - | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line") - end - -let set_conf_file s = - begin match !conf_file with - | None -> conf_file := Some s - | Some _ -> raise (Arg.Bad "multiple configuration files given on command line") - end - -let read_sdumps_from_channel ic = - try - while true do - let l = input_line ic in - if l <> "" then sdump_files := l :: !sdump_files - done - with End_of_file -> - () - -let read_sdumps_from_file f = - if f = "-" then - read_sdumps_from_channel stdin - else begin - try - let ic = open_in f in - read_sdumps_from_channel ic; - close_in ic - with Sys_error msg -> - Printf.eprintf "Error reading file: %s\n" msg; exit 2 - end - -let option_disassemble = ref false -let disassemble_list = ref ([]: string list) -let add_disassemble s = - disassemble_list := s :: !disassemble_list; - option_disassemble := true - -let options = [ - (* Main options *) - "-exe", Arg.String set_elf_file, - " Specify the ELF executable file to analyze"; - "-conf", Arg.String set_conf_file, - " Specify a configuration file"; - "-files-from", Arg.String read_sdumps_from_file, - " Read names of .sdump files from the given file\n\ - \t(or from standard input if is '-')"; - (* Parsing behavior *) - "-relaxed", Arg.Set ELF_parsers.relaxed, - "Allows the following behaviors in the ELF parser:\n\ -\t* Use of a fallback heuristic to resolve symbols bootstrapped at load time"; - (* Printing behavior *) - "-no-exhaustive", Arg.Clear Check.exhaustivity, - "Disable the exhaustivity check of ELF function and data symbols"; - "-list-missing", Arg.Set Check.list_missing, - "List function and data symbols that were missing in the exhaustivity check"; - (* Alternative outputs *) - "-debug", Arg.Set Check.debug, - "Print a detailed trace of verification"; - "-disass", Arg.String add_disassemble, - " Disassemble the symbol with specified name (can be repeated)"; - "-print-elf", Arg.Set option_printelf, - "Print the contents of the unanalyzed ELF executable"; - (* ELF map related *) - "-print-elfmap", Arg.Set Check.print_elfmap, - "Print a map of the analyzed ELF executable"; - "-verbose-elfmap", Arg.Set Frameworks.verbose_elfmap, - "Show sections and symbols contained in the unknown parts of the elf map"; - (* Fuzz testing related *) - "-dump-elfmap", Arg.Set Check.dump_elfmap, - "Dump an ELF map to .elfmap, for use with random fuzzing"; - "-fuzz", Arg.Set option_fuzz, - "Random fuzz testing"; - "-fuzz-byte", Arg.Set option_bytefuzz, - "Random fuzz testing byte per byte"; - "-fuzz-debug", Arg.Set Fuzz.fuzz_debug, - "Print a detailed trace of ongoing fuzz testing"; -] - -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 " ^ Version.version ^ " -Usage: cchecklink [options] <.sdump files> -In the absence of options, checks are performed and a short result is displayed. -Options are:" - -let _ = - Arg.parse options anonymous usage; - begin match !elf_file with - | None -> - Arg.usage options usage; - exit 2 - | Some elffilename -> - let sdumps = List.rev !sdump_files in - if !option_disassemble then begin - let elf = read_elf elffilename in - List.iter - (fun s -> - Printf.printf "Disassembling %s:\n%s\n\n" s (disassemble elf s) - ) - !disassemble_list - end else if !option_bytefuzz then begin - Random.self_init(); - fuzz_every_byte_loop elffilename sdumps - end else if !option_fuzz then begin - Random.self_init(); - fuzz_loop elffilename sdumps - end else if !option_printelf then begin - let elf = read_elf elffilename in - print_endline (string_of_elf elf) - end else begin - check_elf_dump elffilename sdumps - end - end diff --git a/configure b/configure index 9bbc5019..6c661db4 100755 --- a/configure +++ b/configure @@ -19,17 +19,16 @@ toolprefix='' target='' has_runtime_lib=true has_standard_headers=true -build_checklink=true advanced_debug=false usage='Usage: ./configure [options] target Supported targets: - ppc-linux (PowerPC, Linux) ppc-eabi (PowerPC, EABI with GNU/Unix tools) ppc-eabi-diab (PowerPC, EABI with Diab tools) - arm-linux (ARM, EABI) + ppc-linux (PowerPC, Linux) arm-eabi (ARM, EABI) + arm-linux (ARM, EABI) arm-eabihf (ARM, EABI using hardware FP registers) arm-hardfloat (ARM, EABI using hardware FP registers) ia32-linux (x86 32 bits, Linux) @@ -40,7 +39,7 @@ Supported targets: For PowerPC targets, the "ppc-" prefix can be refined into: ppc64- PowerPC 64 bits - e5500- FreeCell e5500 core (PowerPC 64 bits + EREF extensions) + e5500- Freescale e5500 core (PowerPC 64 bits + EREF extensions) For ARM targets, the "arm-" prefix can be refined into: armv6- ARMv6 + VFPv2 @@ -74,8 +73,6 @@ while : ; do has_runtime_lib=false;; -no-standard-headers) has_standard_headers=false;; - -no-checklink) - build_checklink=false;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -85,7 +82,6 @@ done # Per-target configuration -cchecklink=false casmruntime="" asm_supports_cfi="" struct_passing="" @@ -114,7 +110,6 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" - cchecklink=${build_checklink} advanced_debug=true;; *) system="linux" @@ -124,7 +119,6 @@ case "$target" in casmruntime="${toolprefix}gcc -c -Wa,-mregnames" clinker="${toolprefix}gcc" libmath="-lm" - cchecklink=${build_checklink} advanced_debug=true;; esac;; arm*-*) @@ -326,20 +320,6 @@ if $missingtools; then exit 2 fi -# Additional packages needed for cchecklink - -if $cchecklink; then - echo "Testing availability of ocaml-bitstring... " | tr -d '\n' - if ocamlfind query bitstring > /dev/null - then - echo "yes" - else - echo "no" - echo "ocamlfind or ocaml-bitstring missing, cchecklink will not be built" - cchecklink=false - fi -fi - # Generate Makefile.config sharedir="$(dirname "$bindir")"/share @@ -369,7 +349,6 @@ CLINKER=$clinker LIBMATH=$libmath HAS_RUNTIME_LIB=$has_runtime_lib HAS_STANDARD_HEADERS=$has_standard_headers -CCHECKLINK=$cchecklink ASM_SUPPORTS_CFI=$asm_supports_cfi ADVANCED_DEBUG=$advanced_debug EOF @@ -383,7 +362,9 @@ cat >> Makefile.config <<'EOF' ARCH= # Hardware variant -# MODEL=standard # for PowerPC +# MODEL=ppc32 # for plain PowerPC +# MODEL=ppc64 # for PowerPC with 64-bit instructions +# MODEL=e5500 # for Freescale e5500 PowerPC variant # MODEL=armv6 # for ARM # MODEL=armv7a # for ARM # MODEL=armv7r # for ARM @@ -488,7 +469,6 @@ CompCert configuration: Library files installed in.... $libdirexp Standard headers provided..... $has_standard_headers Standard headers installed in. $libdirexp/include - cchecklink tool supported..... $cchecklink Build command to use.......... $make If anything above looks wrong, please edit file ./Makefile.config to correct. -- cgit