aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-10-12 11:48:36 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-10-12 11:48:36 +0200
commit3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267 (patch)
tree41afaa730849b6f9e8116ddc3068044928997d8c
parentef0f69dc1caeab169dcefca4d8b89f4d9e756bb5 (diff)
downloadcompcert-kvx-3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267.tar.gz
compcert-kvx-3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267.zip
Removal of cchecklink, superseded by AbsInt's Valex tool.
-rw-r--r--.gitignore2
-rw-r--r--Makefile.extr56
-rw-r--r--checklink/Asm_printers.ml321
-rw-r--r--checklink/Bitstring_utils.ml33
-rw-r--r--checklink/Check.ml3216
-rw-r--r--checklink/Disassembler.ml15
-rw-r--r--checklink/ELF_parsers.ml362
-rw-r--r--checklink/ELF_printers.ml206
-rw-r--r--checklink/ELF_types.ml170
-rw-r--r--checklink/ELF_utils.ml128
-rw-r--r--checklink/Exc.ml2
-rw-r--r--checklink/Frameworks.ml214
-rw-r--r--checklink/Fuzz.ml175
-rw-r--r--checklink/Lens.ml32
-rw-r--r--checklink/Library.ml171
-rw-r--r--checklink/Makefile52
-rw-r--r--checklink/PPC_parsers.ml397
-rw-r--r--checklink/PPC_printers.ml203
-rw-r--r--checklink/PPC_types.ml198
-rw-r--r--checklink/PPC_utils.ml26
-rw-r--r--checklink/Safe.ml25
-rw-r--r--checklink/Safe32.ml34
-rw-r--r--checklink/Validator.ml132
-rwxr-xr-xconfigure32
24 files changed, 9 insertions, 6193 deletions
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,
- "<filename> Specify the ELF executable file to analyze";
- "-conf", Arg.String set_conf_file,
- "<filename> Specify a configuration file";
- "-files-from", Arg.String read_sdumps_from_file,
- "<filename> Read names of .sdump files from the given file\n\
- \t(or from standard input if <filename> 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,
- "<symname> 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 <exename>.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> <ELF executable>
-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.