Skip to content

Commit

Permalink
fixes 'concat' function for bit concatenation with i64 promotion
Browse files Browse the repository at this point in the history
- refactor the 'concat' function to improve readability

- automatic promotion to 'i64' when lsb is upwards of 32 bits
  • Loading branch information
filipeom authored and zapashcanon committed Oct 5, 2023
1 parent 4445d60 commit dc88bc1
Showing 1 changed file with 23 additions and 12 deletions.
35 changes: 23 additions & 12 deletions src/symbolic_memory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ module M = struct
let old_size = m.size * page_size in
m.size <- max m.size ((old_size + delta) / page_size)

let size { size; _ } = Value.const_i32 @@ Int32.of_int @@ (size * page_size)
let size { size; _ } = Value.const_i32 @@ Int32.of_int (size * page_size)

let size_in_pages { size; _ } = Value.const_i32 @@ Int32.of_int @@ size

Expand Down Expand Up @@ -69,23 +69,34 @@ module M = struct

let load_byte m a = Option.value (load_byte_opt a m) ~default:Value.I32.zero

let concat a b offset =
match (a, b) with
let concat ~msb ~lsb offset =
assert (offset > 0 && offset <= 8);
match (msb, lsb) with
| Val (Num (I32 i1)), Val (Num (I32 i2)) ->
let offset = Int32.of_int @@ (offset * 8) in
Value.const_i32 (Int32.logor (Int32.shl i1 offset) i2)
let offset = offset * 8 in
if offset < 32 then
Value.const_i32 Int32.(logor (shl i1 (of_int offset)) i2)
else
let i1' = Int64.of_int32 i1 in
let i2' = Int64.of_int32 i2 in
Value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
| Val (Num (I32 i1)), Val (Num (I64 i2)) ->
let offset = Int64.of_int (offset * 8) in
Value.const_i64 Int64.(logor (shl (of_int32 i1) offset) i2)
| Extract (e1, h, m1), Extract (e2, m2, l) when m1 = m2 && Expr.equal e1 e2
->
if h - l = Types.size (Expr.type_of e1) then e1 else Extract (e1, h, l)
| _ -> Concat (a, b)
-> (
match Expr.type_of e1 with
| Some t -> if h - l = Types.size t then e1 else Extract (e1, h, l)
| _ -> Extract (e1, h, l) )
| _ -> Concat (msb, lsb)

let loadn m a n : int32 =
let rec loop addr n i v =
if i = n then v
let rec loop addr size i acc =
if i = size then acc
else
let addr' = Int32.add addr @@ Int32.of_int i in
let addr' = Int32.(add addr (of_int i)) in
let byte = load_byte m addr' in
loop addr n (i + 1) (concat byte v i)
loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
in
let v0 = load_byte m a in
loop a n 1 v0
Expand Down

0 comments on commit dc88bc1

Please sign in to comment.