diff options
| author | Pierre-Marie Pédrot | 2018-07-04 23:24:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-12 16:22:25 +0200 |
| commit | f7d57c92a2fed40099b33fa2d804861c02c95ec6 (patch) | |
| tree | 0b01bc8935a265d53a0dea8400ad9062cd32a6d7 /kernel/nativevalues.ml | |
| parent | 31fce698ec8c3186dc6af49961e8572e81cab50b (diff) | |
Fix #7854: Native compilation + flambda trigger SEGFAULT.
We use a more abstract representation for accumulators in the native
compilation scheme, that requires less fiddling with low-level implementation
details. It might be slower though.
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 63 |
1 files changed, 30 insertions, 33 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 3901cb9ce4..91f6add1c3 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -68,28 +68,29 @@ type atom = let accumulate_tag = 0 -let accumulate_code (k:accumulator) (x:t) = - let o = Obj.repr k in - let osize = Obj.size o in - let r = Obj.new_block accumulate_tag (osize + 1) in - for i = 0 to osize - 1 do - Obj.set_field r i (Obj.field o i) - done; - Obj.set_field r osize (Obj.repr x); - (Obj.obj r:t) - -let rec accumulate (x:t) = - accumulate_code (Obj.magic accumulate) x - -let mk_accu_gen rcode (a:atom) = -(* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *) - let r = Obj.new_block 0 3 in - Obj.set_field r 0 (Obj.field (Obj.magic rcode) 0); - Obj.set_field r 1 (Obj.field (Obj.magic rcode) 1); - Obj.set_field r 2 (Obj.magic a); - (Obj.magic r:t);; - -let mk_accu (a:atom) = mk_accu_gen accumulate a +(** Unique pointer used to drive the accumulator function *) +let ret_accu = Obj.repr (ref ()) + +type accu_val = { mutable acc_atm : atom; acc_arg : Obj.t list } + +let mk_accu (a : atom) : t = + let rec accumulate data x = + if x == ret_accu then Obj.repr data + else + let data = { data with acc_arg = x :: data.acc_arg } in + let ans = Obj.repr (accumulate data) in + let () = Obj.set_tag ans accumulate_tag in + ans + in + let acc = { acc_atm = a; acc_arg = [] } in + let ans = Obj.repr (accumulate acc) in + (** FIXME: use another representation for accumulators, this causes naked + pointers. *) + let () = Obj.set_tag ans accumulate_tag in + (Obj.obj ans : t) + +let get_accu (k : accumulator) = + (Obj.magic k : Obj.t -> accu_val) ret_accu let mk_rel_accu i = mk_accu (Arel i) @@ -141,31 +142,27 @@ let mk_proj_accu kn c = mk_accu (Aproj (kn,c)) let atom_of_accu (k:accumulator) = - (Obj.magic (Obj.field (Obj.magic k) 2) : atom) + (get_accu k).acc_atm let set_atom_of_accu (k:accumulator) (a:atom) = - Obj.set_field (Obj.magic k) 2 (Obj.magic a) + (get_accu k).acc_atm <- a let accu_nargs (k:accumulator) = - let nargs = Obj.size (Obj.magic k) - 3 in -(* if nargs < 0 then Format.eprintf "nargs = %i\n" nargs; *) - assert (nargs >= 0); - nargs + List.length (get_accu k).acc_arg let args_of_accu (k:accumulator) = - let nargs = accu_nargs k in - let f i = (Obj.magic (Obj.field (Obj.magic k) (nargs-i+2)) : t) in - Array.init nargs f + let acc = (get_accu k).acc_arg in + (Obj.magic (Array.of_list acc) : t array) let is_accu x = let o = Obj.repr x in Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag let mk_fix_accu rec_pos pos types bodies = - mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos)) + mk_accu (Afix(types,bodies,rec_pos, pos)) let mk_cofix_accu pos types norm = - mk_accu_gen accumulate (Acofix(types,norm,pos,(Obj.magic 0 : t))) + mk_accu (Acofix(types,norm,pos,(Obj.magic 0 : t))) let upd_cofix (cofix :t) (cofix_fun : t) = let atom = atom_of_accu (Obj.magic cofix) in |
