Source file `generic_decoder_sig.ml`

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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(**************************************************************************)
(*  This file is part of BINSEC.                                          *)
(*                                                                        *)
(*  Copyright (C) 2016-2026                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

module type Monad = sig
  type 'a m

  val return : 'a -> 'a m
  val bind : 'a m -> ('a -> 'b m) -> 'b m
end

module Monadic_Arity (M : Monad) = struct
  type 'a m = 'a M.m
  type 'r ar0 = 'r m
  type ('a, 'r) ar1 = 'a -> 'r m
  type ('a, 'b, 'r) ar2 = 'a -> 'b -> 'r m
  type ('a, 'b, 'c, 'r) ar3 = 'a -> 'b -> 'c -> 'r m
  type ('a, 'r) variadic = 'a list -> 'r m
end

module type Expr_Input = sig
  module M : Monad

  type boolean
  type binary

  module Binary : sig
    include
      Transfer_functions.Binary_Forward
        with module Arity := Monadic_Arity(M)
         and type binary = binary
         and type boolean = boolean
  end

  module Boolean : sig
    include
      Transfer_functions.Boolean_Forward
        with module Arity := Monadic_Arity(M)
         and type boolean = boolean
  end

  val bin_of_bool : boolean -> binary M.m
  val bool_of_bin : binary -> boolean M.m

  (* If(cond) then a else b operation. *)
  val ite : boolean -> binary -> binary -> binary M.m
  val get_var : size:int -> string -> binary M.m
  val load : size:int -> Machine.endianness -> binary -> binary M.m
  val assume : boolean -> unit M.m
end

module State_Monad (State : sig
  type t
end) : Monad with type 'a m = State.t -> 'a * State.t = struct
  type 'a m = State.t -> 'a * State.t

  let return x state = (x, state)

  let bind a f state1 =
    let x, state2 = a state1 in
    (f x) state2
end

module type Instr_Input = sig
  module State : sig
    type t
  end

  include Expr_Input with module M := State_Monad(State)

  val unknown : size:int -> binary State_Monad(State).m
  val undef : size:int -> binary State_Monad(State).m

  (* Note: could return a unit State_Monad(State).m instead, but this
     is more convenient. *)
  val store :
    size:int -> Machine.endianness -> binary -> binary -> State.t -> State.t

  val set_var : size:int -> string -> binary -> State.t -> State.t

  (* Add a comment "at the current position". In LLVM for instance, it
     corresponds to a metadata attached to the next instruction which
     is translated. *)
  val add_comment : string -> State.t -> State.t
end

type 'bin jump_target = Static of Dba.id Dba.jump_target | Dynamic of 'bin

type ('bool, 'bin) jump_kind =
  | JKIf of 'bool * 'bin jump_target * 'bin jump_target
  | JKJump of 'bin jump_target
  | JKStop
  | JKAssume of 'bool * 'bin jump_target