From compcert Require Import lib.Integers.
From compcert Require Import lib.Floats.
From Velus Require Import Common.
From Velus Require Import Common.CompCertLib.
From Velus Require Import Operators.
From Velus Require Import Ident.
From compcert Require common.Values.
From compcert Require cfrontend.Cop.
From compcert Require cfrontend.Ctypes.
From compcert Require cfrontend.Ctyping.
From compcert Require cfrontend.ClightBigstep.
From compcert Require common.Memory.
From compcert Require common.Memdata.
From compcert Require lib.Maps.
From Coq Require Import String.
From Coq Require Import ZArith.BinInt.
Import List.ListNotations.
Open Scope list_scope.
Open Scope bool_scope.
Global Hint Resolve Z.divide_refl :
core.
Definition empty_composite_env :
Ctypes.composite_env := (
Maps.PTree.empty _).
Module Export Op <:
OPERATORS.
Definition cvalue:
Type :=
Values.val.
Inductive ctype' :
Type :=
|
Tint:
Ctypes.intsize ->
Ctypes.signedness ->
ctype'
|
Tlong:
Ctypes.signedness ->
ctype'
|
Tfloat:
Ctypes.floatsize ->
ctype'.
Definition ctype :=
ctype'.
Definition cltype (
ty:
ctype) :
Ctypes.type :=
match ty with
|
Tint sz sg =>
Ctypes.Tint sz sg Ctypes.noattr
|
Tlong sg =>
Ctypes.Tlong sg (
Ctypes.mk_attr false (
Some (
Npos 3)))
|
Tfloat sz =>
Ctypes.Tfloat sz Ctypes.noattr
end.
Definition typecl (
ty:
Ctypes.type) :
option ctype :=
match ty with
|
Ctypes.Tint sz sg attr =>
Some (
Tint sz sg)
|
Ctypes.Tlong sg attr =>
Some (
Tlong sg)
|
Ctypes.Tfloat sz attr =>
Some (
Tfloat sz)
| _ =>
None
end.
Definition type_chunk (
ty:
ctype) :
AST.memory_chunk :=
match ty with
|
Tint Ctypes.I8 Ctypes.Signed =>
AST.Mint8signed
|
Tint Ctypes.I8 Ctypes.Unsigned =>
AST.Mint8unsigned
|
Tint Ctypes.I16 Ctypes.Signed =>
AST.Mint16signed
|
Tint Ctypes.I16 Ctypes.Unsigned =>
AST.Mint16unsigned
|
Tint Ctypes.I32 _ =>
AST.Mint32
|
Tint Ctypes.IBool _ =>
AST.Mbool
|
Tlong _ =>
AST.Mint64
|
Tfloat Ctypes.F32 =>
AST.Mfloat32
|
Tfloat Ctypes.F64 =>
AST.Mfloat64
end.
Lemma cltype_align:
forall gcenv ty,
(
Memdata.align_chunk (
type_chunk ty) |
Ctypes.alignof gcenv (
cltype ty))%
Z.
Proof.
Lemma cltype_access_by_value:
forall ty,
Ctypes.access_mode (
cltype ty) =
Ctypes.By_value (
type_chunk ty).
Proof.
destruct ty; simpl; cases.
Qed.
Lemma sizeof_cltype_chunk:
forall gcenv t,
Ctypes.sizeof gcenv (
cltype t) =
Memdata.size_chunk (
type_chunk t).
Proof.
Inductive constant :
Type :=
|
Cint:
Integers.int ->
Ctypes.intsize ->
Ctypes.signedness ->
constant
|
Clong:
Integers.int64 ->
Ctypes.signedness ->
constant
|
Cfloat:
Floats.float ->
constant
|
Csingle:
Floats.float32 ->
constant.
Definition cconst :=
constant.
Definition enumtag :=
nat.
Definition enumtag_to_int (
c:
enumtag) :
int :=
Int.repr (
Z.of_nat c).
Inductive value :=
|
Vscalar :
cvalue ->
value
|
Venum :
enumtag ->
value.
Inductive type :=
|
Tprimitive :
ctype ->
type
|
Tenum :
ident ->
list ident ->
type.
Inductive const :=
|
Const:
cconst ->
const
|
Enum :
enumtag ->
const.
Definition ctype_cconst (
c:
cconst) :
ctype :=
match c with
|
Cint _
sz sg =>
Tint sz sg
|
Clong _
sg =>
Tlong sg
|
Cfloat _ =>
Tfloat Ctypes.F64
|
Csingle _ =>
Tfloat Ctypes.F32
end.
Definition sem_cconst (
c:
cconst) :
cvalue :=
match c with
|
Cint i sz sg =>
Values.Vint (
Cop.cast_int_int sz sg i)
|
Clong i sg =>
Values.Vlong i
|
Cfloat f =>
Values.Vfloat f
|
Csingle f =>
Values.Vsingle f
end.
Definition init_ctype (
ty:
ctype) :
cconst :=
match ty with
|
Tint sz sg =>
Cint Integers.Int.zero sz sg
|
Tlong sg =>
Clong Integers.Int64.zero sg
|
Tfloat Ctypes.F64 =>
Cfloat Floats.Float.zero
|
Tfloat Ctypes.F32 =>
Csingle Floats.Float32.zero
end.
Inductive unop' :
Type :=
|
UnaryOp:
Cop.unary_operation ->
unop'
|
CastOp:
ctype ->
unop'.
Definition unop :=
unop'.
Definition binop :=
Cop.binary_operation.
Open Scope nat_scope.
Definition intsize_of_enumtag (
n:
enumtag):
Ctypes.intsize :=
if n <=? 2 ^ 8
then Ctypes.I8
else if n <=? 2 ^ 16
then Ctypes.I16
else Ctypes.I32.
Definition enumtag_ctype (
n:
nat) :
ctype :=
Tint (
intsize_of_enumtag n)
Ctypes.Unsigned.
Definition sem_unop_bool (
uop:
unop) (
c:
enumtag) :
option enumtag :=
match uop with
|
UnaryOp op =>
match op with
|
Cop.Onotbool =>
match c with
| 0 =>
Some 1
| 1 =>
Some 0
| _ =>
None
end
| _ =>
None
end
|
CastOp _ =>
None
end.
Definition sem_unop (
uop:
unop) (
v:
value) (
ty:
type) :
option value :=
match v,
ty with
|
Vscalar v,
Tprimitive ty =>
option_map Vscalar
match uop with
|
UnaryOp op =>
Cop.sem_unary_operation op v (
cltype ty)
Memory.Mem.empty
|
CastOp ty' =>
Cop.sem_cast v (
cltype ty) (
cltype ty')
Memory.Mem.empty
end
|
Venum c,
Tenum t _ =>
if t ==
b bool_id
then option_map Venum (
sem_unop_bool uop c)
else None
| _, _ =>
None
end.
Definition truth_table (
c1 c2:
enumtag) (
c00 c10 c01 c11:
enumtag):
option enumtag :=
match c1,
c2 with
| 0, 0 =>
Some c00
| 1, 0 =>
Some c10
| 0, 1 =>
Some c01
| 1, 1 =>
Some c11
| _, _ =>
None
end.
Definition sem_binop_bool (
bop:
binop) (
c1 c2:
enumtag) :
option enumtag :=
match bop with
|
Cop.Oand =>
truth_table c1 c2 0 0 0 1
|
Cop.Oor =>
truth_table c1 c2 0 1 1 1
|
Cop.Oxor =>
truth_table c1 c2 0 1 1 0
|
Cop.Oeq =>
truth_table c1 c2 1 0 0 1
|
Cop.One =>
truth_table c1 c2 0 1 1 0
|
Cop.Olt =>
truth_table c1 c2 0 0 1 0
|
Cop.Ogt =>
truth_table c1 c2 0 1 0 0
|
Cop.Ole =>
truth_table c1 c2 1 0 1 1
|
Cop.Oge =>
truth_table c1 c2 1 1 0 1
| _ =>
None
end.
Definition enumtag_of_cvalue (
v:
cvalue) :
enumtag :=
match v with
|
Values.Vundef
|
Values.Vlong _
|
Values.Vfloat _
|
Values.Vsingle _
|
Values.Vptr _ _ => 0%
nat
|
Values.Vint n =>
Z.to_nat (
Int.unsigned n)
end.
Definition binop_always_returns_bool (
op:
binop) :
bool :=
match op with
|
Cop.Oeq
|
Cop.One
|
Cop.Olt
|
Cop.Ogt
|
Cop.Ole
|
Cop.Oge =>
true
| _ =>
false
end.
Definition binop_sometimes_returns_bool (
op:
binop) :
bool :=
match op with
|
Cop.Oand
|
Cop.Oor
|
Cop.Oxor
|
Cop.Oeq
|
Cop.One
|
Cop.Olt
|
Cop.Ogt
|
Cop.Ole
|
Cop.Oge =>
true
| _ =>
false
end.
Definition sem_binop (
bop:
binop) (
v1:
value) (
ty1:
type)
(
v2:
value) (
ty2:
type) :
option value :=
match v1,
ty1,
v2,
ty2 with
|
Vscalar v1,
Tprimitive ty1,
Vscalar v2,
Tprimitive ty2 =>
let v' :=
Cop.sem_binary_operation empty_composite_env
bop v1 (
cltype ty1)
v2 (
cltype ty2)
Memory.Mem.empty
in
if binop_always_returns_bool bop
then option_map Venum (
option_map enumtag_of_cvalue v')
else option_map Vscalar v'
|
Venum c1,
Tenum t1 _,
Venum c2,
Tenum t2 _ =>
if (
t1 ==
b bool_id) && (
t2 ==
b bool_id)
then option_map Venum (
sem_binop_bool bop c1 c2)
else match bop with
|
Cop.Oeq =>
Some (
Venum (
if Int.eq (
enumtag_to_int c1) (
enumtag_to_int c2)
then 1
else 0))
|
Cop.One =>
Some (
Venum (
if Int.eq (
enumtag_to_int c1) (
enumtag_to_int c2)
then 0
else 1))
| _ =>
None
end
| _, _, _, _ =>
None
end.
Definition bool_type :=
Tenum bool_id [
false_id;
true_id].
Definition type_unop (
uop:
unop) (
ty:
type) :
option type :=
match ty with
|
Tprimitive ty =>
match uop with
|
UnaryOp op =>
match Ctyping.type_unop op (
cltype ty)
with
|
Errors.OK ty' =>
option_map Tprimitive (
typecl ty')
|
Errors.Error _ =>
None
end
|
CastOp ty' =>
match Ctyping.check_cast (
cltype ty) (
cltype ty')
with
|
Errors.OK _ =>
Some (
Tprimitive ty')
|
Errors.Error _ =>
None
end
end
|
Tenum tx tn =>
if (
tx ==
b bool_id) && (
List.length tn =? 2)
then
match uop with
|
UnaryOp Cop.Onotbool =>
Some bool_type
| _ =>
None
end
else None
end.
Definition type_binop (
bop:
binop) (
ty1 ty2:
type) :
option type :=
match ty1,
ty2 with
|
Tprimitive ty1,
Tprimitive ty2 =>
if binop_always_returns_bool bop then Some bool_type
else match Ctyping.type_binop bop (
cltype ty1) (
cltype ty2)
with
|
Errors.OK ty' =>
option_map Tprimitive (
typecl ty')
|
Errors.Error _ =>
None
end
|
Tenum t1 tn1,
Tenum t2 tn2 =>
if (
t1 ==
b bool_id) && (
t2 ==
b bool_id) && (
binop_sometimes_returns_bool bop)
then
if (
List.length tn1 =? 2) && (
List.length tn2 =? 2)
then Some bool_type
else None
else match bop with
|
Cop.Oeq =>
Some bool_type
|
Cop.One =>
Some bool_type
| _ =>
None
end
| _, _ =>
None
end.
Inductive wt_cvalue' :
cvalue ->
ctype ->
Prop :=
|
wt_cvalue_int:
forall n sz sg,
Ctyping.wt_int n sz sg ->
(
sz =
Ctypes.IBool -> (
n =
Int.zero \/
n =
Int.one)) ->
wt_cvalue' (
Values.Vint n) (
Tint sz sg)
|
wt_cvalue_long:
forall n sg,
wt_cvalue' (
Values.Vlong n) (
Tlong sg)
|
wt_cvalue_float:
forall f,
wt_cvalue' (
Values.Vfloat f) (
Tfloat Ctypes.F64)
|
wt_cvalue_single:
forall f,
wt_cvalue' (
Values.Vsingle f) (
Tfloat Ctypes.F32).
Definition wt_cvalue :
cvalue ->
ctype ->
Prop :=
wt_cvalue'.
Global Hint Unfold wt_cvalue :
typing.
Global Hint Constructors wt_cvalue' :
typing.
Lemma wt_cvalue_cconst:
forall c,
wt_cvalue (
sem_cconst c) (
ctype_cconst c).
Proof.
Lemma wt_init_ctype:
forall ty,
wt_cvalue (
sem_cconst (
init_ctype ty))
ty.
Proof.
Lemma ctype_init_ctype:
forall ty,
ctype_cconst (
init_ctype ty) =
ty.
Proof.
destruct ty; auto.
destruct f; auto.
Qed.
Ltac DestructCases :=
match goal with
|
H: ?
x <> ?
x |- _ =>
now contradiction H
| _ =>
Ctyping.DestructCases
end.
Definition good_bool (
v:
Values.val) (
ty:
Ctypes.type) :=
match ty,
v with
|
Ctypes.Tint Ctypes.IBool sg a,
Values.Vint v =>
(
v =
Int.zero \/
v =
Int.one)
| _, _ =>
True
end.
Lemma wt_cvalue_good_bool:
forall v ty,
wt_cvalue v ty ->
good_bool v (
cltype ty).
Proof.
intros *
WTv.
unfold good_bool.
inv WTv;
simpl;
auto.
match goal with H:
sz =
Ctypes.IBool -> _ |- _ =>
destruct sz;
auto;
destruct H;
subst;
auto
end.
Qed.
Lemma good_bool_not_bool:
forall v ty,
(
forall sg a,
ty <>
Ctypes.Tint Ctypes.IBool sg a) ->
good_bool v ty.
Proof.
intros v ty Hty.
destruct ty; simpl; eauto.
destruct i, v; auto.
now contradiction (Hty s a).
Qed.
Local Hint Resolve good_bool_not_bool :
core.
Lemma good_bool_zero_or_one:
forall i sz sg a,
good_bool (
Values.Vint i) (
Ctypes.Tint sz sg a) ->
sz =
Ctypes.IBool ->
i =
Int.zero \/
i =
Int.one.
Proof.
intros * Hgb Hsz; subst; inversion_clear Hgb; auto.
Qed.
Lemma typecl_wt_val_wt_cvalue:
forall cty ty v,
typecl cty =
Some ty ->
Ctyping.wt_val v cty ->
v <>
Values.Vundef ->
(
forall b ofs,
v <>
Values.Vptr b ofs) ->
good_bool v cty ->
wt_cvalue v ty.
Proof.
intros * Htcl Hcty Hnun Hnptr Hgb.
inv Hcty; inv Htcl; simpl in *; eauto with typing;
try contradiction; try discriminate.
- constructor; auto.
intros; subst; auto.
- exfalso; now eapply Hnptr.
Qed.
Lemma wt_cvalue_not_vundef_nor_vptr:
forall v ty,
wt_cvalue v ty ->
v <>
Values.Vundef /\ (
forall b ofs,
v <>
Values.Vptr b ofs).
Proof.
intros * Hwt.
destruct ty; inversion Hwt; subst;
split; discriminate.
Qed.
Lemma wt_cvalue_wt_val_cltype:
forall v ty,
wt_cvalue v ty ->
Ctyping.wt_val v (
cltype ty).
Proof.
intros *
Hwt.
destruct ty;
inversion_clear Hwt;
eauto using Ctyping.wt_val.
Qed.
Lemma type_castop:
forall ty ty',
type_unop (
CastOp ty') (
Tprimitive ty) =
Some (
Tprimitive ty').
Proof.
intros ty ty'.
destruct ty, ty';
try destruct i, s; try destruct i0; try destruct s0;
try destruct f; try destruct f0; auto.
Qed.
Ltac GoalMatchMatch :=
repeat match goal with
| |-
match match ?
x with _ => _
end with _ => _
end = _ =>
destruct x
end;
auto.
Lemma check_cltype_cast:
forall ty ty',
Ctyping.check_cast (
cltype ty) (
cltype ty') =
Errors.OK tt.
Proof.
Inductive wt_value:
value ->
type ->
Prop :=
|
WTVScalarPrimitive:
forall v t,
wt_cvalue v t ->
wt_value (
Vscalar v) (
Tprimitive t)
|
WTVEnum:
forall v tx tn,
v <
List.length tn ->
wt_value (
Venum v) (
Tenum tx tn).
Lemma typecl_cltype:
forall t,
typecl (
cltype t) =
Some t.
Proof.
now destruct t.
Qed.
Lemma pres_sem_unop:
forall op ty1 ty v1 v,
type_unop op ty1 =
Some ty ->
sem_unop op v1 ty1 =
Some v ->
wt_value v1 ty1 ->
wt_value v ty.
Proof.
Lemma sem_cast_same:
forall m v t,
wt_cvalue v t ->
Cop.sem_cast v (
cltype t) (
cltype t)
m =
Some v.
Proof.
Ltac ContradictNotVptr :=
match goal with
|
H:
context [
Values.Vptr ?
b ?
i <>
Values.Vptr _ _] |- _ =>
contradiction (
H b i)
end.
Lemma cases_of_bool:
forall P b,
P Values.Vtrue ->
P Values.Vfalse ->
P (
Values.Val.of_bool b).
Proof.
destruct b; auto.
Qed.
Lemma option_map_of_bool_true_false:
forall e x,
Coqlib.option_map Values.Val.of_bool e =
Some x ->
x =
Values.Vtrue \/
x =
Values.Vfalse.
Proof.
intros e x Hom.
destruct e as [b|]; [destruct b|].
- injection Hom; intro; subst; auto with *.
- injection Hom; intro; subst; auto with *.
- discriminate Hom.
Qed.
Lemma sem_cmp_not_vundef_nor_vptr:
forall cop v1 ty1 v2 ty2 m v,
Cop.sem_cmp cop v1 ty1 v2 ty2 m =
Some v ->
v <>
Values.Vundef /\ (
forall b ofs,
v <>
Values.Vptr b ofs).
Proof.
Lemma classify_add_cltypes:
forall ty1 ty2,
Cop.classify_add (
cltype ty1) (
cltype ty2) =
Cop.add_default.
Proof.
Lemma classify_sub_cltypes:
forall ty1 ty2,
Cop.classify_sub (
cltype ty1) (
cltype ty2) =
Cop.sub_default.
Proof.
Lemma classify_cmp_cltypes:
forall ty1 ty2,
Cop.classify_cmp (
cltype ty1) (
cltype ty2) =
Cop.cmp_default.
Proof.
Lemma sem_cmp_true_or_false:
forall cop v1 ty1 v2 ty2 m v,
Cop.sem_cmp cop v1 ty1 v2 ty2 m =
Some v ->
v =
Values.Vtrue \/
v =
Values.Vfalse.
Proof.
Lemma binop_always_returns_bool_spec:
forall ce bop v1 t1 v2 t2 m v,
binop_always_returns_bool bop =
true ->
Cop.sem_binary_operation ce bop v1 t1 v2 t2 m =
Some v ->
v =
Values.Vint (
enumtag_to_int (
enumtag_of_cvalue v)).
Proof.
Lemma enumtag_to_int_0:
enumtag_to_int 0%
nat =
Int.zero.
Proof.
reflexivity. Qed.
Lemma enumtag_to_int_1:
enumtag_to_int 1%
nat =
Int.one.
Proof.
reflexivity. Qed.
Definition enumtag_cltype (
n:
nat) :
Ctypes.type :=
Ctypes.Tint (
intsize_of_enumtag n)
Ctypes.Unsigned Ctypes.noattr.
Fact enumtag_cltype_ctype:
forall n,
enumtag_cltype n =
cltype (
enumtag_ctype n).
Proof.
reflexivity. Qed.
Definition memory_chunk_of_enumtag (
n:
nat) :
AST.memory_chunk :=
if n <=? 2 ^ 8
then AST.Mint8unsigned
else if n <=? 2 ^ 16
then AST.Mint16unsigned
else AST.Mint32.
Definition type_to_chunk (
ty:
type) :
AST.memory_chunk :=
match ty with
|
Tprimitive ty =>
type_chunk ty
|
Tenum _
n =>
memory_chunk_of_enumtag (
List.length n)
end.
Lemma memory_chunk_of_enumtag_spec:
forall n,
n <= 2 ^ 8 /\
memory_chunk_of_enumtag n =
AST.Mint8unsigned
\/ 2 ^ 8 <
n <= 2 ^ 16 /\
memory_chunk_of_enumtag n =
AST.Mint16unsigned
\/ 2 ^ 16 <
n /\
memory_chunk_of_enumtag n =
AST.Mint32.
Proof.
Lemma intsize_of_enumtag_spec:
forall n,
n <= 2 ^ 8 /\
intsize_of_enumtag n =
Ctypes.I8
\/ 2 ^ 8 <
n <= 2 ^ 16 /\
intsize_of_enumtag n =
Ctypes.I16
\/ 2 ^ 16 <
n /\
intsize_of_enumtag n =
Ctypes.I32.
Proof.
Lemma intsize_memory_chunk_of_enumtag_spec:
forall n,
n <= 2 ^ 8
/\
intsize_of_enumtag n =
Ctypes.I8
/\
memory_chunk_of_enumtag n =
AST.Mint8unsigned
\/
2 ^ 8 <
n <= 2 ^ 16
/\
intsize_of_enumtag n =
Ctypes.I16
/\
memory_chunk_of_enumtag n =
AST.Mint16unsigned
\/
2 ^ 16 <
n
/\
intsize_of_enumtag n =
Ctypes.I32
/\
memory_chunk_of_enumtag n =
AST.Mint32.
Proof.
Lemma sem_cast_binarith_enumtag_cltype_l:
forall v n1 n2 m,
Cop.sem_cast (
Values.Vint v) (
enumtag_cltype n1)
(
Cop.binarith_type (
Cop.classify_binarith (
enumtag_cltype n1) (
enumtag_cltype n2)))
m
=
Some (
Values.Vint v).
Proof.
Lemma sem_cast_binarith_enumtag_cltype_r:
forall v n1 n2 m,
Cop.sem_cast (
Values.Vint v) (
enumtag_cltype n2)
(
Cop.binarith_type (
Cop.classify_binarith (
enumtag_cltype n1) (
enumtag_cltype n2)))
m
=
Some (
Values.Vint v).
Proof.
Lemma sem_binop_bool_spec:
forall ce bop c1 c2 m c n1 n2,
c1 <
n1 ->
c2 <
n2 ->
sem_binop_bool bop c1 c2 =
Some c ->
Cop.sem_binary_operation ce bop
(
Values.Vint (
enumtag_to_int c1)) (
enumtag_cltype n1)
(
Values.Vint (
enumtag_to_int c2)) (
enumtag_cltype n2)
m =
Some (
Values.Vint (
enumtag_to_int c)).
Proof.
Lemma binop_never_bool:
forall op ty1 ty2 ty,
Ctyping.type_binop op ty1 ty2 =
Errors.OK ty ->
forall sz a,
ty <>
Ctypes.Tint Ctypes.IBool sz a.
Proof.
Lemma truth_table_wt_value:
forall c1 c2 n1 n2 n3 n4 c,
n1 <= 1 ->
n2 <= 1 ->
n3 <= 1 ->
n4 <= 1 ->
truth_table c1 c2 n1 n2 n3 n4 =
Some c ->
wt_value (
Venum c)
bool_type.
Proof.
intros * ???? TT.
constructor; simpl.
destruct c1 as [|[]], c2 as [|[]]; simpl in *; inv TT; lia.
Qed.
Lemma pres_sem_binop:
forall bop ty1 ty2 ty v1 v2 v,
type_binop bop ty1 ty2 =
Some ty ->
sem_binop bop v1 ty1 v2 ty2 =
Some v ->
wt_value v1 ty1 ->
wt_value v2 ty2 ->
wt_value v ty.
Proof.
unfold type_binop,
sem_binop.
intros *
Hty Hsem Hwt1 Hwt2.
inversion Hwt1 as [??
Hwt1'|?
t1 n1];
inversion Hwt2 as [??
Hwt2'|?
t2 n2];
subst;
try discriminate.
-
destruct (
binop_always_returns_bool bop)
eqn:
Hbop;
apply option_map_inv in Hsem as (
c &
Hsem & ?);
subst.
+
inv Hty.
constructor.
apply option_map_inv in Hsem as (
cv &
Hsem & ?);
subst.
destruct bop;
try discriminate Hbop;
unfold Cop.sem_binary_operation in Hsem;
destruct (
sem_cmp_true_or_false _ _ _ _ _ _ _
Hsem);
subst;
simpl;
(
rewrite Int.unsigned_one ||
rewrite Int.unsigned_zero);
simpl;
lia.
+
destruct (
Ctyping.type_binop bop (
cltype _) (
cltype _))
as [
ct'|]
eqn:
E;
simpl in *;
try discriminate.
apply option_map_inv in Hty as (
ty' &
Hty & ?);
subst.
constructor.
pose proof (
binop_never_bool _ _ _ _
E)
as Hnbool.
pose proof (
wt_cvalue_not_vundef_nor_vptr _ _
Hwt1')
as (
Hnun1 &
Hnptr1).
pose proof (
wt_cvalue_not_vundef_nor_vptr _ _
Hwt2')
as (
Hnun2 &
Hnptr2).
apply wt_cvalue_wt_val_cltype in Hwt1'.
apply wt_cvalue_wt_val_cltype in Hwt2'.
pose proof (
Ctyping.pres_sem_binop _ _ _ _ _ _ _ _ _
E Hsem Hwt1' Hwt2')
as Hwt.
cut (
c <>
Values.Vundef
/\ (
forall b ofs,
c <>
Values.Vptr b ofs)
/\
good_bool c ct').
{
destruct 1
as (
Hnun' &
Hnptr' &
Hgb);
eauto using typecl_wt_val_wt_cvalue. }
destruct bop;
simpl in Hsem;
try discriminate Hbop.
*
unfold Cop.sem_add,
Cop.sem_binarith in Hsem.
rewrite classify_add_cltypes in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_sub,
Cop.sem_binarith in Hsem.
rewrite classify_sub_cltypes in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_mul,
Cop.sem_binarith in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_div,
Cop.sem_binarith in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_mod,
Cop.sem_binarith in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_and,
Cop.sem_binarith in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_or,
Cop.sem_binarith in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_xor,
Cop.sem_binarith in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_shl,
Cop.sem_shift in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
*
unfold Cop.sem_shr,
Cop.sem_shift in Hsem.
DestructCases;
repeat split;
try discriminate;
try ContradictNotVptr;
auto.
-
destruct ((
t1 ==
b bool_id) && (
t2 ==
b bool_id));
simpl in *.
+
apply option_map_inv in Hsem as (
c &
Hsem & ?);
subst.
destruct bop, (_ && _);
simpl in *;
try discriminate;
inv Hty;
eapply truth_table_wt_value with (5:=
Hsem);
eauto.
+
destruct bop;
try discriminate;
inv Hty;
inv Hsem;
constructor;
cases;
simpl;
lia.
Qed.
Lemma cvalue_dec:
forall v1 v2 :
cvalue, {
v1 =
v2} + {
v1 <>
v2}.
Proof.
Lemma ctype_dec:
forall t1 t2 :
ctype, {
t1 =
t2} + {
t1 <>
t2}.
Proof.
Lemma cconst_dec:
forall c1 c2 :
cconst, {
c1 =
c2} + {
c1 <>
c2}.
Proof.
Lemma unop_dec :
forall op1 op2 :
unop, {
op1 =
op2} + {
op1 <>
op2}.
Proof.
Lemma binop_dec :
forall op1 op2 :
binop, {
op1 =
op2} + {
op1 <>
op2}.
Proof.
decide equality.
Qed.
Lemma sem_unary_operation_any_mem:
forall op v ty M1 M2,
(
forall b ofs,
v <>
Values.Vptr b ofs) ->
Cop.sem_unary_operation op v ty M1
=
Cop.sem_unary_operation op v ty M2.
Proof.
intros *
Hnptr.
destruct op,
v;
simpl;
unfold Cop.sem_notbool,
Cop.sem_notint,
Cop.sem_neg,
Cop.sem_absfloat;
repeat match goal with
| |- (
match ?
x with _ => _
end) = _ =>
destruct x;
auto
| _ =>
ContradictNotVptr
end;
try (
now destruct ty;
auto).
specialize (
Hnptr b i);
contradiction.
Qed.
Lemma sem_cast_any_mem:
forall v ty1 ty2 M1 M2,
(
forall b ofs,
v <>
Values.Vptr b ofs) ->
Cop.sem_cast v ty1 ty2 M1 =
Cop.sem_cast v ty1 ty2 M2.
Proof.
Lemma sem_binary_operation_any_cenv_mem:
forall op v1 ty1 v2 ty2 M1 M2 cenv1 cenv2,
(
forall b ofs,
v1 <>
Values.Vptr b ofs) ->
(
forall b ofs,
v2 <>
Values.Vptr b ofs) ->
Cop.sem_binary_operation cenv1 op v1 (
cltype ty1)
v2 (
cltype ty2)
M1
=
Cop.sem_binary_operation cenv2 op v1 (
cltype ty1)
v2 (
cltype ty2)
M2.
Proof.
intros *
Hnptr1 Hnptr2.
destruct op;
simpl;
unfold Cop.sem_add,
Cop.sem_sub,
Cop.sem_mul,
Cop.sem_div,
Cop.sem_mod,
Cop.sem_and,
Cop.sem_or,
Cop.sem_xor,
Cop.sem_shl,
Cop.sem_shr,
Cop.sem_cmp,
Cop.sem_binarith;
try rewrite classify_add_cltypes;
try rewrite classify_sub_cltypes;
try rewrite classify_cmp_cltypes;
try rewrite (
sem_cast_any_mem v1 (
cltype ty1) _
M1 M2 Hnptr1);
try rewrite (
sem_cast_any_mem v2 (
cltype ty2) _
M1 M2 Hnptr2);
GoalMatchMatch.
Qed.
Lemma access_mode_cltype:
forall ty,
Ctypes.access_mode (
cltype ty) =
Ctypes.By_value (
type_chunk ty).
Proof.
destruct ty as [sz sg|sz|f].
- destruct sz, sg; auto.
- destruct sz; auto.
- destruct f; auto.
Qed.
Lemma wt_cvalue_load_result:
forall ty v,
wt_cvalue v ty ->
v =
Values.Val.load_result (
type_chunk ty)
v.
Proof.
intros *
Hwt.
destruct ty as [
sz sg|
sz|
sz].
-
destruct sz,
sg;
simpl;
inv Hwt;
auto.
+
rewrite <-
H2.
rewrite Int.sign_ext_idem;
auto with *.
+
rewrite <-
H2.
rewrite Int.zero_ext_idem;
auto with *.
+
rewrite <-
H2.
rewrite Int.sign_ext_idem;
auto with *.
+
rewrite <-
H2.
rewrite Int.zero_ext_idem;
auto with *.
+
destruct H2 as [
H2 |
H2 ];
rewrite H2;
rewrite <-
Int.zero_ext_idem;
auto with *.
+
destruct H2 as [
H2 |
H2 ];
rewrite H2;
rewrite <-
Int.zero_ext_idem;
auto with *.
-
destruct sz;
inv Hwt;
auto.
-
destruct sz;
inv Hwt;
auto.
Qed.
Open Scope string_scope.
Definition string_of_ctype (
ty:
ctype) :
String.string :=
match ty with
|
Tint Ctypes.IBool sg =>
"bool"
|
Tint Ctypes.I8 Ctypes.Signed =>
"int8"
|
Tint Ctypes.I8 Ctypes.Unsigned =>
"uint8"
|
Tint Ctypes.I16 Ctypes.Signed =>
"int16"
|
Tint Ctypes.I16 Ctypes.Unsigned =>
"uint16"
|
Tint Ctypes.I32 Ctypes.Signed =>
"int32"
|
Tint Ctypes.I32 Ctypes.Unsigned =>
"uint32"
|
Tlong Ctypes.Signed =>
"int64"
|
Tlong Ctypes.Unsigned =>
"uint64"
|
Tfloat Ctypes.F32 =>
"float32"
|
Tfloat Ctypes.F64 =>
"float64"
end.
Definition sem_extern f (
tyins :
list ctype)
xs (
tyout :
ctype)
y :=
forall ge mem,
Events.external_functions_sem
(
pos_to_str f)
{|
AST.sig_args :=
List.map (
fun cty =>
Ctypes.argtype_of_type (
cltype cty))
tyins;
AST.sig_res :=
Ctypes.rettype_of_type (
cltype tyout);
AST.sig_cc :=
AST.cc_default |}
ge xs mem nil y mem
/\
wt_cvalue y tyout.
Lemma sem_extern_det :
forall f tyins ins tyout out1 out2,
sem_extern f tyins ins tyout out1 ->
sem_extern f tyins ins tyout out2 ->
out1 =
out2.
Proof.
Lemma pres_sem_extern:
forall f tyins vins tyout vout,
List.Forall2 wt_cvalue vins tyins ->
sem_extern f tyins vins tyout vout ->
wt_cvalue vout tyout.
Proof.
Section Check_ops.
Concrete definition of check_unop.
* With no value provided, we only prohibit cast operations from floats
* to integers, which can fail on some values. More precisely, all of
* Float.to_int, Float.to_intu, Float.to_long, Float.to_longu
* triggers the operation ZofB_range f zmin zmax that can return None if either
* - f is infinite or NaN
* - ZofB f < zmin
* - ZofB f > zmax
Definition check_unop (
op :
unop) (_ :
option value) (
ty :
type) :
bool :=
match op,
ty with
|
CastOp t2,
Tprimitive t1 =>
match Cop.classify_cast (
cltype t1) (
cltype t2)
with
|
Cop.cast_case_f2i _ _
|
Cop.cast_case_s2i _ _
|
Cop.cast_case_f2l _
|
Cop.cast_case_s2l _ =>
false
| _ =>
true
end
| _, _ =>
true
end.
Lemma sem_cast_ok :
forall v ov t1 t2 r m,
wt_cvalue v t1 ->
check_unop (
CastOp t2)
ov (
Tprimitive t1) =
true ->
Ctyping.check_cast (
cltype t1) (
cltype t2) =
Errors.OK r ->
Cop.sem_cast v (
cltype t1) (
cltype t2)
m <>
None.
Proof.
intros *
Hwt Hck Ht.
unfold Cop.sem_cast,
Ctyping.check_cast in *.
destruct t1,
t2;
inv Hwt.
all:
simpl in *;
try congruence.
all:
cases_eqn HH;
congruence.
Qed.
Lemma unary_operation_ok :
forall op ty ty' v m,
Ctyping.type_unop op (
cltype ty) =
Errors.OK ty' ->
wt_cvalue v ty ->
Cop.sem_unary_operation op v (
cltype ty)
m <>
None.
Proof.
intros *
Hok Hwt.
destruct op;
simpl in *;
cases_eqn HH;
subst;
simpl in *.
all:
inv Hwt;
simpl in *;
cbn;
try congruence.
all:
cases_eqn HH;
subst;
cbn;
try congruence.
all:
unfold Cop.sem_notbool,
Cop.bool_val,
Cop.classify_bool in *.
all:
repeat (
cases_eqn HH;
subst;
simpl in *;
try congruence).
Qed.
Theorem check_unop_correct :
forall op ov ty,
check_unop op ov ty =
true ->
type_unop op ty <>
None ->
forall v,
wt_value v ty ->
match ov with
|
Some v' =>
v' =
v
| _ =>
True
end ->
sem_unop op v ty <>
None.
Proof.
Definition check_binop (
op :
binop) (
ov1 :
option value) (
ty1 :
type)
(
ov2 :
option value) (
ty2 :
type) :
bool :=
match op with
|
Cop.Odiv =>
match ty1,
ty2 with
|
Tprimitive t1,
Tprimitive t2 =>
match Cop.classify_binarith (
cltype t1) (
cltype t2)
with
|
Cop.bin_case_f
|
Cop.bin_case_s =>
true
|
Cop.bin_default =>
false
|
Cop.bin_case_i s =>
match ov2 with
|
Some (
Vscalar v2) =>
match Cop.sem_cast v2 (
cltype t2) (
Cop.binarith_type (
Cop.bin_case_i s))
Memory.Mem.empty with
|
Some (
Values.Vint n) =>
negb (
Integers.Int.eq n Integers.Int.zero)
&&
negb (
Integers.Int.eq n Integers.Int.mone)
| _ =>
false
end
| _ =>
false
end
|
Cop.bin_case_l s =>
match ov2 with
|
Some (
Vscalar v2) =>
match Cop.sem_cast v2 (
cltype t2) (
Cop.binarith_type (
Cop.bin_case_l s))
Memory.Mem.empty with
|
Some (
Values.Vlong n) =>
negb (
Integers.Int64.eq n Integers.Int64.zero)
&&
negb (
Integers.Int64.eq n Integers.Int64.mone)
| _ =>
false
end
| _ =>
false
end
end
| _,_ =>
false
end
|
Cop.Omod =>
match ty1,
ty2 with
|
Tprimitive t1,
Tprimitive t2 =>
match Cop.classify_binarith (
cltype t1) (
cltype t2)
with
|
Cop.bin_case_f
|
Cop.bin_case_s
|
Cop.bin_default =>
false
|
Cop.bin_case_i s =>
match ov2 with
|
Some (
Vscalar v2) =>
match Cop.sem_cast v2 (
cltype t2) (
Cop.binarith_type (
Cop.bin_case_i s))
Memory.Mem.empty with
|
Some (
Values.Vint n) =>
negb (
Integers.Int.eq n Integers.Int.zero)
&&
negb (
Integers.Int.eq n Integers.Int.mone)
| _ =>
false
end
| _ =>
false
end
|
Cop.bin_case_l s =>
match ov2 with
|
Some (
Vscalar v2) =>
match Cop.sem_cast v2 (
cltype t2) (
Cop.binarith_type (
Cop.bin_case_l s))
Memory.Mem.empty with
|
Some (
Values.Vlong n) =>
negb (
Integers.Int64.eq n Integers.Int64.zero)
&&
negb (
Integers.Int64.eq n Integers.Int64.mone)
| _ =>
false
end
| _ =>
false
end
end
| _,_ =>
false
end
|
Cop.Oshl
|
Cop.Oshr =>
match ty1,
ty2 with
|
Tprimitive t1,
Tprimitive t2 =>
match Cop.classify_shift (
cltype t1) (
cltype t2),
ov2 with
|
Cop.shift_case_ii _,
Some (
Vscalar (
Values.Vint n2)) =>
Int.ltu n2 Int.iwordsize
|
Cop.shift_case_il _,
Some (
Vscalar (
Values.Vlong n2)) =>
Int64.ltu n2 (
Int64.repr 32)
|
Cop.shift_case_li _,
Some (
Vscalar (
Values.Vint n2)) =>
Int.ltu n2 Int64.iwordsize'
|
Cop.shift_case_ll _,
Some (
Vscalar (
Values.Vlong n2)) =>
Int64.ltu n2 Int64.iwordsize
| _,_ =>
false
end
| _,_ =>
false
end
| _ =>
true
end.
Lemma sem_cast1_ok :
forall v1 t1 t2 m,
wt_cvalue v1 t1 ->
Cop.sem_cast v1 (
cltype t1) (
Cop.binarith_type (
Cop.classify_binarith (
cltype t1) (
cltype t2)))
m <>
None.
Proof.
unfold Cop.sem_cast,
Cop.classify_binarith.
intros *
Hwt1.
inv Hwt1;
simpl.
all:
cases_eqn HH;
subst.
all:
try congruence.
all:
simpl in *;
cases_eqn HH;
subst;
congruence.
Qed.
Lemma sem_cast2_ok :
forall v2 t1 t2 m,
wt_cvalue v2 t2 ->
Cop.sem_cast v2 (
cltype t2) (
Cop.binarith_type (
Cop.classify_binarith (
cltype t1) (
cltype t2)))
m <>
None.
Proof.
unfold Cop.sem_cast,
Cop.classify_binarith.
intros *
Hwt.
inv Hwt;
simpl.
all:
cases_eqn HH;
subst.
all:
try congruence.
all:
simpl in *;
cases_eqn HH;
subst;
congruence.
Qed.
Lemma sem_binarith_ok1 :
forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 m,
(
forall sg n1 n2,
sem_int sg n1 n2 <>
None) ->
(
forall sg n1 n2,
sem_long sg n1 n2 <>
None) ->
(
forall n1 n2,
sem_float n1 n2 <>
None) ->
(
forall n1 n2,
sem_single n1 n2 <>
None) ->
wt_cvalue v1 t1 ->
wt_cvalue v2 t2 ->
Cop.sem_binarith sem_int sem_long sem_float sem_single v1 (
cltype t1)
v2 (
cltype t2)
m <>
None.
Proof.
intros *
Hint Hlong Hfloat Hsingle Hwt1 Hwt2.
unfold Cop.sem_binarith.
destruct (
Cop.sem_cast v1 _ _ _)
eqn:
Hc1.
2:{
apply sem_cast1_ok in Hc1;
auto. }
destruct (
Cop.sem_cast v2 _ _ _)
eqn:
Hc2.
2:{
apply sem_cast2_ok in Hc2;
auto. }
destruct t1,
t2;
simpl.
all:
inv Hwt1;
inv Hwt2.
all:
repeat (
simpl in *;
cases_eqn HH;
subst).
all:
inv Hc1;
inv Hc2.
Qed.
Lemma sem_binarith_ok2 :
forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 m,
match Cop.classify_binarith (
cltype t1) (
cltype t2)
with
|
Cop.bin_case_i _ |
Cop.bin_case_l _ =>
(
forall sg n1 n2,
sem_int sg n1 n2 <>
None)
/\ (
forall sg n1 n2,
sem_long sg n1 n2 <>
None)
|
Cop.bin_case_f |
Cop.bin_case_s =>
(
forall n1 n2,
sem_float n1 n2 <>
None)
/\ (
forall n1 n2,
sem_single n1 n2 <>
None)
| _ =>
False
end ->
wt_cvalue v1 t1 ->
wt_cvalue v2 t2 ->
Cop.sem_binarith sem_int sem_long sem_float sem_single v1 (
cltype t1)
v2 (
cltype t2)
m <>
None.
Proof.
intros *
Hcl Hwt1 Hwt2.
unfold Cop.sem_binarith.
destruct (
Cop.sem_cast v1 _ _ _)
eqn:
Hc1.
2:{
apply sem_cast1_ok in Hc1;
auto. }
destruct (
Cop.sem_cast v2 _ _ _)
eqn:
Hc2.
2:{
apply sem_cast2_ok in Hc2;
auto. }
destruct t1,
t2;
simpl.
all:
inv Hwt1;
inv Hwt2.
all:
repeat (
simpl in *;
cases_eqn HH;
subst).
all:
inv Hc1;
inv Hc2.
all:
destruct Hcl;
congruence.
Qed.
Lemma cast_int_int :
forall v t1 t2 s,
wt_cvalue v t1 ->
Cop.classify_binarith (
cltype t1) (
cltype t2) =
Cop.bin_case_i s ->
exists n,
Cop.sem_cast v (
cltype t1) (
Ctypes.Tint Ctypes.I32 s Ctypes.noattr)
Memory.Mem.empty =
Some (
Values.Vint n).
Proof.
intros *
Hwt.
unfold Cop.classify_binarith.
destruct t1,
t2;
simpl;
cases_eqn HH;
subst;
try congruence.
all:
intro Hcl;
inv Hcl;
inv Hwt.
all:
unfold Cop.sem_cast;
simpl;
cases_eqn HH;
eauto.
Qed.
Lemma cast_long_long :
forall v t1 t2 s,
wt_cvalue v t1 ->
Cop.classify_binarith (
cltype t1) (
cltype t2) =
Cop.bin_case_l s ->
exists n,
Cop.sem_cast v (
cltype t1) (
Ctypes.Tlong s Ctypes.noattr)
Memory.Mem.empty =
Some (
Values.Vlong n).
Proof.
intros *
Hwt.
unfold Cop.classify_binarith.
destruct t1,
t2;
simpl;
cases_eqn HH;
subst;
try congruence.
all:
intro Hcl;
inv Hcl;
inv Hwt.
all:
unfold Cop.sem_cast;
simpl;
cases_eqn HH;
eauto.
Qed.
Theorem check_binop_correct :
forall op ov1 ty1 ov2 ty2,
check_binop op ov1 ty1 ov2 ty2 =
true ->
type_binop op ty1 ty2 <>
None ->
forall v1 v2,
wt_value v1 ty1 ->
wt_value v2 ty2 ->
match ov1 with
|
Some v =>
v =
v1
| _ =>
True
end ->
match ov2 with
|
Some v =>
v =
v2
| _ =>
True
end ->
sem_binop op v1 ty1 v2 ty2 <>
None.
Proof.
unfold sem_binop,
type_binop.
intros *
Hck Hty v1 v2 Hwt1 Hwt2 Hov1 Hov2.
destruct ty1 as [
t1|],
ty2 as [
t2|];
try congruence.
-
inv Hwt1;
inv Hwt2.
destruct op;
simpl in *;
try congruence;
repeat rewrite option_map_None.
+
unfold Cop.sem_add.
rewrite classify_add_cltypes.
apply sem_binarith_ok1;
congruence.
+
unfold Cop.sem_sub.
rewrite classify_sub_cltypes.
apply sem_binarith_ok1;
congruence.
+
unfold Cop.sem_mul.
apply sem_binarith_ok1;
congruence.
+
clear Hov1.
destruct (
Cop.classify_binarith (
cltype t1) (
cltype t2))
eqn:
Hcl.
all:
unfold Ctyping.binarith_type in Hty;
rewrite Hcl in Hty;
try congruence.
3,4:
unfold Cop.sem_div
;
apply sem_binarith_ok2;
try congruence
;
rewrite Hcl;
cases;
split;
congruence.
all:
destruct ov2 as [[
v2|]|];
try congruence;
inv Hov2;
clear Hty.
all:
unfold Cop.sem_div,
Cop.sem_binarith;
rewrite Hcl.
all:
destruct (
Cop.sem_cast v0 _ _ _)
as [[]|];
simpl;
try congruence.
1:
destruct (
cast_int_int v t1 t2 s)
as [? ->];
auto.
2:
destruct (
cast_long_long v t1 t2 s)
as [? ->];
auto.
all:
cases_eqn HH;
rewrite ?
Bool.andb_true_iff, ?
Bool.negb_true_iff,
?
Bool.orb_true_iff, ?
Bool.andb_true_iff in *;
destruct Hck;
try congruence;
destruct HH0 as [|[]];
congruence.
+
clear Hov1.
destruct (
Cop.classify_binarith (
cltype t1) (
cltype t2))
eqn:
Hcl.
all:
unfold Ctyping.binarith_int_type in Hty;
rewrite Hcl in Hty;
try congruence.
all:
destruct ov2 as [[
v2|]|];
try congruence;
inv Hov2;
clear Hty.
all:
unfold Cop.sem_mod,
Cop.sem_binarith;
rewrite Hcl.
all:
destruct (
Cop.sem_cast v0 _ _ _)
as [[]|];
simpl;
try congruence.
1:
destruct (
cast_int_int v t1 t2 s)
as [? ->];
auto.
2:
destruct (
cast_long_long v t1 t2 s)
as [? ->];
auto.
all:
cases_eqn HH;
rewrite ?
Bool.andb_true_iff, ?
Bool.negb_true_iff,
?
Bool.orb_true_iff, ?
Bool.andb_true_iff in *;
destruct Hck;
try congruence;
destruct HH0 as [|[]];
congruence.
+
clear Hov1 Hov2.
apply sem_binarith_ok2;
auto.
unfold Ctyping.binarith_int_type in *.
cases_eqn HH;
subst;
split;
try congruence.
+
clear Hov1 Hov2.
apply sem_binarith_ok2;
auto.
unfold Ctyping.binarith_int_type in *.
cases_eqn HH;
subst;
split;
try congruence.
+
clear Hov1 Hov2.
apply sem_binarith_ok2;
auto.
unfold Ctyping.binarith_int_type in *.
cases_eqn HH;
subst;
split;
try congruence.
+
clear Hov1.
inv H1;
inv H2;
simpl in *;
try congruence.
all:
unfold Cop.sem_shl,
Cop.sem_shift.
all:
cases_eqn HH;
subst;
try congruence.
all:
unfold Cop.classify_shift in *;
simpl in *.
all:
cases_eqn HH;
congruence.
+
clear Hov1.
inv H1;
inv H2;
simpl in *;
try congruence.
all:
unfold Cop.sem_shr,
Cop.sem_shift.
all:
cases_eqn HH;
subst;
try congruence.
all:
unfold Cop.classify_shift in *;
simpl in *.
all:
cases_eqn HH;
congruence.
+
unfold Cop.sem_cmp.
rewrite classify_cmp_cltypes.
apply sem_binarith_ok1;
congruence.
+
unfold Cop.sem_cmp.
rewrite classify_cmp_cltypes.
apply sem_binarith_ok1;
congruence.
+
unfold Cop.sem_cmp.
rewrite classify_cmp_cltypes.
apply sem_binarith_ok1;
congruence.
+
unfold Cop.sem_cmp.
rewrite classify_cmp_cltypes.
apply sem_binarith_ok1;
congruence.
+
unfold Cop.sem_cmp.
rewrite classify_cmp_cltypes.
apply sem_binarith_ok1;
congruence.
+
unfold Cop.sem_cmp.
rewrite classify_cmp_cltypes.
apply sem_binarith_ok1;
congruence.
-
clear Hov1 Hov2.
inv Hwt1;
inv Hwt2.
destruct ((
i ==
b bool_id) && (
i0 ==
b Ident.Ids.bool_id))
eqn:
Heq1.
2:
cases_eqn HH;
simpl in *;
congruence.
repeat (
cases_eqn Hl;
simpl in *;
try congruence).
apply andb_prop in Hl0 as [
Hl1 Hl2 ].
apply PeanoNat.Nat.eqb_eq in Hl1,
Hl2.
unfold option_map,
sem_binop_bool,
truth_table.
destruct op;
simpl in Hck;
try congruence.
all:
cases_eqn HH;
subst;
simpl in *;
try congruence;
lia.
Qed.
End Check_ops.
End Op.
Global Hint Resolve cltype_access_by_value cltype_align wt_cvalue_load_result sem_cast_same :
core.
Module OpAux :=
OperatorsAux Ids Op.
Import OpAux.
Definition value_to_cvalue (
v:
value) :
cvalue :=
match v with
|
Vscalar v =>
v
|
Venum n =>
Values.Vint (
enumtag_to_int n)
end.
From Velus Require Import CommonTyping.
From Velus Require Import Clocks.
Lemma wt_value_load_result:
forall ty v,
wt_value v ty ->
value_to_cvalue v =
Values.Val.load_result (
type_to_chunk ty) (
value_to_cvalue v).
Proof.
Global Hint Resolve wt_value_load_result :
typing.
Lemma wt_value_not_vundef_nor_vptr:
forall v ty,
wt_value v ty ->
value_to_cvalue v <>
Values.Vundef
/\
forall b ofs,
value_to_cvalue v <>
Values.Vptr b ofs.
Proof.
Definition translate_type (
ty:
type) :
Ctypes.type :=
match ty with
|
Tprimitive t =>
cltype t
|
Tenum _
tn =>
enumtag_cltype (
Datatypes.length tn)
end.
Lemma translate_type_align:
forall gcenv ty,
(
Memdata.align_chunk (
type_to_chunk ty) |
Ctypes.alignof gcenv (
translate_type ty))%
Z.
Proof.
Lemma translate_type_access_by_value:
forall ty,
Ctypes.access_mode (
translate_type ty) =
Ctypes.By_value (
type_to_chunk ty).
Proof.
Lemma sizeof_translate_type_chunk:
forall gcenv ty,
Ctypes.sizeof gcenv (
translate_type ty) =
Memdata.size_chunk (
type_to_chunk ty).
Proof.
Global Hint Resolve translate_type_access_by_value translate_type_align :
clight.
Lemma translate_type_not_void:
forall t,
translate_type t <>
Ctypes.Tvoid.
Proof.
intros [[]|[]]; simpl; discriminate.
Qed.
Global Hint Resolve translate_type_not_void :
clight.
Lemma sem_binary_operation_any_cenv_mem':
forall op v1 ty1 v2 ty2 M1 M2 cenv1 cenv2,
(
forall b ofs,
v1 <>
Values.Vptr b ofs) ->
(
forall b ofs,
v2 <>
Values.Vptr b ofs) ->
Cop.sem_binary_operation cenv1 op v1 (
translate_type ty1)
v2 (
translate_type ty2)
M1
=
Cop.sem_binary_operation cenv2 op v1 (
translate_type ty1)
v2 (
translate_type ty2)
M2.
Proof.
Lemma sem_cast_same':
forall m v t,
wt_value v t ->
Cop.sem_cast (
value_to_cvalue v) (
translate_type t) (
translate_type t)
m =
Some (
value_to_cvalue v).
Proof.
Global Hint Resolve sem_cast_same' :
clight.
Lemma sem_switch_arg_enum:
forall c tx tn,
Cop.sem_switch_arg (
value_to_cvalue (
Venum c)) (
translate_type (
Tenum tx tn)) =
Some (
Int.unsigned (
Int.repr (
Z.of_nat c))).
Proof.
Global Hint Resolve sem_switch_arg_enum :
clight.
Definition string_of_type (
ty:
type) :
String.string :=
match ty with
|
Tprimitive t =>
string_of_ctype t
|
Tenum t _ =>
pos_to_str t
end.
From Velus Require Import IndexedStreams.
From Velus Require Import CoindStreams.
From Velus Require Import Obc.
Module ComTyp :=
CommonTypingFun Ids Op OpAux.
Module Cks :=
ClocksFun Ids Op OpAux.
Module IStr :=
IndexedStreamsFun Ids Op OpAux Cks.
Module CStr :=
CoindStreamsFun Ids Op OpAux Cks.
Module Obc :=
ObcFun Ids Op OpAux ComTyp.