diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-06 12:36:11 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-06 12:36:11 +0100 |
commit | c19ecc9326d0278989d7651bf8c8cf0d1c387235 (patch) | |
tree | 479bd06ca0ed2e2d14900a78c93914537e4a7d91 /riscV | |
parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
download | compcert-kvx-c19ecc9326d0278989d7651bf8c8cf0d1c387235.tar.gz compcert-kvx-c19ecc9326d0278989d7651bf8c8cf0d1c387235.zip |
Adding a mini CSE pass in the expansion oracle
Diffstat (limited to 'riscV')
-rw-r--r-- | riscV/Asmgen.v | 8 | ||||
-rw-r--r-- | riscV/Asmgenproof1.v | 6 | ||||
-rw-r--r-- | riscV/ExpansionOracle.ml | 238 | ||||
-rw-r--r-- | riscV/NeedOp.v | 5 | ||||
-rw-r--r-- | riscV/Op.v | 63 | ||||
-rw-r--r-- | riscV/PrintOp.ml | 5 | ||||
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 90 | ||||
-rw-r--r-- | riscV/ValueAOp.v | 41 |
8 files changed, 263 insertions, 193 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 957166b6..87db0181 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -565,10 +565,10 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pxoriw rd rs n :: k) - | OEluiw n _, a1 :: nil => + | OEluiw n, nil => do rd <- ireg_of res; OK (Pluiw rd n :: k) - | OEaddiwr0 n _, a1 :: nil => + | OEaddiwr0 n, nil => do rd <- ireg_of res; OK (Paddiw rd X0 n :: k) | OEseql optR0, a1 :: a2 :: nil => @@ -613,10 +613,10 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pxoril rd rs n :: k) - | OEluil n, a1 :: nil => + | OEluil n, nil => do rd <- ireg_of res; OK (Pluil rd n :: k) - | OEaddilr0 n, a1 :: nil => + | OEaddilr0 n, nil => do rd <- ireg_of res; OK (Paddil rd X0 n :: k) | OEloadli n, nil => diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index f0def29b..20d9e1da 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -641,11 +641,11 @@ Opaque Int.eq. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } (* Expanded instructions from RTL *) - 7,8,15,16: + 7,14: econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl; + split; intros; Simpl; simpl; try rewrite Int.add_commut; try rewrite Int64.add_commut; - destruct (rs (preg_of m0)); try discriminate; eauto. + auto. 1-12: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; econstructor; split; try apply exec_straight_one; simpl; eauto; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 95a300c5..44049ecf 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -20,14 +20,21 @@ open Asmgen open DebugPrint open RTLpath open! Integers +open Camlcoq + +type sop = Sop of operation * P.t list + +type sval = Si of RTL.instruction | Sr of P.t let reg = ref 1 let node = ref 1 -let r2p () = Camlcoq.P.of_int !reg +let p2i r = P.to_int r + +let r2p () = P.of_int !reg -let n2p () = Camlcoq.P.of_int !node +let n2p () = P.of_int !node let r2pi () = reg := !reg + 1; @@ -39,30 +46,72 @@ let n2pi () = type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul -let load_hilo32 a1 dest hi lo succ is_long k = - if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k +let debug_was_cse = ref false + +let find_or_addnmove op args rd succ sargs map_consts = + let sop = Sop (op, sargs) in + match Hashtbl.find_opt map_consts sop with + | Some r -> + debug_was_cse := true; + Sr (P.of_int r) + | None -> + Hashtbl.add map_consts sop (p2i rd); + Si (Iop (op, args, rd, succ)) + +let build_head_tuple head sv = + match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r) + +let load_hilo32 dest hi lo succ map_consts = + let op1 = OEluiw hi in + if Int.eq lo Int.zero then + let sv = find_or_addnmove op1 [] dest succ [] map_consts in + build_head_tuple [] sv else let r = r2pi () in - Iop (OEluiw (hi, is_long), [ a1 ], r, n2pi ()) - :: Iop (Oaddimm lo, [ r ], dest, succ) :: k - -let load_hilo64 a1 dest hi lo succ k = - if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k + let op2 = Oaddimm lo in + match find_or_addnmove op1 [] r (n2pi ()) [] map_consts with + | Si i -> + let sv = find_or_addnmove op2 [ r ] dest succ [ r ] map_consts in + build_head_tuple [ i ] sv + | Sr r' -> + let sv = find_or_addnmove op2 [ r' ] dest succ [ r' ] map_consts in + build_head_tuple [] sv + +let load_hilo64 dest hi lo succ map_consts = + let op1 = OEluil hi in + if Int64.eq lo Int64.zero then + let sv = find_or_addnmove op1 [] dest succ [] map_consts in + build_head_tuple [] sv else let r = r2pi () in - Iop (OEluil hi, [ a1 ], r, n2pi ()) - :: Iop (Oaddlimm lo, [ r ], dest, succ) :: k - -let loadimm32 a1 dest n succ is_long k = + let op2 = Oaddlimm lo in + match find_or_addnmove op1 [] r (n2pi ()) [] map_consts with + | Si i -> + let sv = find_or_addnmove op2 [ r ] dest succ [ r ] map_consts in + build_head_tuple [ i ] sv + | Sr r' -> + let sv = find_or_addnmove op2 [ r' ] dest succ [ r' ] map_consts in + build_head_tuple [] sv + +let loadimm32 dest n succ map_consts = match make_immed32 n with - | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [ a1 ], dest, succ) :: k - | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k + | Imm32_single imm -> + let op1 = OEaddiwr0 imm in + let sv = find_or_addnmove op1 [] dest succ [] map_consts in + build_head_tuple [] sv + | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts -let loadimm64 a1 dest n succ k = +let loadimm64 dest n succ map_consts = match make_immed64 n with - | Imm64_single imm -> Iop (OEaddilr0 imm, [ a1 ], dest, succ) :: k - | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k - | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k + | Imm64_single imm -> + let op1 = OEaddilr0 imm in + let sv = find_or_addnmove op1 [] dest succ [] map_consts in + build_head_tuple [] sv + | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts + | Imm64_large imm -> + let op1 = OEloadli imm in + let sv = find_or_addnmove op1 [] dest succ [] map_consts in + build_head_tuple [] sv let get_opimm imm = function | Xoriw -> OExoriw imm @@ -72,32 +121,42 @@ let get_opimm imm = function | Sltil -> OEsltil imm | Sltiul -> OEsltiul imm -let opimm32 a1 dest n succ is_long k op opimm = +let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r + +let opimm32 a1 dest n succ k op opimm map_consts = match make_immed32 n with | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm32_pair (hi, lo) -> let r = r2pi () in - load_hilo32 a1 r hi lo (n2pi ()) is_long - (Iop (op, [ a1; r ], dest, succ) :: k) + let ht = load_hilo32 r hi lo (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k -let opimm64 a1 dest n succ k op opimm = +let opimm64 a1 dest n succ k op opimm map_consts = match make_immed64 n with | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm64_pair (hi, lo) -> let r = r2pi () in - load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k) + let ht = load_hilo64 r hi lo (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k | Imm64_large imm -> let r = r2pi () in - Iop (OEloadli imm, [], r, n2pi ()) :: Iop (op, [ a1; r ], dest, succ) :: k + let op1 = OEloadli imm in + let inode = n2pi () in + let sv = find_or_addnmove op1 [] r inode [] map_consts in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k -let xorimm32 a1 dest n succ is_long k = - opimm32 a1 dest n succ is_long k Oxor Xoriw +let xorimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k Oxor Xoriw map_consts -let sltimm32 a1 dest n succ is_long k = - opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw +let sltimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k (OEsltw None) Sltiw map_consts -let sltuimm32 a1 dest n succ is_long k = - opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw +let sltuimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril @@ -233,85 +292,101 @@ let cond_single cmp f1 f2 dest succ = | Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ) | Cge -> Iop (OEfles, [ f2; f1 ], dest, succ) -let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k = +let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts = if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - loadimm32 a1 r n (n2pi ()) false - (cbranch_int32s false cmp a1 r info succ1 succ2 k) + let ht = loadimm32 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k -let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k = +let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts = if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - loadimm32 a1 r n (n2pi ()) false - (cbranch_int32u false cmp a1 r info succ1 succ2 k) + let ht = loadimm32 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k -let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k = +let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts = if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - loadimm64 a1 r n (n2pi ()) - (cbranch_int64s false cmp a1 r info succ1 succ2 k) + let ht = loadimm64 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k -let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k = +let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts = if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - loadimm64 a1 r n (n2pi ()) - (cbranch_int64u false cmp a1 r info succ1 succ2 k) + let ht = loadimm64 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k -let expanse_condimm_int32s cmp a1 n dest succ k = +let expanse_condimm_int32s cmp a1 n dest succ k map_consts = if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k else match cmp with | Ceq | Cne -> let r = r2pi () in - xorimm32 a1 r n (n2pi ()) false (cond_int32s true cmp r r dest succ k) - | Clt -> sltimm32 a1 dest n succ false k + xorimm32 a1 r n (n2pi ()) + (cond_int32s true cmp r r dest succ k) + map_consts + | Clt -> sltimm32 a1 dest n succ k map_consts | Cle -> if Int.eq n (Int.repr Int.max_signed) then - loadimm32 a1 dest Int.one succ false k - else sltimm32 a1 dest (Int.add n Int.one) succ false k + let ht = loadimm32 dest Int.one succ map_consts in + fst ht @ k + else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts | _ -> let r = r2pi () in - loadimm32 a1 r n (n2pi ()) false - (cond_int32s false cmp a1 r dest succ k) + let ht = loadimm32 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cond_int32s false cmp a1 r' dest succ k -let expanse_condimm_int32u cmp a1 n dest succ k = +let expanse_condimm_int32u cmp a1 n dest succ k map_consts = if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k else match cmp with - | Clt -> sltuimm32 a1 dest n succ false k + | Clt -> sltuimm32 a1 dest n succ k map_consts | _ -> let r = r2pi () in - loadimm32 a1 r n (n2pi ()) false - (cond_int32u false cmp a1 r dest succ k) + let ht = loadimm32 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cond_int32u false cmp a1 r' dest succ k -let expanse_condimm_int64s cmp a1 n dest succ k = +let expanse_condimm_int64s cmp a1 n dest succ k map_consts = if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k else match cmp with | Ceq | Cne -> let r = r2pi () in - xorimm64 a1 r n (n2pi ()) (cond_int64s true cmp r r dest succ k) - | Clt -> sltimm64 a1 dest n succ k + xorimm64 a1 r n (n2pi ()) + (cond_int64s true cmp r r dest succ k) + map_consts + | Clt -> sltimm64 a1 dest n succ k map_consts | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) then - loadimm32 a1 dest Int.one succ true k - else sltimm64 a1 dest (Int64.add n Int64.one) succ k + let ht = loadimm32 dest Int.one succ map_consts in + fst ht @ k + else sltimm64 a1 dest (Int64.add n Int64.one) succ k map_consts | _ -> let r = r2pi () in - loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k) + let ht = loadimm64 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cond_int64s false cmp a1 r' dest succ k -let expanse_condimm_int64u cmp a1 n dest succ k = +let expanse_condimm_int64u cmp a1 n dest succ k map_consts = if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k else match cmp with - | Clt -> sltuimm64 a1 dest n succ k + | Clt -> sltuimm64 a1 dest n succ k map_consts | _ -> let r = r2pi () in - loadimm64 a1 r n (n2pi ()) (cond_int64u false cmp a1 r dest succ k) + let ht = loadimm64 r n (n2pi ()) map_consts in + let r' = unzip_head_tuple ht r in + fst ht @ cond_int64u false cmp a1 r' dest succ k let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = let normal = is_normal_cmp cmp in @@ -368,12 +443,12 @@ let write_pathmap initial esize pm' = let rec write_tree exp current code' new_order = match exp with | (Iop (_, _, _, succ) as inst) :: k -> - code' := PTree.set (Camlcoq.P.of_int current) inst !code'; - new_order := Camlcoq.P.of_int current :: !new_order; + code' := PTree.set (P.of_int current) inst !code'; + new_order := P.of_int current :: !new_order; write_tree k (current - 1) code' new_order | (Icond (_, _, succ1, succ2, _) as inst) :: k -> - code' := PTree.set (Camlcoq.P.of_int current) inst !code'; - new_order := Camlcoq.P.of_int current :: !new_order; + code' := PTree.set (P.of_int current) inst !code'; + new_order := P.of_int current :: !new_order; write_tree k (current - 1) code' new_order | [] -> () | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." @@ -387,11 +462,13 @@ let expanse (sb : superblock) code pm = let was_exp = ref false in let code' = ref code in let pm' = ref pm in + let map_consts = Hashtbl.create 100 in Array.iter (fun n -> was_branch := false; was_exp := false; let inst = get_some @@ PTree.get n code in + (*print_instruction stderr (0, inst);*) (match inst with | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccomp\n"; @@ -403,11 +480,11 @@ let expanse (sb : superblock) code pm = was_exp := true | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompimm\n"; - exp := expanse_condimm_int32s c a1 imm dest succ []; + exp := expanse_condimm_int32s c a1 imm dest succ [] map_consts; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompuimm\n"; - exp := expanse_condimm_int32u c a1 imm dest succ []; + exp := expanse_condimm_int32u c a1 imm dest succ [] map_consts; was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompl\n"; @@ -419,11 +496,11 @@ let expanse (sb : superblock) code pm = was_exp := true | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccomplimm\n"; - exp := expanse_condimm_int64s c a1 imm dest succ []; + exp := expanse_condimm_int64s c a1 imm dest succ [] map_consts; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompluimm\n"; - exp := expanse_condimm_int64u c a1 imm dest succ []; + exp := expanse_condimm_int64u c a1 imm dest succ [] map_consts; was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Ccompf\n"; @@ -453,12 +530,14 @@ let expanse (sb : superblock) code pm = was_exp := true | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccompimm\n"; - exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 []; + exp := + expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [] map_consts; was_branch := true; was_exp := true | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccompuimm\n"; - exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 []; + exp := + expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [] map_consts; was_branch := true; was_exp := true | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> @@ -473,12 +552,14 @@ let expanse (sb : superblock) code pm = was_exp := true | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccomplimm\n"; - exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 []; + exp := + expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [] map_consts; was_branch := true; was_exp := true | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> debug "Icond/Ccompluimm\n"; - exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 []; + exp := + expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [] map_consts; was_branch := true; was_exp := true | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> @@ -509,9 +590,7 @@ let expanse (sb : superblock) code pm = let lives = PTree.get n !liveins in match lives with | Some lives -> - let new_branch_pc = - Camlcoq.P.of_int (!node - (List.length !exp - 1)) - in + let new_branch_pc = P.of_int (!node - (List.length !exp - 1)) in liveins := PTree.set new_branch_pc lives !liveins; liveins := PTree.remove n !liveins | _ -> ()); @@ -521,6 +600,7 @@ let expanse (sb : superblock) code pm = sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; + (*print_arrayp sb.instructions;*) (*debug_flag := false;*) (!code', !pm') @@ -530,7 +610,7 @@ let rec find_last_node_reg = function let rec traverse_list var = function | [] -> () | e :: t -> - let e' = Camlcoq.P.to_int e in + let e' = p2i e in if e' > !var then var := e'; traverse_list var t in diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 4b309f5b..46d6ee73 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -96,8 +96,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsltiw _ => op1 (default nv) | OEsltiuw _ => op1 (default nv) | OExoriw _ => op1 (bitwise nv) - | OEluiw _ _ => op1 (default nv) - | OEaddiwr0 _ _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEluiw _ => op1 (default nv) + | OEaddiwr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) | OEseql _ => op2 (default nv) | OEsnel _ => op2 (default nv) | OEsequl _ => op2 (default nv) @@ -110,6 +110,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEluil _ => op1 (default nv) | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) | OEloadli _ => op1 (default nv) + | OEmayundef _ => op2 (default nv) | OEfeqd => op2 (default nv) | OEfltd => op2 (default nv) | OEfled => op2 (default nv) @@ -181,8 +181,8 @@ Inductive operation : Type := | OEsltiw (n: int) (**r set-less-than immediate *) | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) | OExoriw (n: int) (**r xor immediate *) - | OEluiw (n: int) (is_long: bool) (**r load upper-immediate *) - | OEaddiwr0 (n: int) (is_long: bool) (**r add immediate *) + | OEluiw (n: int) (**r load upper-immediate *) + | OEaddiwr0 (n: int) (**r add immediate *) | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) @@ -195,6 +195,7 @@ Inductive operation : Type := | OEluil (n: int64) (**r load upper-immediate *) | OEaddilr0 (n: int64) (**r add immediate *) | OEloadli (n: int64) (**r load an immediate int64 *) + | OEmayundef (is_long: bool) | OEfeqd (**r compare equal *) | OEfltd (**r compare less-than *) | OEfled (**r compare less-than/equal *) @@ -269,24 +270,18 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v | Some false => sem v1 vz end. -Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val := +Definition may_undef_int (is_long: bool) (v1 v2: val): val := if negb is_long then match v1 with - | Vint _ => sem vimm vz + | Vint _ => v2 | _ => Vundef end else match v1 with - | Vlong _ => sem vimm vz + | Vlong _ => v2 | _ => Vundef end. -Definition may_undef_luil (v1: val) (n: int64): val := - match v1 with - | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) - | _ => Vundef - end. - Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2 @@ -432,8 +427,8 @@ Definition eval_operation | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n)) | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) - | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12))) - | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32) + | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12))) + | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32) | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64)) | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) @@ -443,9 +438,10 @@ Definition eval_operation | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n))) | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) - | OEluil n, v1::nil => Some (may_undef_luil v1 n) - | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64) + | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) + | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64) | OEloadli n, nil => Some (Vlong n) + | OEmayundef is_long, v1::v2::nil => Some (may_undef_int is_long v1 v2) | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2) @@ -634,8 +630,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltiw _ => (Tint :: nil, Tint) | OEsltiuw _ => (Tint :: nil, Tint) | OExoriw _ => (Tint :: nil, Tint) - | OEluiw _ _ => (Tint :: nil, Tint) - | OEaddiwr0 _ _ => (Tint :: nil, Tint) + | OEluiw _ => (nil, Tint) + | OEaddiwr0 _ => (nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) | OEsnel _ => (Tlong :: Tlong :: nil, Tint) | OEsequl _ => (Tlong :: Tlong :: nil, Tint) @@ -645,9 +641,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltil _ => (Tlong :: nil, Tint) | OEsltiul _ => (Tlong :: nil, Tint) | OExoril _ => (Tlong :: nil, Tlong) - | OEluil _ => (Tlong :: nil, Tlong) - | OEaddilr0 _ => (Tlong :: nil, Tlong) + | OEluil _ => (nil, Tlong) + | OEaddilr0 _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) + | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64) | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) | OEfled => (Tfloat :: Tfloat :: nil, Tint) @@ -892,10 +889,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0... (* OEluiw *) - unfold may_undef_int; - destruct v0, is_long; simpl; trivial; destruct (Int.ltu _ _); cbn; trivial. (* OEaddiwr0 *) - - destruct v0, is_long; simpl; trivial. + - simpl; trivial. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... @@ -922,11 +918,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OExoril *) - destruct v0... (* OEluil *) - - destruct v0; simpl; trivial. + - simpl; trivial. (* OEaddilr0 *) - - destruct v0; simpl; trivial. + - simpl; trivial. (* OEloadli *) - trivial. + (* OEmayundef *) + - unfold may_undef_int; + destruct is_long, v0, v1; simpl; trivial. (* OEfeqd *) - destruct v0; destruct v1; cbn; auto. destruct Float.cmp; cbn; auto. @@ -1740,14 +1739,7 @@ Proof. (* OExoriw *) - inv H4; simpl; auto. (* OEluiw *) - - unfold may_undef_int; - destruct is_long; - inv H4; simpl; auto; - destruct (Int.ltu _ _); auto. - (* OEaddiwr0 *) - - unfold may_undef_int; - destruct is_long; - inv H4; simpl; auto. + - destruct (Int.ltu _ _); auto. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; @@ -1772,11 +1764,10 @@ Proof. - apply eval_cmplu_bool_inj; auto. (* OExoril *) - inv H4; simpl; auto. - (* OEluil *) - - inv H4; simpl; auto. - (* OEaddilr0 *) - - unfold may_undef_int; - inv H4; simpl; auto. + (* OEmayundef *) + - destruct is_long; inv H4; inv H2; + unfold may_undef_int; simpl; auto; + eapply Val.inject_ptr; eauto. (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 84380251..8ba72fb2 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -202,8 +202,8 @@ let print_operation reg pp = function | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n) - | OEluiw (n, _), _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) - | OEaddiwr0 (n, _), _ -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n) + | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) + | OEaddiwr0 n, _ -> fprintf pp "OEaddiwr0(%ld,X0)" (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) @@ -216,6 +216,7 @@ let print_operation reg pp = function | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) | OEaddilr0 n, _ -> fprintf pp "OEaddilr0(%ld,X0)" (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 | 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 diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 6a0297e9..0180c0dd 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -31,48 +31,44 @@ Definition make_lhsv_single (hvs: hsval) : list_hsval := (* Immediate loads *) -Definition load_hilo32 (hv1: hsval) (hi lo: int) (is_long: bool) := - let hl := make_lhsv_single hv1 in +Definition load_hilo32 (hi lo: int) := if Int.eq lo Int.zero then - fSop (OEluiw hi is_long) hl + fSop (OEluiw hi) fSnil else - let hvs := fSop (OEluiw hi is_long) hl in - let hl' := make_lhsv_single hvs in - fSop (Oaddimm lo) hl'. + let hvs := fSop (OEluiw hi) fSnil in + let hl := make_lhsv_single hvs in + fSop (Oaddimm lo) hl. -Definition load_hilo64 (hv1: hsval) (hi lo: int64) := - let hl := make_lhsv_single hv1 in +Definition load_hilo64 (hi lo: int64) := if Int64.eq lo Int64.zero then - fSop (OEluil hi) hl + fSop (OEluil hi) fSnil else - let hvs := fSop (OEluil hi) hl in + let hvs := fSop (OEluil hi) fSnil in let hl := make_lhsv_single hvs in fSop (Oaddlimm lo) hl. -Definition loadimm32 (hv1: hsval) (n: int) (is_long: bool) := +Definition loadimm32 (n: int) := match make_immed32 n with | Imm32_single imm => - let hl := make_lhsv_single hv1 in - fSop (OEaddiwr0 imm is_long) hl - | Imm32_pair hi lo => load_hilo32 hv1 hi lo is_long + fSop (OEaddiwr0 imm) fSnil + | Imm32_pair hi lo => load_hilo32 hi lo end. -Definition loadimm64 (hv1: hsval) (n: int64) := +Definition loadimm64 (n: int64) := match make_immed64 n with | Imm64_single imm => - let hl := make_lhsv_single hv1 in - fSop (OEaddilr0 imm) hl - | Imm64_pair hi lo => load_hilo64 hv1 hi lo + fSop (OEaddilr0 imm) fSnil + | Imm64_pair hi lo => load_hilo64 hi lo | Imm64_large imm => fSop (OEloadli imm) fSnil end. -Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) (is_long: bool) := +Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) := match make_immed32 n with | Imm32_single imm => let hl := make_lhsv_single hv1 in fSop (opimm imm) hl | Imm32_pair hi lo => - let hvs := load_hilo32 hv1 hi lo is_long in + let hvs := load_hilo32 hi lo in let hl := make_lhsv_cmp false hv1 hvs in fSop op hl end. @@ -83,7 +79,7 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper let hl := make_lhsv_single hv1 in fSop (opimm imm) hl | Imm64_pair hi lo => - let hvs := load_hilo64 hv1 hi lo in + let hvs := load_hilo64 hi lo in let hl := make_lhsv_cmp false hv1 hvs in fSop op hl | Imm64_large imm => @@ -92,9 +88,9 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper fSop op hl end. -Definition xorimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n Oxor OExoriw is_long. -Definition sltimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltw None) OEsltiw is_long. -Definition sltuimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltuw None) OEsltiuw is_long. +Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw. +Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. +Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril. Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. @@ -155,17 +151,19 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) := match cmp with | Ceq | Cne => let optR0 := make_optR0 true is_inv in - let hvs := xorimm32 hv1 n false in + let hvs := xorimm32 hv1 n in let hl := make_lhsv_cmp false hvs hvs in cond_int32s cmp hl optR0 - | Clt => sltimm32 hv1 n false + | Clt => sltimm32 hv1 n | Cle => if Int.eq n (Int.repr Int.max_signed) then - loadimm32 hv1 Int.one false - else sltimm32 hv1 (Int.add n Int.one) false + let hvs := loadimm32 Int.one in + let hl := make_lhsv_cmp false hv1 hvs in + fSop (OEmayundef false) hl + else sltimm32 hv1 (Int.add n Int.one) | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm32 hv1 n false in + let hvs := loadimm32 n in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int32s cmp hl optR0 end. @@ -178,10 +176,10 @@ Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) := cond_int32u cmp hl optR0 else match cmp with - | Clt => sltuimm32 hv1 n false + | Clt => sltuimm32 hv1 n | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm32 hv1 n false in + let hvs := loadimm32 n in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int32u cmp hl optR0 end. @@ -202,11 +200,13 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := | Clt => sltimm64 hv1 n | Cle => if Int64.eq n (Int64.repr Int64.max_signed) then - loadimm32 hv1 Int.one true + let hvs := loadimm32 Int.one in + let hl := make_lhsv_cmp false hv1 hvs in + fSop (OEmayundef true) hl else sltimm64 hv1 (Int64.add n Int64.one) | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm64 hv1 n in + let hvs := loadimm64 n in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int64s cmp hl optR0 end. @@ -222,7 +222,7 @@ Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) := | Clt => sltuimm64 hv1 n | _ => let optR0 := make_optR0 false is_inv in - let hvs := loadimm64 hv1 n in + let hvs := loadimm64 n in let hl := make_lhsv_cmp is_inv hv1 hvs in cond_int64u cmp hl optR0 end. @@ -395,7 +395,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in Some (cond, lhsv) else - let hvs := loadimm32 hv1 n false in + let hvs := loadimm32 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in Some (cond, lhsv)) @@ -407,7 +407,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in Some (cond, lhsv) else - let hvs := loadimm32 hv1 n false in + let hvs := loadimm32 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in Some (cond, lhsv)) @@ -433,7 +433,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in Some (cond, lhsv) else - let hvs := loadimm64 hv1 n in + let hvs := loadimm64 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in Some (cond, lhsv)) @@ -445,7 +445,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in Some (cond, lhsv) else - let hvs := loadimm64 hv1 n in + let hvs := loadimm64 n in let lhsv := make_lhsv_cmp is_inv hv1 hvs in let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in Some (cond, lhsv)) @@ -842,7 +842,6 @@ Proof. try rewrite OKv1; try rewrite OK2; try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; - try rewrite xor_neg_ltle_cmp; trivial; unfold Val.cmp, may_undef_int, zero32, Val.add; simpl; destruct v; auto. all: @@ -896,12 +895,12 @@ Proof. rewrite HMEM; unfold may_undef_int, Val.cmpu; destruct v; simpl; auto; - try rewrite EQIMM; try destruct (Archi.ptr64); simpl; + try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl; try rewrite ltu_12_wordsize; trivial; - try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int.add_commut, Int.add_zero_l in *; try destruct (Int.ltu _ _) eqn:EQLTU; simpl; - try rewrite EQLTU; simpl; - trivial. + try rewrite EQLTU; simpl; try rewrite EQIMM; + try rewrite EQARCH; trivial. Qed. Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall @@ -1008,12 +1007,11 @@ Proof. try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; try rewrite OK2; - unfold may_undef_luil; try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst; try fold (Val.cmpl Clt v (Vlong imm)); try rewrite xor_neg_ltge_cmpl; trivial; try rewrite xor_neg_ltle_cmpl; trivial; - unfold Val.cmpl, may_undef_luil, Val.addl; + unfold Val.cmpl, Val.addl; try rewrite xorl_zero_eq_cmpl; trivial; try rewrite optbool_mktotal; trivial; unfold may_undef_int, zero32, Val.add; simpl; @@ -1286,7 +1284,7 @@ Proof. try destruct (Int64.eq lo Int64.zero) eqn:EQLO; try apply Int.same_if_eq in EQLO; simpl; trivial; try apply Int64.same_if_eq in EQLO; simpl; trivial; - unfold may_undef_int, may_undef_luil; + unfold may_undef_int; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; simpl; trivial; try destruct v; try rewrite H; diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 97f3ff61..d50bd00f 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -27,24 +27,18 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 | Some false => sem v1 vz end. -Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval := +Definition may_undef_int (is_long: bool) (v1 v2: aval): aval := if negb is_long then match v1 with - | I _ => sem vimm vz + | I _ => v2 | _ => Ifptr Ptop end else match v1 with - | L _ => sem vimm vz + | L _ => v2 | _ => Ifptr Ptop end. -Definition may_undef_luil (v1: aval) (n: int64): aval := - match v1 with - | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | _ => Ifptr Ptop - end. - Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -223,8 +217,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) - | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12)) - | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32 + | OEluiw n, nil => shl (I n) (I (Int.repr 12)) + | OEaddiwr0 n, nil => add (I n) zero32 | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) @@ -234,9 +228,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OExoril n, v1::nil => xorl v1 (L n) - | OEluil n, v1::nil => may_undef_luil v1 n - | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64 + | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) + | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) + | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) @@ -464,14 +459,18 @@ Proof. 1,2,3: apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - unfold zero32; simpl; eauto with va. - - 1,2,11,12: - try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64; - try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1; - inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va; - try apply vmatch_ifptr_i; try apply vmatch_ifptr_l. - + + simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; + try apply vmatch_ifptr_undef. + 10: + simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; + apply vmatch_ifptr_l. + 1,10: simpl; eauto with va. + 9: + unfold Op.may_undef_int, may_undef_int; destruct is_long; + simpl; inv H0; inv H1; eauto with va; inv H; + apply vmatch_ifptr_p; eauto with va. + 3,4,6: apply eval_cmplu_sound; auto. 1,2,3: apply eval_cmpl_sound; auto. unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. |