package binsec
Semantic analysis of binary executables
Install
Dune Dependency
Authors
-
AAdel Djoudi
-
BBenjamin Farinier
-
CChakib Foulani
-
DDorian Lesbre
-
FFrédéric Recoules
-
GGuillaume Girol
-
JJosselin Feist
-
LLesly-Ann Daniel
-
MMahmudul Faisal Al Ameen
-
MManh-Dung Nguyen
-
MMathéo Vergnolle
-
MMathilde Ollivier
-
MMatthieu Lemerre
-
NNicolas Bellec
-
OOlivier Nicole
-
RRichard Bonichon
-
RRobin David
-
SSébastien Bardin
-
SSoline Ducousso
-
TTa Thanh Dinh
-
YYaëlle Vinçont
-
YYanis Sellami
Maintainers
Sources
binsec-0.10.1.tbz
sha256=87d4048c9a90c8a14ee029e77d31032a15427f06416a31938cec8a68394234c4
sha512=6a023d2a5c87c56b0aac489874431d8dcccee1451a072a826190be3a7f75a961688bab95f193f494231744abc3bc9733ab5c809057d36a5e4d24c6c29c369144
doc/src/libterm/ai.ml.html
Source file ai.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
(**************************************************************************) (* This file is part of BINSEC. *) (* *) (* Copyright (C) 2016-2025 *) (* 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 Sexpr module type CONTEXT = sig type t (** context *) type v (** domain abstract value *) val add_dependency : t -> parent:Expr.t -> Expr.t -> unit val find_dependency : t -> Expr.t -> BvSet.t val add : t -> Expr.t -> v -> unit val find : t -> Expr.t -> v end module type S = sig type t type v val eval : t -> Expr.t -> v val refine : t -> Expr.t -> v -> unit end module Make (D : Domains.S) (C : CONTEXT with type v := D.t) : S with type t = C.t and type v := D.t = struct type t = C.t open D let unary (f : Term.unary Term.operator) ~size x = match f with | Not -> lognot ~size x | Minus -> uminus ~size x | Sext n -> sext n ~size x | Uext n -> uext n ~size x | Restrict { hi; lo } -> restrict ~hi ~lo ~size x let binary (f : Term.binary Term.operator) = match f with | Plus -> add | Minus -> sub | Mul -> mul | Udiv -> udiv | Umod -> umod | Sdiv -> sdiv | Smod -> smod | Or -> logor | And -> logand | Xor -> logxor | Eq -> equal | Diff -> diff | Ule -> ule | Ult -> ult | Uge -> uge | Ugt -> ugt | Sle -> sle | Slt -> slt | Sge -> sge | Sgt -> sgt | Lsl -> shift_left | Lsr -> shift_right | Asr -> shift_right_signed | Rol -> rotate_left | Ror -> rotate_right | Concat -> assert false let rec eval ctx (e : Expr.t) = try C.find ctx e with Not_found -> let d = match e with | Cst bv -> constant ~size:(Bitvector.size_of bv) (Bitvector.value_of bv) | Var { size; _ } -> top size | Load { len; _ } -> top (len lsl 3) | Unary { f; x; _ } -> C.add_dependency ctx x ~parent:e; unary f ~size:(Expr.sizeof x) (eval ctx x) | Binary { f = Concat; x; y; _ } -> C.add_dependency ctx x ~parent:e; C.add_dependency ctx y ~parent:e; append ~size1:(Expr.sizeof x) (eval ctx x) ~size2:(Expr.sizeof y) (eval ctx y) | Binary { f; x; y; _ } -> C.add_dependency ctx x ~parent:e; C.add_dependency ctx y ~parent:e; (binary f) ~size:(Expr.sizeof x) (eval ctx x) (eval ctx y) | Ite { c; t; e = r; _ } -> ( C.add_dependency ctx c ~parent:e; C.add_dependency ctx t ~parent:e; C.add_dependency ctx r ~parent:e; let c' = eval ctx c in match is_zero c' with | False -> eval ctx t | True -> eval ctx r | Unknown -> union ~size:(Expr.sizeof t) (eval ctx t) (eval ctx r)) in C.add ctx e d; d let unary_feedback (f : Term.unary Term.operator) x d = match f with | Not -> lognot_feedback x d | Minus -> uminus_feedback x d | Sext n -> sext_feedback n x d | Uext n -> uext_feedback n x d | Restrict { hi; lo } -> restrict_feedback ~hi ~lo x d let binary_feedback (f : Term.binary Term.operator) = match f with | Plus -> add_feedback | Minus -> sub_feedback | Mul -> mul_feedback | Udiv -> udiv_feedback | Umod -> umod_feedback | Sdiv -> sdiv_feedback | Smod -> smod_feedback | Or -> logor_feedback | And -> logand_feedback | Xor -> logxor_feedback | Eq -> equal_feedback | Diff -> diff_feedback | Ule -> ule_feedback | Ult -> ult_feedback | Uge -> uge_feedback | Ugt -> ugt_feedback | Sle -> sle_feedback | Slt -> slt_feedback | Sge -> sge_feedback | Sgt -> sgt_feedback | Lsl -> shift_left_feedback | Lsr -> shift_right_feedback | Asr -> shift_right_signed_feedback | Rol -> rotate_left_feedback | Ror -> rotate_right_feedback | Concat -> assert false let refine = let rec loop_up todo ctx locked = if BvSet.is_empty todo then () else let e = BvSet.choose todo in let todo = BvSet.remove e todo in if BvSet.mem e locked then loop_up todo ctx locked else (* let locked = BvSet.add e locked in *) let o = C.find ctx e in let n = match e with | Cst _ | Var _ | Load _ -> assert false | Unary { f; x; _ } -> unary f ~size:(Expr.sizeof x) (C.find ctx x) | Binary { f = Concat; x; y; _ } -> append ~size1:(Expr.sizeof x) (C.find ctx x) ~size2:(Expr.sizeof y) (C.find ctx y) | Binary { f; x; y; _ } -> binary f ~size:(Expr.sizeof x) (C.find ctx x) (C.find ctx y) | Ite { c; t; e = r; _ } -> ( let c' = C.find ctx c in match is_zero c' with | False -> C.find ctx t | True -> C.find ctx r | Unknown -> union ~size:(Expr.sizeof t) (C.find ctx t) (C.find ctx r)) in if included ~size:(Expr.sizeof e) o n then loop_up todo ctx locked else let todo = try BvSet.union (C.find_dependency ctx e) todo with Not_found -> todo in C.add ctx e n; loop_up todo ctx locked in let rec loop_down todo ctx dirty locked = if Queue.is_empty todo then loop_up dirty ctx locked else let (e : Expr.t), (d : t) = Queue.pop todo in let size = Expr.sizeof e in let o = C.find ctx e in if included ~size o d then loop_down todo ctx dirty locked else let n = inter ~size o d in let locked = BvSet.add e locked in C.add ctx e n; let dirty = try BvSet.union (C.find_dependency ctx e) dirty with Not_found -> dirty in (match e with | Cst _ | Var _ | Load _ -> () | Unary { f; x; _ } -> let x' = unary_feedback f ~size:(Expr.sizeof x) (C.find ctx x) n in Queue.add (x, x') todo | Binary { f = Concat; x; y; _ } -> let x', y' = append_feedback ~size1:(Expr.sizeof x) (C.find ctx x) ~size2:(Expr.sizeof y) (C.find ctx y) n in Queue.add (x, x') todo; Queue.add (y, y') todo | Binary { f; x; y; _ } -> let x', y' = (binary_feedback f) ~size:(Expr.sizeof x) (C.find ctx x) (C.find ctx y) n in Queue.add (x, x') todo; Queue.add (y, y') todo | Ite { c; t; e; _ } -> let c' = C.find ctx c in if included ~size:1 c' one then Queue.add (t, n) todo else if included ~size:1 c' zero then Queue.add (e, n) todo else if disjoint ~size (C.find ctx t) n then Queue.add (c, zero) todo else if disjoint ~size (C.find ctx e) n then Queue.add (c, one) todo); loop_down todo ctx dirty locked in fun ctx e d -> let todo = Queue.create () in Queue.add (e, d) todo; loop_down todo ctx BvSet.empty BvSet.empty end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>