Skip to content

Commit 762351e

Browse files
filipeomfilipeom
committed
wip
1 parent bbeaa76 commit 762351e

File tree

8 files changed

+156
-58
lines changed

8 files changed

+156
-58
lines changed

‎src/dune‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,9 +67,11 @@
6767
symbolic_choice_without_memory
6868
symbolic_global
6969
symbolic_memory
70+
symbolic_memory_base
7071
symbolic_memory_concretizing
7172
symbolic_memory_intf
7273
symbolic_memory_make
74+
symbolic_memory_memsight
7375
symbolic_table
7476
symbolic_value
7577
symbolic_wasm_ffi

‎src/symbolic/symbolic.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -136,10 +136,10 @@ struct
136136
end
137137

138138
module P =
139-
MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory)
139+
MakeP [@inlined hint] (Symbolic_memory_memsight) (Thread_with_memory)
140140
(Symbolic_choice_with_memory)
141141
module M =
142-
MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory)
142+
MakeP [@inlined hint] (Symbolic_memory_memsight) (Thread_with_memory)
143143
(Symbolic_choice_minimalist)
144144

145145
let convert_module_to_run (m : 'f Link.module_to_run) =

‎src/symbolic/symbolic_memory_base.ml‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
open Smtml
2+
3+
(* TODO: These functions should be in smtml *)
4+
5+
(* TODO: don't rebuild so many values it generates unecessary hc lookups *)
6+
let merge_extracts (e1, h, m1) (e2, m2, l) =
7+
let ty = Expr.ty e1 in
8+
if m1 = m2 && Expr.equal e1 e2 then
9+
if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l))
10+
else
11+
Expr.(make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))))
12+
13+
let concat ~msb ~lsb offset =
14+
assert (offset > 0 && offset <= 8);
15+
match (Expr.view msb, Expr.view lsb) with
16+
| Val (Num (I8 i1)), Val (Num (I8 i2)) ->
17+
Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
18+
| Val (Num (I8 i1)), Val (Num (I32 i2)) ->
19+
let offset = offset * 8 in
20+
if offset < 32 then
21+
Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2)
22+
else
23+
let i1' = Int64.of_int i1 in
24+
let i2' = Int64.of_int32 i2 in
25+
Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
26+
| Val (Num (I8 i1)), Val (Num (I64 i2)) ->
27+
let offset = Int64.of_int (offset * 8) in
28+
Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
29+
| Extract (e1, h, m1), Extract (e2, m2, l) ->
30+
merge_extracts (e1, h, m1) (e2, m2, l)
31+
| Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
32+
Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)))
33+
| _ -> Expr.make (Concat (msb, lsb))
34+
35+
let extract v pos =
36+
match Expr.view v with
37+
| Val (Num (I8 _)) -> v
38+
| Val (Num (I32 i)) ->
39+
let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
40+
Expr.value (Num (I8 i'))
41+
| Val (Num (I64 i)) ->
42+
let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
43+
Expr.value (Num (I8 i'))
44+
| Cvtop
45+
(_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
46+
| Cvtop
47+
(_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
48+
->
49+
sym
50+
| _ -> Expr.make (Extract (v, pos + 1, pos))

‎src/symbolic/symbolic_memory_concretizing.ml‎

Lines changed: 5 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
module Backend = struct
22
open Smtml
3+
include Symbolic_memory_base
34

45
type address = Int32.t
56

@@ -36,65 +37,16 @@ module Backend = struct
3637
| None -> Expr.value (Num (I8 0))
3738
| Some parent -> load_byte parent a )
3839

39-
(* TODO: don't rebuild so many values it generates unecessary hc lookups *)
40-
let merge_extracts (e1, h, m1) (e2, m2, l) =
41-
let ty = Expr.ty e1 in
42-
if m1 = m2 && Expr.equal e1 e2 then
43-
if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l))
44-
else
45-
Expr.(
46-
make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) )
47-
48-
let concat ~msb ~lsb offset =
49-
assert (offset > 0 && offset <= 8);
50-
match (Expr.view msb, Expr.view lsb) with
51-
| Val (Num (I8 i1)), Val (Num (I8 i2)) ->
52-
Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
53-
| Val (Num (I8 i1)), Val (Num (I32 i2)) ->
54-
let offset = offset * 8 in
55-
if offset < 32 then
56-
Symbolic_value.const_i32
57-
Int32.(logor (shl (of_int i1) (of_int offset)) i2)
58-
else
59-
let i1' = Int64.of_int i1 in
60-
let i2' = Int64.of_int32 i2 in
61-
Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
62-
| Val (Num (I8 i1)), Val (Num (I64 i2)) ->
63-
let offset = Int64.of_int (offset * 8) in
64-
Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
65-
| Extract (e1, h, m1), Extract (e2, m2, l) ->
66-
merge_extracts (e1, h, m1) (e2, m2, l)
67-
| Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
68-
Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)))
69-
| _ -> Expr.make (Concat (msb, lsb))
70-
7140
let loadn m a n =
72-
let rec loop addr size i acc =
73-
if i = size then acc
41+
let rec loop addr i acc =
42+
if i = n then acc
7443
else
7544
let addr' = Int32.(add addr (of_int i)) in
7645
let byte = load_byte m addr' in
77-
loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
46+
loop addr (i + 1) (concat i ~msb:byte ~lsb:acc)
7847
in
7948
let v0 = load_byte m a in
80-
loop a n 1 v0
81-
82-
let extract v pos =
83-
match Expr.view v with
84-
| Val (Num (I8 _)) -> v
85-
| Val (Num (I32 i)) ->
86-
let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
87-
Expr.value (Num (I8 i'))
88-
| Val (Num (I64 i)) ->
89-
let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
90-
Expr.value (Num (I8 i'))
91-
| Cvtop
92-
(_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
93-
| Cvtop
94-
(_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
95-
->
96-
sym
97-
| _ -> Expr.make (Extract (v, pos + 1, pos))
49+
loop a 1 v0
9850

9951
let storen m a v n =
10052
for i = 0 to n - 1 do

‎src/symbolic/symbolic_memory_memsight.ml‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
2+
(* Copyright © 2021-2024 OCamlPro *)
3+
(* Written by the Owi programmers *)
4+
5+
[@@@warning "-69"]
6+
7+
module Memsight_backend = struct
8+
open Smtml
9+
open Symbolic_choice_without_memory
10+
include Symbolic_memory_base
11+
12+
type address = Symbolic_value.int32
13+
14+
type record =
15+
{ address : address
16+
; value : Symbolic_value.int32
17+
; condition : Symbolic_value.vbool
18+
; time : int
19+
}
20+
21+
type t =
22+
{ mutable records : record list
23+
; mutable time : int
24+
}
25+
26+
let make () = { records = []; time = 0 }
27+
28+
let clone { records; time } = { records; time }
29+
30+
let address a = return a
31+
32+
let address_i32 i = Symbolic_value.const_i32 i
33+
34+
let load_byte mem addr =
35+
let open Symbolic_value in
36+
let v = Expr.value (Num (I8 0)) in
37+
List.fold_right
38+
(fun r acc ->
39+
Bool.select_expr
40+
(Bool.and_ (I32.eq addr r.address) r.condition)
41+
~if_true:r.value ~if_false:acc )
42+
mem.records v
43+
44+
let loadn mem addr n =
45+
let open Symbolic_value in
46+
let rec loop i acc =
47+
if i = n then acc
48+
else
49+
let addr' = I32.add addr (const_i32 (Int32.of_int i)) in
50+
let byte = load_byte mem addr' in
51+
loop (i + 1) (concat i ~msb:byte ~lsb:acc)
52+
in
53+
loop 1 (load_byte mem addr)
54+
55+
let storen mem addr v n =
56+
let open Symbolic_value in
57+
mem.time <- succ mem.time;
58+
for i = n - 1 downto 0 do
59+
let record =
60+
{ address = I32.add addr (const_i32 (Int32.of_int i))
61+
; value = extract v i
62+
; condition = Bool.const true
63+
; time = mem.time
64+
}
65+
in
66+
mem.records <- record :: mem.records
67+
done
68+
69+
let validate_address _m a = return (Ok a)
70+
71+
let free _ _ =
72+
Fmt.epr "TODO: Symbolic_memory.free@.";
73+
return ()
74+
75+
let realloc _m ~ptr ~size:_ =
76+
(* Fmt.epr "TODO: Symbolic_memory.replace_size@."; *)
77+
let+ base = select_i32 ptr in
78+
Expr.ptr base (Symbolic_value.const_i32 0l)
79+
80+
let pp_record fmt { address; value; condition; time } =
81+
Fmt.pf fmt "%a, %a, %a, %d" Expr.pp address Expr.pp value Expr.pp condition
82+
time
83+
84+
let pp fmt { time; records; _ } =
85+
Fmt.pf fmt "Time: %d@;" time;
86+
Fmt.pf fmt "Records:@; @[<v 2>%a@]"
87+
(Fmt.list (Fmt.parens pp_record))
88+
records
89+
end
90+
91+
module Memsight_backend' : Symbolic_memory_intf.M = Memsight_backend
92+
93+
include Symbolic_memory_make.Make (Memsight_backend)

‎src/symbolic/thread_with_memory.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
(* Copyright © 2021-2024 OCamlPro *)
33
(* Written by the Owi programmers *)
44

5-
include Thread.Make (Symbolic_memory_concretizing)
5+
include Thread.Make (Symbolic_memory_memsight)
66

77
let project (th : t) : Thread_without_memory.t * _ =
88
let projected =
@@ -25,7 +25,7 @@ let restore backup th =
2525
let pc = Thread_without_memory.pc th in
2626
let memories =
2727
if Thread_without_memory.memories th then
28-
Symbolic_memory_concretizing.clone backup
28+
Symbolic_memory_memsight.clone backup
2929
else backup
3030
in
3131
let tables = Thread_without_memory.tables th in

‎src/symbolic/thread_with_memory.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44

55
(** @inline *)
66
include
7-
Thread.S with type Memory.collection = Symbolic_memory_concretizing.collection
7+
Thread.S with type Memory.collection = Symbolic_memory_memsight.collection
88

99
val project : t -> Thread_without_memory.t * Memory.collection
1010

‎test/sym/memory/basic_store_load_single_address_01.wat‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
i32.const 0x00000000
1010
i32.const 0x50ffc001
1111
i32.store
12+
call $dump_memory
1213
i32.const 0x00000000
1314
i32.load
1415
i32.const 0x50ffc001

0 commit comments

Comments
 (0)