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