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
module Backend = struct
type address = Int32.t
module Map = Map.Make (struct
include Int32
(* TODO: define this in Int32 directly? *)
let compare i1 i2 = compare (Int32.to_int i1) (Int32.to_int i2)
end)
type t =
{ mutable data : Symbolic_value.int32 Map.t
; mutable chunks : Symbolic_value.int32 Map.t
}
let make () = { data = Map.empty; chunks = Map.empty }
let clone { data; chunks } =
(* Caution, it is tempting not to rebuild the record here, but...
it must be! otherwise the mutable data points to the same location *)
{ data; chunks }
let address a =
let open Symbolic_choice_without_memory in
match Smtml.Expr.view a with
| Val (Bitv bv) when Smtml.Bitvector.numbits bv <= 32 ->
return (Smtml.Bitvector.to_int32 bv)
| Ptr { base; offset } ->
select_i32 Symbolic_value.(I32.add (const_i32 base) offset)
| _ -> select_i32 a
let address_i32 a = a
let load_byte a { data; _ } =
match Map.find_opt a data with
| None -> Smtml.Expr.value (Bitv (Smtml.Bitvector.of_int8 0))
| Some v -> v
let loadn m a n =
let rec loop addr size i acc =
if i = size then acc
else
let addr' = Int32.(add addr (of_int i)) in
let byte = load_byte addr' m in
loop addr size (i + 1) (Smtml.Expr.concat byte acc)
in
let v0 = load_byte a m in
loop a n 1 v0
let replace m k v = m.data <- Map.add k v m.data
let storen m a v n =
for i = 0 to n - 1 do
let a' = Int32.add a (Int32.of_int i) in
let v' = Smtml.Expr.extract v ~low:i ~high:(i + 1) in
replace m a' v'
done
let validate_address m a range =
let open Symbolic_choice_without_memory in
match Smtml.Expr.view a with
| Val (Bitv _) ->
(* An i32 is not a pointer to a heap chunk, so its valid *)
return (Ok a)
| Ptr { base; offset = start_offset } -> (
let open Symbolic_value in
match Map.find_opt base m.chunks with
| None -> return (Error `Memory_leak_use_after_free)
| Some chunk_size ->
let+ is_out_of_bounds =
let range = const_i32 (Int32.of_int (range - 1)) in
(* end_offset: last byte we will read/write *)
let end_offset = I32.add start_offset range in
select
(Bool.or_
(I32.ge_u start_offset chunk_size)
(I32.ge_u end_offset chunk_size) )
in
if is_out_of_bounds then Error `Memory_heap_buffer_overflow else Ok a )
| _ ->
(* A symbolic expression is valid, but we print to check if Ptr's are passing through here *)
Logs.warn (fun m -> m "Saw a symbolic address: %a" Smtml.Expr.pp a);
return (Ok a)
let ptr v =
let open Symbolic_choice_without_memory in
match Smtml.Expr.view v with
| Ptr { base; _ } -> return base
| _ ->
Logs.err (fun m ->
m {|free: cannot fetch pointer base of "%a"|} Smtml.Expr.pp v );
assert false
let free m p =
let open Symbolic_choice_without_memory in
match Smtml.Expr.view p with
| Val (Bitv bv) when Smtml.Bitvector.eqz bv ->
return (Symbolic_value.const_i32 0l)
| _ ->
let* base = ptr p in
if not @@ Map.mem base m.chunks then trap `Double_free
else begin
let chunks = Map.remove base m.chunks in
m.chunks <- chunks;
return (Symbolic_value.const_i32 base)
end
let realloc m ~ptr ~size =
let open Symbolic_choice_without_memory in
let+ base = address ptr in
let chunks = Map.add base size m.chunks in
m.chunks <- chunks;
Smtml.Expr.ptr base (Symbolic_value.const_i32 0l)
end
include Symbolic_memory_make.Make (Backend)