package binsec

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file script.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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
(**************************************************************************)
(*  This file is part of BINSEC.                                          *)
(*                                                                        *)
(*  Copyright (C) 2016-2023                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

open Types

module Expr = struct
  include Dba.Expr

  let neg = uminus

  let succ e = add e (constant (Bitvector.create Z.one (size_of e)))
end

module Pexpr : Ast_types.PARSER_EXPRESSION with type expr := Expr.t = struct
  type t = Int of Z.t | Expr of Expr.t

  let int_to_expr n i =
    if Z.numbits i > n then
      Options.Logger.fatal "integer %a does not fit in %a" Z.pp_print i
        (fun ppf n ->
          if n = 1 then Format.pp_print_string ppf "bool"
          else Format.fprintf ppf "bitvector of %d bits" n)
        n
    else Expr.constant (Bitvector.create i n)

  let to_expr n x =
    match x with
    | Int i -> int_to_expr n i
    | Expr e ->
        if Expr.size_of e <> n then
          Options.Logger.fatal "%a was expected to be a bitvector of %d bit%s"
            Dba_printer.Ascii.pp_bl_term e n
            (if n = 1 then "" else "s")
        else e

  let to_bool = to_expr 1

  let unary (o : Dba.Unary_op.t) x =
    match x with
    | Int _ ->
        Options.Logger.fatal "unable to apply %a operator on an integer"
          Dba_printer.Ascii.pp_unary_op o
    | Expr e -> Expr (Expr.unary o e)

  let binary (o : Dba.Binary_op.t) x y =
    match (x, y) with
    | Int _, Int _ ->
        Options.Logger.fatal "unable to apply %a operator on two integers"
          Dba_printer.Ascii.pp_binary_op o
    | Int i, Expr e -> Expr Expr.(binary o (int_to_expr (size_of e) i) e)
    | Expr e, Int i -> Expr Expr.(binary o e (int_to_expr (size_of e) i))
    | Expr e, Expr e' -> Expr (Expr.binary o e e')

  let add = binary Plus

  let sub = binary Minus

  let mul = binary Mult

  let neg = unary UMinus

  let udiv = binary DivU

  let umod = binary ModU

  let urem = binary ModU

  let sdiv = binary DivS

  let smod = binary ModS

  let srem = binary ModS

  let equal = binary Eq

  let diff = binary Diff

  let ule = binary LeqU

  let uge = binary GeqU

  let ult = binary LtU

  let ugt = binary GtU

  let sle = binary LeqS

  let sge = binary GeqS

  let slt = binary LtS

  let sgt = binary GtS

  let logand = binary And

  let logor = binary Or

  let lognot = unary Not

  let logxor = binary Xor

  let shift_left = binary LShift

  let shift_right = binary RShiftU

  let shift_right_signed = binary RShiftS

  let rotate_left = binary LeftRotate

  let rotate_right = binary RightRotate

  let sext n x = unary (Sext n) x

  let uext n x = unary (Uext n) x

  let restrict lo hi x =
    match x with
    | Int i ->
        let n = hi - lo + 1 in
        Expr (Expr.constant (Bitvector.create (Z.extract i lo n) n))
    | Expr e -> Expr (Expr.restrict lo hi e)

  let append x y =
    match (x, y) with
    | Int _, _ | _, Int _ ->
        Options.Logger.fatal "unable to concatenate integer without size"
    | Expr a, Expr b -> Expr (Expr.append a b)

  let ite c x y =
    let t, e =
      match (x, y) with
      | Int _, Int _ ->
          Options.Logger.fatal "unable to infer the size of ite body"
      | Int i, Expr e -> (int_to_expr (Expr.size_of e) i, e)
      | Expr e, Int i -> (e, int_to_expr (Expr.size_of e) i)
      | Expr e, Expr e' -> (e, e')
    in
    Expr (Expr.ite c t e)
end

module LValue = Dba.LValue

module Instr = struct
  type t =
    | Assign of LValue.t * Expr.t
    | Undef of LValue.t
    | Nondet of LValue.t
    | Assume of Expr.t
    | Assert of Expr.t
    | It of Expr.t * string
    | Goto of string
    | Jump of Expr.t
    | Label of string
    | Halt

  let assign loc value = Assign (loc, value)

  let undef loc = Undef loc

  let nondet loc = Nondet loc

  let assume test = Assume test

  let dynamic_assert test = Assert test

  let conditional_jump test target = It (test, target)

  let goto target = Goto target

  let dynamic_jump target = Jump target

  let label name = Label name

  let halt = Halt

  let pp_list ppf hunk =
    Format.pp_open_vbox ppf 0;
    Format.pp_open_vbox ppf 2;
    List.iter
      (fun instr ->
        match instr with
        | Assign (lval, rval) ->
            Format.fprintf ppf "@ @[<hov>%a := %a@]" Dba_printer.Ascii.pp_lhs
              lval Dba_printer.Ascii.pp_bl_term rval
        | Undef lval ->
            Format.fprintf ppf "@ @[<hov>%a := \\undef@]"
              Dba_printer.Ascii.pp_lhs lval
        | Nondet lval ->
            Format.fprintf ppf "@ @[<hov>%a := \\nondet@]"
              Dba_printer.Ascii.pp_lhs lval
        | Assume test ->
            Format.fprintf ppf "@ @[<hov>assume %a@]"
              Dba_printer.Ascii.pp_bl_term test
        | Assert test ->
            Format.fprintf ppf "@ @[<hov>assert %a]"
              Dba_printer.Ascii.pp_bl_term test
        | It (test, target) ->
            Format.fprintf ppf "@ @[<hov>if %a@ goto %s@]"
              Dba_printer.Ascii.pp_bl_term test target
        | Goto target -> Format.fprintf ppf "@ goto %s" target
        | Jump target ->
            Format.fprintf ppf "@ @[<hov>jump %a@]" Dba_printer.Ascii.pp_bl_term
              target
        | Label name -> Format.fprintf ppf "@]@ @[<v 2>%s:" name
        | Halt -> Format.fprintf ppf "@ halt")
      hunk;
    Format.pp_close_box ppf ();
    Format.pp_close_box ppf ()
end

module Directive = struct
  type t =
    | Cut of Expr.t option
    | Assume of Expr.t
    | Assert of Expr.t
    | Reach of int * Expr.t option * Output.t list
    | Enumerate of int * Expr.t
end

type t =
  | Start_from of Expr.t * Instr.t list
  | Start_from_core of Instr.t list
  | Load_sections of string list
  | Load_data of Expr.t
  | Import_symbols of (string * Dba.Var.Tag.attribute) list * string
  | Stub of Expr.t list * Instr.t list
  | Init of Instr.t list
  | Directive of Expr.t * Directive.t
OCaml

Innovation. Community. Security.