From 17b35c465bf8aca074c8354e910af0bf8f686c09 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 26 Mar 2021 17:22:55 +0100 Subject: bugfix and printOp --- riscV/ExpansionOracle.ml | 42 +++++++++++++++++++++++------------------- riscV/PrintOp.ml | 6 ++++++ 2 files changed, 29 insertions(+), 19 deletions(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index a5fa4a0a..6eb82274 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -59,14 +59,15 @@ type immt = | Sltil | Sltiul -let find_or_addnmove op args rd succ map_consts node_dec = +let find_or_addnmove op args rd succ map_consts not_final = let sop = Sop (op, args) in match Hashtbl.find_opt map_consts sop with | Some r -> - if node_dec then node := !node - 1; + if not_final then node := !node - 1; Sr (P.of_int r) | None -> - Hashtbl.add map_consts sop (p2i rd); + if not (List.exists (fun a -> a = rd) args) && not_final then + Hashtbl.add map_consts sop (p2i rd); Si (Iop (op, args, rd, succ)) let build_head_tuple head sv = @@ -75,59 +76,62 @@ let build_head_tuple head sv = let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r let unzip_head_tuple_move ht r succ = - match ht with l, Some r' -> [ Iop (Omove, [ r' ], r, succ) ] | l, None -> l + match ht with + | l, Some r' -> + if r' != r then [ Iop (Omove, [ r' ], r, succ) ] else [ Inop succ ] + | l, None -> l let build_full_ilist op args dest succ hd k map_consts = let sv = find_or_addnmove op args dest succ map_consts false in let ht = build_head_tuple hd sv in unzip_head_tuple_move ht dest succ @ k -let load_hilo32 dest hi lo succ map_consts node_dec = +let load_hilo32 dest hi lo succ map_consts not_final = let op1 = OEluiw hi in if Int.eq lo Int.zero then - let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in + let sv = find_or_addnmove op1 [] dest succ map_consts not_final in build_head_tuple [] sv else let r = r2pi () in - let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in + let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in let ht1 = build_head_tuple [] sv1 in let r' = unzip_head_tuple ht1 r in let op2 = OEaddiw lo in - let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in + let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in build_head_tuple (fst ht1) sv2 -let load_hilo64 dest hi lo succ map_consts node_dec = +let load_hilo64 dest hi lo succ map_consts not_final = let op1 = OEluil hi in if Int64.eq lo Int64.zero then - let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in + let sv = find_or_addnmove op1 [] dest succ map_consts not_final in build_head_tuple [] sv else let r = r2pi () in - let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in + let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in let ht1 = build_head_tuple [] sv1 in let r' = unzip_head_tuple ht1 r in let op2 = OEaddil lo in - let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in + let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in build_head_tuple (fst ht1) sv2 -let loadimm32 dest n succ map_consts node_dec = +let loadimm32 dest n succ map_consts not_final = match make_immed32 n with | Imm32_single imm -> let op1 = OEaddiwr0 imm in - let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in + let sv = find_or_addnmove op1 [] dest succ map_consts not_final in build_head_tuple [] sv - | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts node_dec + | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts not_final -let loadimm64 dest n succ map_consts node_dec = +let loadimm64 dest n succ map_consts not_final = match make_immed64 n with | Imm64_single imm -> let op1 = OEaddilr0 imm in - let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in + let sv = find_or_addnmove op1 [] dest succ map_consts not_final in build_head_tuple [] sv - | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts node_dec + | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts not_final | Imm64_large imm -> let op1 = OEloadli imm in - let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in + let sv = find_or_addnmove op1 [] dest succ map_consts not_final in build_head_tuple [] sv let get_opimm imm = function diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index a37f5c9c..4494080e 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -209,6 +209,8 @@ let print_operation reg pp = function | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(X0,%ld)" (camlint_of_coqint n) + | OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0) | OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0) | OEsequl optR0, [r1;r2] -> fprintf pp "OEsequl"; (get_optR0_s Ceq reg pp r1 r2 optR0) @@ -221,8 +223,12 @@ let print_operation reg pp = function | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n) | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(X0,%ld)" (camlint_of_coqint n) + | OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n) | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n) | OEmayundef isl, [r1;r2] -> fprintf pp "OEmayundef (%b,%a,%a)" isl reg r1 reg r2 + | OEshrxundef n, [r1] -> fprintf pp "OEshrxundef (%ld,%a)" (camlint_of_coqint n) reg r1 + | OEshrxlundef n, [r1] -> fprintf pp "OEshrxlundef (%ld,%a)" (camlint_of_coqint n) reg r1 | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 -- cgit