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
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)
open Syntax
let run_file ~unsafe ~optimize filename model =
let next =
let next = ref ~-1 in
fun () ->
incr next;
!next
in
let assume_i32 _ = () in
let assume_positive_i32 _ = () in
let assert_i32 n = assert (not @@ Prelude.Int32.equal n 0l) in
let symbol_i32 () =
match model.(next ()) with
| Concrete_value.I32 n -> n
| v ->
Fmt.epr "Got value %a but expected a i32 value." Concrete_value.pp v;
assert false
in
let symbol_char () =
match model.(next ()) with
| Concrete_value.I32 n -> n
| v ->
Fmt.epr "Got value %a but expected a char (i32) value." Concrete_value.pp
v;
assert false
in
let symbol_i8 () =
match model.(next ()) with
| Concrete_value.I32 n -> n
| v ->
Fmt.epr "Got value %a but expected a i8 (i32) value." Concrete_value.pp v;
assert false
in
let symbol_i64 () =
match model.(next ()) with
| Concrete_value.I64 n -> n
| v ->
Fmt.epr "Got value %a but expected a i64 value." Concrete_value.pp v;
assert false
in
let symbol_f32 () =
match model.(next ()) with
| Concrete_value.F32 n -> n
| v ->
Fmt.epr "Got value %a but expected a f32 value." Concrete_value.pp v;
assert false
in
let symbol_f64 () =
match model.(next ()) with
| Concrete_value.F64 n -> n
| v ->
Fmt.epr "Got value %a but expected a f64 value." Concrete_value.pp v;
assert false
in
let replay_extern_module =
let functions =
[ ( "i8_symbol"
, Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_i8)
)
; ( "char_symbol"
, Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_char)
)
; ( "i32_symbol"
, Concrete_value.Func.Extern_func (Func (UArg Res, R1 I32), symbol_i32)
)
; ( "i64_symbol"
, Concrete_value.Func.Extern_func (Func (UArg Res, R1 I64), symbol_i64)
)
; ( "f32_symbol"
, Concrete_value.Func.Extern_func (Func (UArg Res, R1 F32), symbol_f32)
)
; ( "f64_symbol"
, Concrete_value.Func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
)
; ( "assume"
, Concrete_value.Func.Extern_func (Func (Arg (I32, Res), R0), assume_i32)
)
; ( "assume_positive_i32"
, Concrete_value.Func.Extern_func
(Func (Arg (I32, Res), R0), assume_positive_i32) )
; ( "assert"
, Concrete_value.Func.Extern_func (Func (Arg (I32, Res), R0), assert_i32)
)
]
in
{ Link.functions }
in
let link_state =
Link.extern_module Link.empty_state ~name:"symbolic" replay_extern_module
in
let* m =
Compile.File.until_binary_validate ~rac:false ~srac:false ~unsafe filename
in
let* m = Cmd_utils.add_main_as_start m in
let* m, link_state =
Compile.Binary.until_link ~unsafe link_state ~optimize ~name:None m
in
let c = Interpret.Concrete.modul link_state.envs m in
c
let cmd ~profiling ~debug ~unsafe ~optimize ~replay_file ~source_file =
if profiling then Log.profiling_on := true;
if debug then Log.debug_on := true;
let* model =
match Smtml.Model.Parse.Scfg.from_file replay_file with
| Error msg -> Error (`Invalid_model msg)
| Ok model ->
let+ model =
list_map
(fun (_sym, v) ->
match v with
| Smtml.Value.False -> Ok (Concrete_value.I32 0l)
| True -> Ok (Concrete_value.I32 1l)
| Num (I8 n) -> Ok (Concrete_value.I32 (Int32.of_int n))
| Num (I32 n) -> Ok (Concrete_value.I32 n)
| Num (I64 n) -> Ok (Concrete_value.I64 n)
| Num (F32 n) -> Ok (Concrete_value.F32 (Float32.of_bits n))
| Num (F64 n) -> Ok (Concrete_value.F64 (Float64.of_bits n))
| Unit | Int _ | Real _ | Str _ | List _ | App _ | Nothing ->
Error
(`Invalid_model
(Fmt.str "unexpected value type: %a" Smtml.Value.pp v) ) )
(Smtml.Model.get_bindings model)
in
Array.of_list model
in
let+ () = run_file ~unsafe ~optimize source_file model in
Fmt.pr "All OK@."