From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 May 2020 22:04:20 +0200 Subject: k1c -> kvx changes --- kvx/ValueAOp.v | 884 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 884 insertions(+) create mode 100644 kvx/ValueAOp.v (limited to 'kvx/ValueAOp.v') diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v new file mode 100644 index 00000000..e634fdc0 --- /dev/null +++ b/kvx/ValueAOp.v @@ -0,0 +1,884 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib Compopts. +Require Import AST Integers Floats Values Memory Globalenvs. +Require Import Op ExtValues ExtFloats RTL ValueDomain. + +Definition intoffloat_total (x: aval) := + match x with + | F f => + match Float.to_int f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intuoffloat_total (x: aval) := + match x with + | F f => + match Float.to_intu f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_int f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intuofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_intu f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longoffloat_total (x: aval) := + match x with + | F f => + match Float.to_long f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longuoffloat_total (x: aval) := + match x with + | F f => + match Float.to_longu f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_long f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longuofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_longu f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition minf := binop_float ExtFloat.min. +Definition maxf := binop_float ExtFloat.max. +Definition minfs := binop_single ExtFloat32.min. +Definition maxfs := binop_single ExtFloat32.max. + +Definition ntop3 (x y z: aval) : aval := Ifptr (plub (provenance x) (plub (provenance y) (provenance z))). + +Definition triple_op_float (sem: float -> float -> float -> float) (x y z: aval) := + match x, y, z with + | F a, F b, F c => F (sem a b c) + | _, _, _ => ntop3 x y z + end. + +Definition triple_op_single (sem: float32 -> float32 -> float32 -> float32) (x y z: aval) := + match x, y, z with + | FS a, FS b, FS c => FS (sem a b c) + | _, _, _ => ntop3 x y z + end. + +Definition fmaddf := triple_op_float (fun x y z => Float.fma y z x). +Definition fmsubf := triple_op_float (fun x y z => Float.fma (Float.neg y) z x). +Definition fmaddfs := triple_op_single (fun x y z => Float32.fma y z x). +Definition fmsubfs := triple_op_single (fun x y z => Float32.fma (Float32.neg y) z x). + +Definition invfs (y : aval) := + match y with + | FS f => FS (ExtFloat32.inv f) + | _ => ntop1 y + end. + +(** Value analysis for RISC V operators *) + +Definition eval_static_condition (cond: condition) (vl: list aval): abool := + match cond, vl with + | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 + | Ccompu c, v1 :: v2 :: nil => cmpu_bool c v1 v2 + | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n) + | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n) + | Ccompl c, v1 :: v2 :: nil => cmpl_bool c v1 v2 + | Ccomplu c, v1 :: v2 :: nil => cmplu_bool c v1 v2 + | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n) + | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n) + | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2 + | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) + | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 + | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) + | _, _ => Bnone + end. + +Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := + match addr, vl with + | Aindexed n, v1::nil => offset_ptr v1 n + | Aindexed2, v1::v2::nil => addl v1 v2 + | Aindexed2XS scale, v1::v2::nil => addl v1 (shll v2 (I (Int.repr scale))) + | Aglobal s ofs, nil => Ptr (Gl s ofs) + | Ainstack ofs, nil => Ptr (Stk ofs) + | _, _ => Vbot + end. + +Definition eval_static_condition0 (cond : condition0) (v : aval) : abool := + match cond with + | Ccomp0 c => cmp_bool c v (I Int.zero) + | Ccompu0 c => cmpu_bool c v (I Int.zero) + | Ccompl0 c => cmpl_bool c v (L Int64.zero) + | Ccomplu0 c => cmplu_bool c v (L Int64.zero) + end. + + +Definition eval_static_extfs (stop : Z) (start : Z) (v : aval) := + if is_bitfield stop start + then + let stop' := Z.add stop Z.one in + match v with + | I w => + I (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + +Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := + if is_bitfield stop start + then + let stop' := Z.add stop Z.one in + match v with + | I w => + I (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + +Definition eval_static_extfsl (stop : Z) (start : Z) (v : aval) := + if is_bitfieldl stop start + then + let stop' := Z.add stop Z.one in + match v with + | L w => + L (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + +Definition eval_static_extfzl (stop : Z) (start : Z) (v : aval) := + if is_bitfieldl stop start + then + let stop' := Z.add stop Z.one in + match v with + | L w => + L (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + +Definition eval_static_insf stop start prev fld := + let mask := Int.repr (zbitfield_mask stop start) in + if is_bitfield stop start + then + match prev, fld with + | (I prevI), (I fldI) => + if Int.ltu (Int.repr start) Int.iwordsize + then I (Int.or (Int.and prevI (Int.not mask)) + (Int.and (Int.shl fldI (Int.repr start)) mask)) + else Vtop + | _, _ => Vtop + end + else Vtop. + +Definition eval_static_insfl stop start prev fld := + let mask := Int64.repr (zbitfield_mask stop start) in + if is_bitfieldl stop start + then + match prev, fld with + | (L prevL), (L fldL) => + if Int.ltu (Int.repr start) Int64.iwordsize' + then L (Int64.or (Int64.and prevL (Int64.not mask)) + (Int64.and (Int64.shl' fldL (Int.repr start)) mask)) + else Vtop + | _,_ => Vtop + end + else Vtop. + +Definition eval_static_operation (op: operation) (vl: list aval): aval := + match op, vl with + | Omove, v1::nil => v1 + | Ointconst n, nil => I n + | Olongconst n, nil => L n + | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop + | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) + | Oaddrstack ofs, nil => Ptr (Stk ofs) + | Ocast8signed, v1 :: nil => sign_ext 8 v1 + | Ocast16signed, v1 :: nil => sign_ext 16 v1 + | Oadd, v1::v2::nil => add v1 v2 + | Oaddimm n, v1::nil => add v1 (I n) + | Oaddx shift, v1::v2::nil => add v2 (shl v1 (I (int_of_shift1_4 shift))) + | Oaddximm shift n, v1::nil => add (I n) (shl v1 (I (int_of_shift1_4 shift))) + | Oneg, v1::nil => neg v1 + | Osub, v1::v2::nil => sub v1 v2 + | Orevsubx shift, v1::v2::nil => sub v2 (shl v1 (I (int_of_shift1_4 shift))) + | Orevsubimm n, v1::nil => sub (I n) v1 + | Orevsubximm shift n, v1::nil => sub (I n) (shl v1 (I (int_of_shift1_4 shift))) + | Omul, v1::v2::nil => mul v1 v2 + | Omulimm n, v1::nil => mul v1 (I n) + | Omulhs, v1::v2::nil => mulhs v1 v2 + | Omulhu, v1::v2::nil => mulhu v1 v2 + | Odiv, v1::v2::nil => divs v1 v2 + | Odivu, v1::v2::nil => divu v1 v2 + | Omod, v1::v2::nil => mods v1 v2 + | Omodu, v1::v2::nil => modu v1 v2 + | Oand, v1::v2::nil => and v1 v2 + | Oandimm n, v1::nil => and v1 (I n) + | Onand, v1::v2::nil => notint (and v1 v2) + | Onandimm n, v1::nil => notint (and v1 (I n)) + | Oor, v1::v2::nil => or v1 v2 + | Oorimm n, v1::nil => or v1 (I n) + | Onor, v1::v2::nil => notint (or v1 v2) + | Onorimm n, v1::nil => notint (or v1 (I n)) + | Oxor, v1::v2::nil => xor v1 v2 + | Oxorimm n, v1::nil => xor v1 (I n) + | Onxor, v1::v2::nil => notint (xor v1 v2) + | Onxorimm n, v1::nil => notint (xor v1 (I n)) + | Onot, v1::nil => notint v1 + | Oandn, v1::v2::nil => and (notint v1) v2 + | Oandnimm n, v1::nil => and (notint v1) (I n) + | Oorn, v1::v2::nil => or (notint v1) v2 + | Oornimm n, v1::nil => or (notint v1) (I n) + | Oshl, v1::v2::nil => shl v1 v2 + | Oshlimm n, v1::nil => shl v1 (I n) + | Oshr, v1::v2::nil => shr v1 v2 + | Oshrimm n, v1::nil => shr v1 (I n) + | Ororimm n, v1::nil => ror v1 (I n) + | Oshru, v1::v2::nil => shru v1 v2 + | Oshruimm n, v1::nil => shru v1 (I n) + | Oshrximm n, v1::nil => shrx v1 (I n) + | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3) + | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n)) + | Omsub, v1::v2::v3::nil => sub v1 (mul v2 v3) + | Omakelong, v1::v2::nil => longofwords v1 v2 + | Olowlong, v1::nil => loword v1 + | Ohighlong, v1::nil => hiword v1 + | Ocast32signed, v1::nil => longofint v1 + | Ocast32unsigned, v1::nil => longofintu v1 + | Oaddl, v1::v2::nil => addl v1 v2 + | Oaddlimm n, v1::nil => addl v1 (L n) + | Oaddxl shift, v1::v2::nil => addl v2 (shll v1 (I (int_of_shift1_4 shift))) + | Oaddxlimm shift n, v1::nil => addl (L n) (shll v1 (I (int_of_shift1_4 shift))) + | Onegl, v1::nil => negl v1 + | Osubl, v1::v2::nil => subl v1 v2 + | Orevsubxl shift, v1::v2::nil => subl v2 (shll v1 (I (int_of_shift1_4 shift))) + | Orevsublimm n, v1::nil => subl (L n) v1 + | Orevsubxlimm shift n, v1::nil => subl (L n) (shll v1 (I (int_of_shift1_4 shift))) + | Omull, v1::v2::nil => mull v1 v2 + | Omullimm n, v1::nil => mull v1 (L n) + | Omullhs, v1::v2::nil => mullhs v1 v2 + | Omullhu, v1::v2::nil => mullhu v1 v2 + | Odivl, v1::v2::nil => divls v1 v2 + | Odivlu, v1::v2::nil => divlu v1 v2 + | Omodl, v1::v2::nil => modls v1 v2 + | Omodlu, v1::v2::nil => modlu v1 v2 + | Oandl, v1::v2::nil => andl v1 v2 + | Oandlimm n, v1::nil => andl v1 (L n) + | Onandl, v1::v2::nil => notl (andl v1 v2) + | Onandlimm n, v1::nil => notl (andl v1 (L n)) + | Oorl, v1::v2::nil => orl v1 v2 + | Oorlimm n, v1::nil => orl v1 (L n) + | Onorl, v1::v2::nil => notl (orl v1 v2) + | Onorlimm n, v1::nil => notl (orl v1 (L n)) + | Oxorl, v1::v2::nil => xorl v1 v2 + | Oxorlimm n, v1::nil => xorl v1 (L n) + | Onxorl, v1::v2::nil => notl (xorl v1 v2) + | Onxorlimm n, v1::nil => notl (xorl v1 (L n)) + | Onotl, v1::nil => notl v1 + | Oandnl, v1::v2::nil => andl (notl v1) v2 + | Oandnlimm n, v1::nil => andl (notl v1) (L n) + | Oornl, v1::v2::nil => orl (notl v1) v2 + | Oornlimm n, v1::nil => orl (notl v1) (L n) + | Oshll, v1::v2::nil => shll v1 v2 + | Oshllimm n, v1::nil => shll v1 (I n) + | Oshrl, v1::v2::nil => shrl v1 v2 + | Oshrlimm n, v1::nil => shrl v1 (I n) + | Oshrlu, v1::v2::nil => shrlu v1 v2 + | Oshrluimm n, v1::nil => shrlu v1 (I n) + | Oshrxlimm n, v1::nil => shrxl v1 (I n) + | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3) + | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n)) + | Omsubl, v1::v2::v3::nil => subl v1 (mull v2 v3) + | Onegf, v1::nil => negf v1 + | Oabsf, v1::nil => absf v1 + | Oaddf, v1::v2::nil => addf v1 v2 + | Osubf, v1::v2::nil => subf v1 v2 + | Omulf, v1::v2::nil => mulf v1 v2 + | Odivf, v1::v2::nil => divf v1 v2 + | Ominf, v1::v2::nil => minf v1 v2 + | Omaxf, v1::v2::nil => maxf v1 v2 + | Ofmaddf, v1::v2::v3::nil => fmaddf v1 v2 v3 + | Ofmsubf, v1::v2::v3::nil => fmsubf v1 v2 v3 + | Onegfs, v1::nil => negfs v1 + | Oabsfs, v1::nil => absfs v1 + | Oaddfs, v1::v2::nil => addfs v1 v2 + | Osubfs, v1::v2::nil => subfs v1 v2 + | Omulfs, v1::v2::nil => mulfs v1 v2 + | Odivfs, v1::v2::nil => divfs v1 v2 + | Ominfs, v1::v2::nil => minfs v1 v2 + | Omaxfs, v1::v2::nil => maxfs v1 v2 + | Oinvfs, v1::nil => invfs v1 + | Ofmaddfs, v1::v2::v3::nil => fmaddfs v1 v2 v3 + | Ofmsubfs, v1::v2::v3::nil => fmsubfs v1 v2 v3 + | Osingleoffloat, v1::nil => singleoffloat v1 + | Ofloatofsingle, v1::nil => floatofsingle v1 + | Ointoffloat, v1::nil => intoffloat_total v1 + | Ointuoffloat, v1::nil => intuoffloat_total v1 + | Ointofsingle, v1::nil => intofsingle_total v1 + | Ointuofsingle, v1::nil => intuofsingle_total v1 + | Osingleofint, v1::nil => singleofint v1 + | Osingleofintu, v1::nil => singleofintu v1 + | Olongoffloat, v1::nil => longoffloat_total v1 + | Olonguoffloat, v1::nil => longuoffloat_total v1 + | Ofloatoflong, v1::nil => floatoflong v1 + | Ofloatoflongu, v1::nil => floatoflongu v1 + | Olongofsingle, v1::nil => longofsingle_total v1 + | Olonguofsingle, v1::nil => longuofsingle_total v1 + | Osingleoflong, v1::nil => singleoflong v1 + | Osingleoflongu, v1::nil => singleoflongu v1 + | Ocmp c, _ => of_optbool (eval_static_condition c vl) + | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0 + | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0 + | (Oextfzl stop start), v0::nil => eval_static_extfzl stop start v0 + | (Oextfsl stop start), v0::nil => eval_static_extfsl stop start v0 + | (Oinsf stop start), v0::v1::nil => eval_static_insf stop start v0 v1 + | (Oinsfl stop start), v0::v1::nil => eval_static_insfl stop start v0 v1 + | Osel c ty, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 v2 + | Oselimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (I imm) + | Osellimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (L imm) + | _, _ => Vbot + end. + +Section SOUNDNESS. + +Variable bc: block_classification. +Variable ge: genv. +Hypothesis GENV: genv_match bc ge. +Variable sp: block. +Hypothesis STACK: bc sp = BCstack. + +Lemma intoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x). +Proof. + unfold Val.intoffloat, intoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intoffloat_total_sound : va. + +Lemma intuoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x). +Proof. + unfold Val.intoffloat, intoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intuoffloat_total_sound : va. + +Lemma intofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x). +Proof. + unfold Val.intofsingle, intofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intofsingle_total_sound : va. + +Lemma intuofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x). +Proof. + unfold Val.intofsingle, intofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intuofsingle_total_sound : va. + +Lemma singleofint_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x). +Proof. + unfold Val.singleofint, singleofint; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleofint_total_sound : va. + +Lemma singleofintu_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x). +Proof. + unfold Val.singleofintu, singleofintu; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleofintu_total_sound : va. + +Lemma longoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x). +Proof. + unfold Val.longoffloat, longoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longoffloat_total_sound : va. + +Lemma longuoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x). +Proof. + unfold Val.longoffloat, longoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longuoffloat_total_sound : va. + +Lemma longofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x). +Proof. + unfold Val.longofsingle, longofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longofsingle_total_sound : va. + +Lemma longuofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x). +Proof. + unfold Val.longofsingle, longofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longuofsingle_total_sound : va. + +Lemma singleoflong_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x). +Proof. + unfold Val.singleoflong, singleoflong; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleoflong_total_sound : va. + +Lemma singleoflongu_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x). +Proof. + unfold Val.singleoflongu, singleoflongu; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleoflongu_total_sound : va. + +Lemma floatoflong_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x). +Proof. + unfold Val.floatoflong, floatoflong; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve floatoflong_total_sound : va. + +Lemma floatoflongu_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x). +Proof. + unfold Val.floatoflongu, floatoflongu; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve floatoflongu_total_sound : va. + +Lemma minf_sound: + forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). +Proof. + apply (binop_float_sound bc ExtFloat.min); assumption. +Qed. + +Lemma maxf_sound: + forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.maxf v w) (maxf x y). +Proof. + apply (binop_float_sound bc ExtFloat.max); assumption. +Qed. + +Lemma minfs_sound: + forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minfs v w) (minfs x y). +Proof. + apply (binop_single_sound bc ExtFloat32.min); assumption. +Qed. + +Lemma maxfs_sound: + forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.maxfs v w) (maxfs x y). +Proof. + apply (binop_single_sound bc ExtFloat32.max); assumption. +Qed. + +Lemma invfs_sound: + forall v x, vmatch bc v x -> vmatch bc (ExtValues.invfs v) (invfs x). +Proof. + intros v x; + intro MATCH; + inversion MATCH; + simpl; + constructor. +Qed. + +Lemma triple_op_float_sound: + forall f a x b y c z, + vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.triple_op_float f a b c) + (triple_op_float f x y z). +Proof. + intros until z. + intros Hax Hby Hcz. + inv Hax; simpl; try constructor; + inv Hby; simpl; try constructor; + inv Hcz; simpl; try constructor. +Qed. + +Lemma triple_op_single_sound: + forall f a x b y c z, + vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.triple_op_single f a b c) + (triple_op_single f x y z). +Proof. + intros until z. + intros Hax Hby Hcz. + inv Hax; simpl; try constructor; + inv Hby; simpl; try constructor; + inv Hcz; simpl; try constructor. +Qed. + +Lemma fmaddf_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmaddf a b c) (fmaddf x y z). +Proof. + intros. unfold ExtValues.fmaddf, fmaddf. + apply triple_op_float_sound; assumption. +Qed. + +Lemma fmaddfs_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmaddfs a b c) (fmaddfs x y z). +Proof. + intros. unfold ExtValues.fmaddfs, fmaddfs. + apply triple_op_single_sound; assumption. +Qed. + +Lemma fmsubf_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmsubf a b c) (fmsubf x y z). +Proof. + intros. unfold ExtValues.fmsubf, fmsubf. + apply triple_op_float_sound; assumption. +Qed. + +Lemma fmsubfs_sound : + forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z -> + vmatch bc (ExtValues.fmsubfs a b c) (fmsubfs x y z). +Proof. + intros. unfold ExtValues.fmsubfs, fmsubfs. + apply triple_op_single_sound; assumption. +Qed. +Hint Resolve minf_sound maxf_sound minfs_sound maxfs_sound invfs_sound fmaddf_sound fmaddfs_sound fmsubf_sound fmsubfs_sound : va. + +Theorem eval_static_condition_sound: + forall cond vargs m aargs, + list_forall2 (vmatch bc) vargs aargs -> + cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs). +Proof. + intros until aargs; intros VM. inv VM. + destruct cond; auto with va. + inv H0. + destruct cond; simpl; eauto with va. + inv H2. + destruct cond; simpl; eauto with va. + destruct cond; auto with va. +Qed. + +Theorem eval_static_condition0_sound: + forall cond varg m aarg, + vmatch bc varg aarg -> + cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg). +Proof. + intros until aarg; intro VM. + destruct cond; simpl; eauto with va. +Qed. + +Lemma symbol_address_sound: + forall id ofs, + vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)). +Proof. + intros; apply symbol_address_sound; apply GENV. +Qed. + +Lemma symbol_address_sound_2: + forall id ofs, + vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + constructor. constructor. apply GENV; auto. + constructor. +Qed. + +Hint Resolve symbol_address_sound symbol_address_sound_2: va. + +Ltac InvHyps := + match goal with + | [H: None = Some _ |- _ ] => discriminate + | [H: Some _ = Some _ |- _] => inv H + | [H1: match ?vl with nil => _ | _ :: _ => _ end = Some _ , + H2: list_forall2 _ ?vl _ |- _ ] => inv H2; InvHyps + | [H: (if Archi.ptr64 then _ else _) = Some _ |- _] => destruct Archi.ptr64 eqn:?; InvHyps + | _ => idtac + end. + +Theorem eval_static_addressing_sound: + forall addr vargs vres aargs, + eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = Some vres -> + list_forall2 (vmatch bc) vargs aargs -> + vmatch bc vres (eval_static_addressing addr aargs). +Proof. + unfold eval_addressing, eval_static_addressing; intros; + destruct addr; InvHyps; eauto with va. + rewrite Ptrofs.add_zero_l; eauto with va. +Qed. + +Theorem eval_static_addressing_sound_none: + forall addr vargs aargs, + eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = None -> + list_forall2 (vmatch bc) vargs aargs -> + (eval_static_addressing addr aargs) = Vbot. +Proof. + unfold eval_addressing, eval_static_addressing. + intros until aargs. intros Heval_none Hlist. + inv Hlist. + destruct addr; trivial; discriminate. + inv H0. + destruct addr; trivial; discriminate. + inv H2. + destruct addr; trivial; discriminate. + inv H3; + destruct addr; trivial; discriminate. +Qed. + +Lemma vmatch_vint_ntop1: + forall x y, vmatch bc (Vint x) (ntop1 y). +Proof. + intro. unfold ntop1, provenance. + destruct y; + destruct (va_strict tt); + constructor. +Qed. + +Lemma vmatch_vlong_ntop1: + forall x y, vmatch bc (Vlong x) (ntop1 y). +Proof. + intro. unfold ntop1, provenance. + destruct y; + destruct (va_strict tt); + constructor. +Qed. + +Hint Resolve vmatch_vint_ntop1 vmatch_vlong_ntop1: va. + +Theorem eval_static_operation_sound: + forall op vargs m vres aargs, + eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres -> + list_forall2 (vmatch bc) vargs aargs -> + vmatch bc vres (eval_static_operation op aargs). +Proof. + unfold eval_operation, eval_static_operation, addx, revsubx, addxl, revsubxl; intros. + destruct op; InvHyps; eauto with va. + - destruct (propagate_float_constants tt); constructor. + - destruct (propagate_float_constants tt); constructor. + - rewrite Ptrofs.add_zero_l; eauto with va. + - replace(match Val.shl a1 (Vint (int_of_shift1_4 shift)) with + | Vint n2 => Vint (Int.add n n2) + | Vptr b2 ofs2 => + if Archi.ptr64 + then Vundef + else Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int n)) + | _ => Vundef + end) with (Val.add (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct a1; destruct shift; reflexivity. + - (*revsubimm*) inv H1; constructor. + - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with + | Vint n2 => Vint (Int.sub n n2) + | _ => Vundef + end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct n; destruct shift; reflexivity. + - (* shrx *) + inv H1; simpl; try constructor. + all: destruct Int.ltu; [simpl | constructor; fail]. + all: auto with va. + - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with + | Vlong n2 => Vlong (Int64.add n n2) + | Vptr b2 ofs2 => + if Archi.ptr64 + then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n)) + else Vundef + | _ => Vundef + end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct a1; destruct shift; reflexivity. + - inv H1; constructor. + - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with + | Vlong n2 => Vlong (Int64.sub n n2) + | _ => Vundef + end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct a1; destruct shift; reflexivity. + - (* shrxl *) + inv H1; simpl; try constructor. + all: destruct Int.ltu; [simpl | constructor; fail]. + all: auto with va. + - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + + (* extfz *) + - unfold extfz, eval_static_extfz. + destruct (is_bitfield _ _). + + inv H1; constructor. + + constructor. + + (* extfs *) + - unfold extfs, eval_static_extfs. + destruct (is_bitfield _ _). + + inv H1; constructor. + + constructor. + + (* extfzl *) + - unfold extfzl, eval_static_extfzl. + destruct (is_bitfieldl _ _). + + inv H1; constructor. + + constructor. + + (* extfsl *) + - unfold extfsl, eval_static_extfsl. + destruct (is_bitfieldl _ _). + + inv H1; constructor. + + constructor. + + (* insf *) + - unfold insf, eval_static_insf. + destruct (is_bitfield _ _). + + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + constructor. + (* insfl *) + - unfold insfl, eval_static_insfl. + destruct (is_bitfieldl _ _). + + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + constructor. + (* select *) + - apply select_sound; auto. eapply eval_static_condition0_sound; eauto. + (* select imm *) + - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. + (* select long imm *) + - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto. +Qed. + +End SOUNDNESS. + -- cgit