@@ -19,18 +19,14 @@ let bool = Theory.Bool.t
1919
2020let reg t n = Theory.Var. define t n
2121
22- let array t fmt size =
22+ let array ?( from = 0 ) t fmt size =
2323 let fmt = Scanf. format_from_string fmt " %d" in
24- List. init size ~f: (fun i -> reg t (sprintf fmt i ))
24+ List. init size ~f: (fun i -> reg t (sprintf fmt (i + from) ))
2525
2626let untyped = List. map ~f: Theory.Var. forget
2727let (@<) xs ys = untyped xs @ untyped ys
2828
29- let name size order =
30- let order = Theory.Endianness. name order in
31- sprintf " powerpc%d+%s" size (KB.Name. unqualified order)
32-
33- let parent = Theory.Target. declare ~package " powerpc"
29+ let parent = Theory.Target. declare ~package " powerpc-family"
3430
3531let crflags =
3632 List. concat @@ List. init 8 ~f: (fun group ->
@@ -43,7 +39,7 @@ let flags = List.map ~f:(reg bool) [
4339 " C" ; " FL" ; " FE" ; " FG" ; " FU"
4440 ] @ crflags
4541
46- let define ?(parent =parent) ?nicknames bits endianness =
42+ let define ?(parent =parent) ?nicknames name bits endianness =
4743 let size = Theory.Bitv. size bits in
4844 let mems = Theory.Mem. define bits r8 in
4945 let data = Theory.Var. define mems " mem" in
@@ -53,7 +49,7 @@ let define ?(parent=parent) ?nicknames bits endianness =
5349 flags @<
5450 [reg bits " CTR" ; reg bits " LR" ; reg bits " TAR" ] @<
5551 [data] in
56- Theory.Target. declare ~package ( name size endianness)
52+ Theory.Target. declare ~package name
5753 ~parent
5854 ?nicknames
5955 ~bits: size
@@ -74,36 +70,48 @@ let define ?(parent=parent) ?nicknames bits endianness =
7470 [carry_flag], untyped@@ [reg bool " CA" ; reg bool " CA32" ];
7571 [overflow_flag], untyped@@ List. ([" SO" ; " OV" ; " OV32" ] >> | reg bool );
7672 [status; floating], untyped@@ List. ([" FL" ; " FE" ; " FG" ; " FU" ] >> | reg bool );
73+ [caller_saved], untyped [reg bits " R0" ] @
74+ untyped (array bits ~from: 3 " R%d" 10 ) @
75+ untyped (array r64 " F%d" 14 );
76+ [callee_saved], untyped [reg bits " R1" ] @
77+ untyped (array bits ~from: 14 " R%d" 18 ) @
78+ untyped (array r64 ~from: 14 " F%d" 18 );
79+ [function_argument; integer], untyped (array bits ~from: 3 " R%d" 8 );
80+ [function_argument; floating], untyped (array bits ~from: 1 " F%d" 8 );
81+ [function_return; integer], untyped [reg bits " R3" ; reg bits " R4" ];
82+ [function_return; floating], untyped [reg r64 " F0" ];
83+ [reserved], untyped@@ [reg bits " R2" ];
7784 ]
7885
79- let powerpc32bi = define r32 Theory.Endianness. bi
80- ~nicknames: [" powerpc32bi" ; " ppc32bi" ]
86+ let powerpc32bi = define " powerpcbi " r32 Theory.Endianness. bi
87+ ~nicknames: [" powerpc32bi" ; " ppc32bi" ; " powerpc32+bi " ]
8188
82- let powerpc32eb = define r32 Theory.Endianness. eb
89+ let powerpc32eb = define " powerpc " r32 Theory.Endianness. eb
8390 ~nicknames: [
84- " powerpc " ; " ppc" ; " powerpc32" ; " ppc32" ;
91+ " powerpc32+eb " ; " ppc" ; " powerpc32" ; " ppc32" ;
8592 " powerpc32eb" ; " powerpc32be" ; " ppc32eb" ; " ppc32be" ;
8693 " power" ; " power32" ;
8794 ]
88- let powerpc32le = define r32 Theory.Endianness. le
95+ let powerpc32le = define " powerpcle " r32 Theory.Endianness. le
8996 ~nicknames: [
90- " powerpcle " ; " ppcle" ; " ppcel" ;
97+ " powerpc32+le " ; " ppcle" ; " ppcel" ;
9198 " powerpc32le" ; " powerpc32el" ;
9299 " ppc32le" ; " ppc32el"
93100 ]
94101
95- let powerpc64bi = define r64 Theory.Endianness. bi
96- ~nicknames: [" powerpc64bi" ; " power64bi" ]
97- let powerpc64eb = define r64 Theory.Endianness. eb
102+ let powerpc64bi = define " powerpc64bi" r64 Theory.Endianness. bi
103+ ~nicknames: [" powerpc64+bi" ; " power64bi" ]
104+
105+ let powerpc64eb = define " powerpc64" r64 Theory.Endianness. eb
98106 ~nicknames: [
99- " powerpc64" ; " ppc64" ; " power64" ;
107+ " powerpc64+bi " ; " ppc64" ; " power64" ;
100108 " powerpc64eb" ; " powerpc64be" ;
101109 " ppc64eb" ; " ppc64be" ;
102110 " power64eb" ; " power64be"
103111 ]
104- let powerpc64le = define r64 Theory.Endianness. le
112+ let powerpc64le = define " powerpc64le " r64 Theory.Endianness. le
105113 ~nicknames: [
106- " powerpc64el" ; " powerpc64le " ;
114+ " powerpc64el" ; " powerpc64+le " ;
107115 " ppc64el" ; " ppc64le" ;
108116 " power64el" ; " power64le"
109117 ]
@@ -115,35 +123,47 @@ let enable_loader () =
115123 let request =
116124 Ogre. request Image.Scheme. arch >> = fun arch ->
117125 Ogre. request Image.Scheme. is_little_endian >> = fun little ->
118- Ogre. return (arch,little) in
126+ Ogre. request Image.Scheme. format >> = fun format ->
127+ Ogre. return (arch,little,format) in
119128 match Ogre. eval request doc with
120- | Error _ -> None ,None
129+ | Error _ -> None ,None , None
121130 | Ok info -> info in
122131 KB. promise Theory.Unit. target @@ fun unit ->
123- KB. collect Image.Spec. slot unit >> |
124- request_info >> | function
125- | Some "powerpc" , None -> powerpc32bi
126- | Some "powerpc64" ,None -> powerpc64bi
127- | Some "powerpc" ,Some true -> powerpc32le
128- | Some "powerpc64" ,Some true -> powerpc64le
129- | Some "powerpc" ,Some false -> powerpc32eb
130- | Some "powerpc64" ,Some false -> powerpc64eb
131- | _ -> Theory.Target. unknown
132-
133-
134- let mapped_powerpc = Map. of_alist_exn (module Theory. Target ) [
135- powerpc32eb, `ppc ;
136- powerpc64eb, `ppc64 ;
137- powerpc64le, `ppc64le ;
138- ]
132+ KB. collect Image.Spec. slot unit >> | request_info >> | fun (arch ,is_little ,format ) ->
133+ let (abi,filetype) = match format with
134+ | Some "elf" -> Theory.Abi. gnu, Theory.Filetype. elf
135+ | Some "macho" -> Theory.Abi. gnu, Theory.Filetype. macho
136+ | _ -> Theory.Abi. unknown, Theory.Filetype. unknown in
137+ let parent = match arch, is_little with
138+ | Some "powerpc" , (None |Some false ) -> powerpc32eb
139+ | Some "powerpc64" ,(None |Some false ) -> powerpc64eb
140+ | Some "powerpc" ,Some true -> powerpc32le
141+ | Some "powerpc64" ,Some true -> powerpc64le
142+ | _ -> Theory.Target. unknown in
143+ if Theory.Target. is_unknown parent then parent
144+ else Theory.Target. select ~strict: true ~parent ~filetype ~abi ()
145+
146+
147+ let register_subtargets () =
148+ [powerpc32eb; powerpc32le; powerpc64eb; powerpc64le] |>
149+ List. iter ~f: (fun parent ->
150+ Theory.Target. register parent
151+ ~abis: Theory.Abi. [unknown; gnu]
152+ ~systems: Theory.System. [unknown; linux; freebsd; openbsd; vxworks]
153+ ~filetypes: Theory.Filetype. [unknown; elf; macho])
154+
139155
140156let map_powerpc () =
141157 let open KB.Syntax in
142158 KB. promise Arch. unit_slot @@ fun unit ->
143- KB. collect Theory.Unit. target unit >> |
144- Map. find mapped_powerpc >> | function
145- | Some arch -> arch
146- | None -> `unknown
159+ KB. collect Theory.Unit. target unit >> | fun t ->
160+ if Theory.Target. belongs parent t then
161+ match Theory.Target. bits t, Theory.Endianness. (Theory.Target. endianness t = le) with
162+ | 32 ,false -> `ppc
163+ | 64 ,false -> `ppc64
164+ | 64 ,true -> `ppc64le
165+ | _ -> `unknown
166+ else `unknown
147167
148168module Dis = Disasm_expert. Basic
149169
@@ -186,6 +206,7 @@ let enable_pcode_decoder () =
186206 end
187207
188208let load ?(backend =" llvm" ) () =
209+ register_subtargets () ;
189210 enable_loader () ;
190211 map_powerpc () ;
191212 match backend with
0 commit comments