diff --git a/src/concrete/concrete.ml b/src/concrete/concrete.ml index 96ebb9993..55baaae2d 100644 --- a/src/concrete/concrete.ml +++ b/src/concrete/concrete.ml @@ -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 diff --git a/src/interpret/interpret.ml b/src/interpret/interpret.ml index 9edf91a48..7cb8efe6d 100644 --- a/src/interpret/interpret.ml +++ b/src/interpret/interpret.ml @@ -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 @@ -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) @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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