1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(** Basic arch definitions made abstract *)
module type S = sig
(* Who am I ? *)
val arch : Archs.t
val base_type : CType.t
(***********************************************)
(* Basic arch types and their basic operations *)
(***********************************************)
type reg
val parse_reg : string -> reg option
val pp_reg : reg -> string
val reg_compare : reg -> reg -> int
val symb_reg_name : reg -> string option
val symb_reg : string -> reg
val type_reg : reg -> CType.t
type barrier
val pp_barrier : barrier -> string
val barrier_compare : barrier -> barrier -> int
type parsedInstruction
type instruction
val pp_instruction : PPMode.t -> instruction -> string
(* Shorthand for parsable dump *)
val dump_instruction : instruction -> string
(* Shorthand used for hash computation *)
val dump_instruction_hash : instruction -> string
(*************************************)
(* All this needed for symbolic regs *)
(*************************************)
(* Registers that can be allocated to symbolic registers *)
val allowed_for_symb : reg list
(* Apply fonctions to all registers either real or symbolic *)
val fold_regs :
(reg -> 'a -> 'a) * (string -> 'b -> 'b) ->
'a * 'b -> instruction -> 'a * 'b
(* Map over all registers *)
val map_regs :
(reg -> reg) -> (string -> reg) -> instruction -> instruction
(* Apply function to addresses present in code *)
val fold_addrs : (ParsedConstant.v -> 'a -> 'a) -> 'a -> instruction -> 'a
(* Map over addresses *)
val map_addrs :
(ParsedConstant.v -> ParsedConstant.v) -> instruction -> instruction
(* Normalize instruction (for hashes) *)
val norm_ins : instruction -> instruction
(* Check validity of instructions, beyond parsing *)
val is_valid : instruction -> bool
include Pseudo.S
with type ins = instruction
and type pins = parsedInstruction
and type reg_arg = reg
val get_macro :
string ->
(reg list -> pseudo list -> pseudo list)
(* For digest, include normalised prininting of pteval's *)
val hash_pteval : ParsedPteVal.t -> string
end
|
