Skip to content

Commit

Permalink
Fix static slicer handling of removed return instructions
Browse files Browse the repository at this point in the history
  • Loading branch information
acieroid committed Feb 15, 2024
1 parent f59dabc commit 768a57f
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 11 deletions.
23 changes: 13 additions & 10 deletions lib/analysis/slice/slicing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -112,8 +112,8 @@ let instructions_to_keep (cfg : Spec.t Cfg.t) (cfg_instructions : Spec.t Instr.t
let data_deps : InSlice.Set.t = match def with
| Use_def.Def.Instruction (instr', var) ->
Log.info
(Printf.sprintf "Instruction %s is part of the slice due to its data dependence on %s"
(Instr.Label.to_string instr') (Var.to_string var));
(Printf.sprintf "Instruction %s (%s) is part of the slice due to its data dependence on %s"
(Instr.Label.to_string instr') (Instr.to_string (Instr.Label.Map.find_exn cfg_instructions instr')) (Var.to_string var));
InSlice.Set.singleton (InSlice.make instr' (Some var) cfg_instructions)
| Use_def.Def.Entry _ -> InSlice.Set.empty
| Use_def.Def.Constant _ -> InSlice.Set.empty in
Expand All @@ -124,17 +124,17 @@ let instructions_to_keep (cfg : Spec.t Cfg.t) (cfg_instructions : Spec.t Instr.t
| Some deps -> InSlice.Set.of_list (List.map (Instr.Label.Set.to_list deps)
~f:(fun label ->
Log.info
(Printf.sprintf "Instruction %s is part of the slice due to control dependences"
(Instr.Label.to_string label));
(Printf.sprintf "Instruction %s (%s) is part of the slice due to control dependences"
(Instr.Label.to_string label) (Instr.to_string (Instr.Label.Map.find_exn cfg_instructions label)));
InSlice.make label None cfg_instructions)) in
let worklist'' = InSlice.Set.union worklist' control_deps in
(* For instr' in mem_deps(instr): add instr to W *)
let worklist''' = InSlice.Set.union worklist''
(InSlice.Set.of_list
(List.map ~f:(fun label ->
Log.info
(Printf.sprintf "Instruction %s is part of the slice due to memory dependences"
(Instr.Label.to_string label));
(Printf.sprintf "Instruction %s (%s) is part of the slice due to memory dependences"
(Instr.Label.to_string label) (Instr.to_string (Instr.Label.Map.find_exn cfg_instructions label)));
InSlice.make label None cfg_instructions)
(Instr.Label.Set.to_list (Memory_deps.deps_for preanalysis.mem_dependencies slicepart.label)))) in
loop (InSlice.Set.remove worklist''' slicepart) slice' visited' in
Expand Down Expand Up @@ -220,7 +220,7 @@ let type_of_data

let type_of_control
(i : ('a Instr.control, 'a) Instr.labelled)
(cfg : unit Cfg.t)
(_cfg : unit Cfg.t)
(instructions_map : Spec.t Instr.t Instr.Label.Map.t)
: instr_type_element list * instr_type_element list =
let vstack_before = match Cfg.find_instr instructions_map i.label with
Expand Down Expand Up @@ -262,7 +262,10 @@ let type_of_control
let vstack = List.drop vstack_before 1 in
([T Type.I32] @ (List.mapi vstack ~f:(fun i _ -> Any (string_of_int i))), [])
| Return ->
(List.mapi vstack_before ~f:(fun i _ -> Any (string_of_int i)), (List.map cfg.return_types ~f:(fun t -> T t)))
(List.mapi vstack_before ~f:(fun i _ -> Any (string_of_int i)),
(* was this, but it actually doesn't leave anything on the stack:
(List.map cfg.return_types ~f:(fun t -> T t)) *)
[])
| Unreachable -> ([], [])
| Merge -> ([], [])
| Block _ | Loop _ -> failwith "should not happen" (* because we have the block/loop instructions handled in the first match *)
Expand Down Expand Up @@ -322,11 +325,11 @@ let replace_with_equivalent_instructions (instrs : unit Instr.t list) (cfg : 'a
if List.is_empty instrs then instrs else
let t = instrs_type instrs cfg instructions_map in
let replaced = List.map (dummy_instrs t next_label) ~f:(fun i -> Instr.Data i) in
(* Log.info (Printf.sprintf "Replacing instructions %s of type %s -> %s with %s"
Log.info (Printf.sprintf "Replacing instructions %s of type %s -> %s with %s"
(String.concat ~sep:"," (List.map ~f:Instr.to_string instrs))
(String.concat ~sep:"," (List.map ~f:instr_type_element_to_string (fst t)))
(String.concat ~sep:"," (List.map ~f:instr_type_element_to_string (snd t)))
(String.concat ~sep:"," (List.map ~f:Instr.to_string replaced))); *)
(String.concat ~sep:"," (List.map ~f:Instr.to_string replaced)));
replaced

(* Check if the body is empty or only consist only of dummy instructions *)
Expand Down
3 changes: 2 additions & 1 deletion lib/wasm/instr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -219,10 +219,11 @@ let rec control_to_string ?sep:(sep : string = "\n") ?indent:(i : int = 0) ?anno

(** Converts an instruction to its string representation *)
and to_string ?sep:(sep : string = "\n") ?indent:(i : int = 0) ?annot_str:(annot_to_string : 'a -> string = fun _ -> "") (instr : 'a t) : string =
Printf.sprintf "%s%s" (* (Label.to_string (label instr)) *) (String.make i ' ')
Printf.sprintf "%s%s" (String.make i ' ')
(match instr with
| Data instr -> data_to_string instr.instr
| Control instr -> control_to_string instr.instr ~annot_str:annot_to_string ~sep:sep ~indent:i)
(* (Label.to_string (label instr)) *)
and list_to_string ?indent:(i : int = 0) ?sep:(sep : string = ", ") (l : 'a t list) (annot_to_string : 'a -> string) : string =
String.concat ~sep:sep (List.map l ~f:(fun instr -> to_string instr ~annot_str:annot_to_string ?sep:(Some sep) ?indent:(Some i)))

Expand Down

0 comments on commit 768a57f

Please sign in to comment.