Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

simplify code #418

Merged
merged 3 commits into from
Aug 23, 2024
Merged

simplify code #418

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
377223b
clean code
zapashcanon Aug 22, 2024
1cdfff0
simplify code
zapashcanon Aug 23, 2024
3f9cc80
simplify some checks
zapashcanon Aug 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 3 additions & 17 deletions src/concrete/concrete.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,27 +31,13 @@ module Data = struct
end

module Env = struct
type t = Concrete_value.Func.extern_func Link_env.t

let get_memory = Link_env.get_memory

let get_func = Link_env.get_func
include Link_env

let get_table = Link_env.get_table

let get_elem = Link_env.get_elem
type t = Concrete_value.Func.extern_func Link_env.t

let get_data env n =
let data = Link_env.get_data env n in
let data = get_data env n in
Choice.return data

let get_global = Link_env.get_global

let get_extern_func = Link_env.get_extern_func

let drop_elem = Link_env.drop_elem

let drop_data = Link_env.drop_data
end

module Module_to_run = struct
Expand Down
81 changes: 26 additions & 55 deletions src/interpret/interpret.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -802,9 +802,7 @@ module Make (P : Interpret_intf.P) :
match ref_kind with
| Func_ht ->
let size = Table.size t in
let> out_of_bounds =
Bool.or_ I32.(fun_i < const 0l) @@ I32.(consti size <= fun_i)
in
let> out_of_bounds = I32.(le_u (consti size) fun_i) in
if out_of_bounds then Choice.trap Undefined_element
else
let* fun_i = Choice.select_i32 fun_i in
Expand Down Expand Up @@ -939,18 +937,14 @@ module Make (P : Interpret_intf.P) :
let* mem = Env.get_memory env mem_0 in
let old_size = I64.of_int32 @@ Memory.size mem in
let max_size = Memory.get_limit_max mem in
let delta, stack =
(* TODO: convert to unsigned *)
Stack.pop_i32 stack
in
let delta, stack = Stack.pop_i32 stack in
let delta = I64.(of_int32 delta * page_size) in
let new_size = I64.(old_size + delta) in
let> too_big =
Bool.or_ I64.(delta < const_i64 0L)
@@ Bool.or_ I64.(ge_u new_size (page_size * page_size))
Bool.or_ I64.(ge_u new_size (page_size * page_size))
@@
match max_size with
| Some max -> I64.(new_size > max * page_size)
| Some max -> I64.(gt_u new_size (max * page_size))
| None ->
(* TODO: replace by false... *)
I64.(const_i64 0L <> const_i64 0L)
Expand Down Expand Up @@ -1078,8 +1072,8 @@ module Make (P : Interpret_intf.P) :
Bool.and_
( match Table.max_size t with
| None -> Bool.const true
| Some max -> I32.ge (consti max) new_size )
@@ Bool.and_ (I32.ge new_size (const 0l)) (I32.ge new_size size)
| Some max -> I32.ge_u (consti max) new_size )
(I32.ge_u new_size size)
in
let> allowed in
if not allowed then
Expand All @@ -1095,12 +1089,7 @@ module Make (P : Interpret_intf.P) :
let len, stack = Stack.pop_i32 stack in
let x, stack = Stack.pop_as_ref stack in
let pos, stack = Stack.pop_i32 stack in
let> out_of_bounds =
Bool.or_ (I32.lt len (const 0l))
@@ Bool.or_
(I32.lt pos (const 0l))
(I32.gt I32.(pos + len) (consti (Table.size t)))
in
let> out_of_bounds = I32.gt_u I32.(pos + len) (consti (Table.size t)) in
if out_of_bounds then Choice.trap Out_of_bounds_table_access
else begin
let* pos = Choice.select_i32 pos in
Expand All @@ -1117,9 +1106,9 @@ module Make (P : Interpret_intf.P) :
let> out_of_bounds =
let t_src_len = Table.size t_src in
let t_dst_len = Table.size t_dst in
Bool.or_ (I32.gt I32.(src + len) (consti t_src_len))
@@ Bool.or_ (I32.gt I32.(dst + len) (consti t_dst_len))
@@ Bool.or_ (I32.lt len (const 0l))
Bool.or_ (I32.gt_u I32.(src + len) (consti t_src_len))
@@ Bool.or_ (I32.gt_u I32.(dst + len) (consti t_dst_len))
(* TODO: I don't understand why this last one check is needed... *)
@@ Bool.or_ (I32.lt src (const 0l)) (I32.lt dst (const 0l))
in
if out_of_bounds then Choice.trap Out_of_bounds_table_access
Expand Down Expand Up @@ -1147,18 +1136,10 @@ module Make (P : Interpret_intf.P) :
let table_size = Table.size t in
let elem_len = Elem.size elem in
let> out_of_bounds =
Bool.or_ I32.(pos_x + len > consti elem_len)
@@ Bool.or_ I32.(pos + len > consti table_size)
(* TODO: this is dumb, why do we have to fail even when len = 0 ?
* I don't remember where exactly but somewhere else it's the opposite:
* if len is 0 then we do not fail...
* if it wasn't needed, the following check would be useless
* as the next one would take care of it
* (or maybe not because we don't want to fail
* in the middle of the loop but still...)*)
@@ Bool.or_ I32.(const 0l > len)
@@ Bool.or_ I32.(const 0l > pos)
@@ I32.(const 0l > pos_x)
Bool.or_ I32.(gt_u (pos_x + len) (consti elem_len))
@@ Bool.or_
I32.(gt_u (pos + len) (consti table_size))
I32.(const 0l > pos)
in
if out_of_bounds then Choice.trap Out_of_bounds_table_access
else begin
Expand Down Expand Up @@ -1186,10 +1167,9 @@ module Make (P : Interpret_intf.P) :
let addr = I32.(pos + offset) in
let> out_of_bounds =
Bool.or_ I32.(offset < const 0l)
@@ Bool.or_ I32.(Memory.size mem < addr + const 2l)
@@ Bool.or_ I32.(pos < const 0l)
@@ Bool.or_ I32.(addr + const 2l < const 0l)
@@ I32.(addr < const 0l)
@@ Bool.or_
I32.(lt_u (Memory.size mem) (addr + const 2l))
I32.(pos < const 0l)
in
if out_of_bounds then Choice.trap Out_of_bounds_memory_access
else
Expand All @@ -1209,10 +1189,9 @@ module Make (P : Interpret_intf.P) :
let addr = I32.(pos + offset) in
let> out_of_bounds =
Bool.or_ I32.(offset < const 0l)
@@ Bool.or_ I32.(Memory.size mem < addr + const 1l)
@@ Bool.or_ I32.(pos < const 0l)
@@ Bool.or_ I32.(addr + const 1l < const 0l)
@@ I32.(addr < const 0l)
@@ Bool.or_
I32.(lt_u (Memory.size mem) (addr + const 1l))
I32.(pos < const 0l)
in
if out_of_bounds then Choice.trap Out_of_bounds_memory_access
else
Expand Down Expand Up @@ -1240,10 +1219,9 @@ module Make (P : Interpret_intf.P) :
let addr = I32.(pos + offset) in
let> out_of_bounds =
Bool.or_ I32.(offset < const 0l)
@@ Bool.or_ I32.(Memory.size mem < addr + const 1l)
@@ Bool.or_ I32.(pos < const 0l)
@@ Bool.or_ I32.(addr + const 1l < const 0l)
@@ I32.(addr < const 0l)
@@ Bool.or_
I32.(lt_u (Memory.size mem) (addr + const 1l))
I32.(pos < const 0l)
in
if out_of_bounds then Choice.trap Out_of_bounds_memory_access
else begin
Expand All @@ -1258,9 +1236,7 @@ module Make (P : Interpret_intf.P) :
let offset = const offset in
let addr = I32.(pos + offset) in
let> out_of_bounds =
Bool.or_ I32.(offset < const 0l)
@@ Bool.or_ I32.(pos < const 0l)
@@ I32.(addr < const 0l)
Bool.or_ I32.(offset < const 0l) I32.(pos < const 0l)
in
if out_of_bounds then Choice.trap Out_of_bounds_memory_access
else begin
Expand Down Expand Up @@ -1425,8 +1401,7 @@ module Make (P : Interpret_intf.P) :
let pos, stack = Stack.pop_i32 stack in
let addr = I32.(pos + offset) in
let> out_of_bounds =
Bool.or_ I32.(offset < const 0l)
@@ Bool.or_ I32.(pos < const 0l)
Bool.or_ I32.(pos < const 0l)
@@ I32.(lt_u memory_length (addr + const 4l))
in
if out_of_bounds then Choice.trap Out_of_bounds_memory_access
Expand All @@ -1440,11 +1415,7 @@ module Make (P : Interpret_intf.P) :
st stack
| Br_table (inds, Raw i) ->
let target, stack = Stack.pop_i32 stack in
let> out =
Bool.or_
I32.(target < const 0l)
I32.(target >= const (Int32.of_int (Array.length inds)))
in
let> out = I32.(ge_u target (const (Int32.of_int (Array.length inds)))) in
let* target =
if out then return i
else
Expand Down
Loading