Commit c19ecc93 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Adding a mini CSE pass in the expansion oracle

parent 3e953ef4
......@@ -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 =>
......
......@@ -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;
......
......@@ -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
......
......@@ -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;