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
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)
module Expr = Smtml.Expr
(* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *)
module M :
Wasm_ffi_intf.S0
with type 'a t = 'a Concolic_choice.t
and type memory = Concolic_memory.t
and module Value = Concolic_value = struct
type 'a t = 'a Concolic_choice.t
type memory = Concolic_memory.t
module Value = Concolic_value
let symbol_i32 () : Value.int32 Concolic_choice.t =
Concolic_choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value ->
let n =
match forced_value with
| None -> Random.bits32 ()
| Some (Num (I32 n)) -> n
| _ -> assert false
in
(I32 n, (n, Expr.symbol sym)) )
let symbol_i8 () : Value.int32 Concolic_choice.t =
Concolic_choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value ->
let n =
match forced_value with
| None -> Int32.logand 0xFFl (Random.bits32 ())
| Some (Num (I32 n)) -> n
| _ -> assert false
in
let sym_expr =
Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym))
in
(I32 n, (n, sym_expr)) )
let symbol_char () : Value.int32 Concolic_choice.t =
Concolic_choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value ->
let n =
match forced_value with
| None -> Int32.logand 0xFFl (Random.bits32 ())
| Some (Num (I32 n)) -> n
| _ -> assert false
in
let sym_expr =
Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym))
in
(I32 n, (n, sym_expr)) )
let symbol_i64 () : Value.int64 Concolic_choice.t =
Concolic_choice.with_new_symbol (Ty_bitv 64) (fun sym forced_value ->
let n =
match forced_value with
| None -> Random.bits64 ()
| Some (Num (I64 n)) -> n
| _ -> assert false
in
(I64 n, (n, Expr.symbol sym)) )
let symbol_f32 () : Value.float32 Concolic_choice.t =
Concolic_choice.with_new_symbol (Ty_fp 32) (fun sym forced_value ->
let n =
match forced_value with
| None -> Random.bits32 ()
| Some (Num (F32 n)) -> n
| _ -> assert false
in
let n = Float32.of_bits n in
(F32 n, (n, Expr.symbol sym)) )
let symbol_f64 () : Value.float64 Concolic_choice.t =
Concolic_choice.with_new_symbol (Ty_fp 64) (fun sym forced_value ->
let n =
match forced_value with
| None -> Random.bits64 ()
| Some (Num (F64 n)) -> n
| _ -> assert false
in
let n = Float64.of_bits n in
(F64 n, (n, Expr.symbol sym)) )
let assume (i : Value.int32) : unit Concolic_choice.t =
let c = Value.I32.to_bool i in
Concolic_choice.assume c
let assert' (i : Value.int32) : unit Concolic_choice.t =
let c = Value.I32.to_bool i in
Concolic_choice.assertion c
open Expr
let abort () : unit Concolic_choice.t = Concolic_choice.abort
let i32 ((_c, s) : Value.int32) : int32 Concolic_choice.t =
(* TODO: select_i32 ? *)
(* let+ v = Concolic_choice.select_i32 v in *)
(* let n = v.c in *)
(* let x = Concolic_choice.assume (Value.I32.eq v (Value.const_i32 n)) in *)
match view s with
| Val (Num (I32 v)) -> Concolic_choice.return v
| _ ->
Log.debug2 {|alloc: cannot allocate base pointer "%a"@.|} Expr.pp s;
Concolic_choice.bind (abort ()) (fun () -> assert false)
let ptr ((_c, s) : Value.int32) : int32 Concolic_choice.t =
match view s with
| Ptr { base; _ } -> Concolic_choice.return base
| _ ->
Log.debug2 {|free: cannot fetch pointer base of "%a"@.|} Expr.pp s;
Concolic_choice.bind (abort ()) (fun () -> assert false)
let exit (_p : Value.int32) : unit Concolic_choice.t = abort ()
let alloc _ (base : Value.int32) (_size : Value.int32) :
Value.int32 Concolic_choice.t =
Concolic_choice.bind (i32 base) (fun (base : int32) ->
Concolic_choice.return (base, Expr.ptr base (Symbolic_value.const_i32 0l)) )
let free _ (p : Value.int32) =
(* WHAT ???? *)
let open Concolic_choice in
let+ base = ptr p in
Value.const_i32 base
end
type extern_func = Concolic.Extern_func.extern_func
open M
let symbolic_extern_module =
let functions =
[ ( "i8_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i8) )
; ( "i32_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i32)
)
; ( "i64_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 I64), symbol_i64)
)
; ( "f32_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 F32), symbol_f32)
)
; ( "f64_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
)
; ( "assume"
, Concolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), assume) )
; ( "assert"
, Concolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), assert') )
]
in
{ Link.functions }
let summaries_extern_module =
let functions =
[ ( "alloc"
, Concolic.Extern_func.Extern_func
(Func (Mem (Arg (I32, Arg (I32, Res))), R1 I32), alloc) )
; ( "dealloc"
, Concolic.Extern_func.Extern_func
(Func (Mem (Arg (I32, Res)), R1 I32), free) )
; ("abort", Concolic.Extern_func.Extern_func (Func (UArg Res, R0), abort))
]
in
{ Link.functions }