Skip to content

Commit

Permalink
Cleaning up AArch64Sem.ml (in relation to the bugfixes)
Browse files Browse the repository at this point in the history
Removing a comment. Removing a bit of logic preparing a list of
overwriting instructions: currently instructions loaded from the initial
state are a superset of what gets loaded from code, therefore, removing
the latter.
  • Loading branch information
artkhyzha committed Jul 18, 2023
1 parent 73576a4 commit a364b22
Showing 1 changed file with 4 additions and 14 deletions.
18 changes: 4 additions & 14 deletions herd/AArch64Sem.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2701,19 +2701,15 @@ module Make
* overwrite another. By convention, those are
* instructions pointed to by "exported" labels.
*)
let get_overwriting_instrs lbls test =
let get_overwriting_instrs test =
let init_instrs =
AArch64.state_fold
(fun _ v k ->
match v with
| V.Val (Constant.Instruction i) -> i::k
| _ -> k)
test.Test_herd.init_state []
and code_instrs =
List.map
(fun (_,i) -> i)
(AArch64.from_labels lbls test.Test_herd.nice_prog) in
init_instrs@code_instrs
test.Test_herd.init_state [] in
init_instrs


(* Test all possible instructions, when appropriate *)
Expand All @@ -2734,15 +2730,9 @@ module Make
| Some hd ->
let insts =
InstrSet.of_list
(get_overwriting_instrs lbls test) in
(get_overwriting_instrs test) in
let insts =
InstrSet.add inst (InstrSet.filter AArch64.can_overwrite insts) in
if false then
Printf.eprintf "%s: {%s}\n%!"
(Label.pp hd)
(String.concat ","
(List.map AArch64.V.Cst.Instr.pp
(InstrSet.elements insts))) ;
(* Shadow default control sequencing operator *)
let(>>*=) = M.bind_control_set_data_input_first in
let a_v = make_label_value ii.A.fetch_proc hd in
Expand Down

0 comments on commit a364b22

Please sign in to comment.