Module Cminorops
Require Import Coqlib.
Require Import Integers.
Require Import Floats.
Require Import Pointers.
Require Import Values.
Require Import Libtactics.
Require Import Ast.
Inductive unary_operation :
Type :=
|
Ocast8unsigned:
unary_operation (* 8-bit zero extension *)
|
Ocast8signed:
unary_operation (* 8-bit sign extension *)
|
Ocast16unsigned:
unary_operation (* 16-bit zero extension *)
|
Ocast16signed:
unary_operation (* 16-bit sign extension *)
|
Onegint:
unary_operation (* integer opposite *)
|
Onotbool:
unary_operation (* boolean negation *)
|
Onotint:
unary_operation (* bitwise complement *)
|
Onegf:
unary_operation (* float opposite *)
|
Osingleoffloat:
unary_operation (* float truncation *)
|
Ointoffloat:
unary_operation (* signed integer to float *)
|
Ointuoffloat:
unary_operation (* unsigned integer to float *)
|
Ofloatofint:
unary_operation (* float to signed integer *)
|
Ofloatofintu:
unary_operation.
(* float to unsigned integer *)
Inductive binary_operation :
Type :=
|
Oadd:
binary_operation (* integer addition *)
|
Osub:
binary_operation (* integer subtraction *)
|
Omul:
binary_operation (* integer multiplication *)
|
Odiv:
binary_operation (* integer signed division *)
|
Odivu:
binary_operation (* integer unsigned division *)
|
Omod:
binary_operation (* integer signed modulus *)
|
Omodu:
binary_operation (* integer unsigned modulus *)
|
Oand:
binary_operation (* bitwise ``and'' *)
|
Oor:
binary_operation (* bitwise ``or'' *)
|
Oxor:
binary_operation (* bitwise ``xor'' *)
|
Oshl:
binary_operation (* left shift *)
|
Oshr:
binary_operation (* right signed shift *)
|
Oshru:
binary_operation (* right unsigned shift *)
|
Oaddf:
binary_operation (* float addition *)
|
Osubf:
binary_operation (* float subtraction *)
|
Omulf:
binary_operation (* float multiplication *)
|
Odivf:
binary_operation (* float division *)
|
Ocmp:
comparison ->
binary_operation (* integer signed comparison *)
|
Ocmpu:
comparison ->
binary_operation (* integer unsigned comparison *)
|
Ocmpf:
comparison ->
binary_operation.
(* float comparison *)
Inductive atomic_statement :
Type :=
|
AScas:
atomic_statement (* compare and swap *)
|
ASlkinc:
atomic_statement.
(* lock inc *)
Definition eval_unop (
op:
unary_operation) (
arg:
val) :
option val :=
match op,
arg with
|
Ocast8unsigned,
_ =>
Some (
Val.zero_ext 8
arg)
|
Ocast8signed,
_ =>
Some (
Val.sign_ext 8
arg)
|
Ocast16unsigned,
_ =>
Some (
Val.zero_ext 16
arg)
|
Ocast16signed,
_ =>
Some (
Val.sign_ext 16
arg)
|
Onegint,
Vint n1 =>
Some (
Vint (
Int.neg n1))
|
Onotbool,
Vint n1 =>
Some (
Val.of_bool (
Int.eq n1 Int.zero))
|
Onotbool,
Vptr p =>
Some Vfalse
|
Onotint,
Vint n1 =>
Some (
Vint (
Int.not n1))
|
Onegf,
Vfloat f1 =>
Some (
Vfloat (
Float.neg f1))
|
Osingleoffloat,
_ =>
Some (
Val.singleoffloat arg)
|
Ointoffloat,
Vfloat f1 =>
Some (
Vint (
Float.intoffloat f1))
|
Ointuoffloat,
Vfloat f1 =>
Some (
Vint (
Float.intuoffloat f1))
|
Ofloatofint,
Vint n1 =>
Some (
Vfloat (
Float.floatofint n1))
|
Ofloatofintu,
Vint n1 =>
Some (
Vfloat (
Float.floatofintu n1))
|
_,
_ =>
None
end.
Definition eval_compare_mismatch (
c:
comparison) :
option val :=
match c with Ceq =>
Some Vfalse |
Cne =>
Some Vtrue |
_ =>
None end.
Definition eval_compare_null (
c:
comparison) (
n:
int) :
option val :=
if Int.eq n Int.zero then eval_compare_mismatch c else None.
Definition eval_binop
(
op:
binary_operation) (
arg1 arg2:
val):
option val :=
match op,
arg1,
arg2 with
|
Oadd,
Vint n1,
Vint n2 =>
Some (
Vint (
Int.add n1 n2))
|
Oadd,
Vint n1,
Vptr p2 =>
Some (
Vptr (
Ptr.add p2 n1))
|
Oadd,
Vptr p1,
Vint n2 =>
Some (
Vptr (
Ptr.add p1 n2))
|
Osub,
Vint n1,
Vint n2 =>
Some (
Vint (
Int.sub n1 n2))
|
Osub,
Vptr p1,
Vint n2 =>
Some (
Vptr (
Ptr.sub_int p1 n2))
|
Osub,
Vptr p1,
Vptr p2 =>
option_map Vint (
Ptr.sub_ptr p1 p2)
|
Omul,
Vint n1,
Vint n2 =>
Some (
Vint (
Int.mul n1 n2))
|
Odiv,
Vint n1,
Vint n2 =>
if Int.eq n2 Int.zero then None else Some (
Vint (
Int.divs n1 n2))
|
Odivu,
Vint n1,
Vint n2 =>
if Int.eq n2 Int.zero then None else Some (
Vint (
Int.divu n1 n2))
|
Omod,
Vint n1,
Vint n2 =>
if Int.eq n2 Int.zero then None else Some (
Vint (
Int.mods n1 n2))
|
Omodu,
Vint n1,
Vint n2 =>
if Int.eq n2 Int.zero then None else Some (
Vint (
Int.modu n1 n2))
|
Oand,
Vint n1,
Vint n2 =>
Some (
Vint (
Int.and n1 n2))
|
Oor,
Vint n1,
Vint n2 =>
Some (
Vint (
Int.or n1 n2))
|
Oxor,
Vint n1,
Vint n2 =>
Some (
Vint (
Int.xor n1 n2))
|
Oshl,
Vint n1,
Vint n2 =>
if Int.ltu n2 (
Int.repr 32)
then Some (
Vint (
Int.shl n1 n2))
else None
|
Oshr,
Vint n1,
Vint n2 =>
if Int.ltu n2 (
Int.repr 32)
then Some (
Vint (
Int.shr n1 n2))
else None
|
Oshru,
Vint n1,
Vint n2 =>
if Int.ltu n2 (
Int.repr 32)
then Some (
Vint (
Int.shru n1 n2))
else None
|
Oaddf,
Vfloat f1,
Vfloat f2 =>
Some (
Vfloat (
Float.add f1 f2))
|
Osubf,
Vfloat f1,
Vfloat f2 =>
Some (
Vfloat (
Float.sub f1 f2))
|
Omulf,
Vfloat f1,
Vfloat f2 =>
Some (
Vfloat (
Float.mul f1 f2))
|
Odivf,
Vfloat f1,
Vfloat f2 =>
Some (
Vfloat (
Float.div f1 f2))
|
Ocmp c,
Vint n1,
Vint n2 =>
Some (
Val.of_bool(
Int.cmp c n1 n2))
|
Ocmp c,
Vptr p1,
Vptr p2 =>
Val.option_val_of_bool3 (
Ptr.cmp c p1 p2)
|
Ocmp c,
Vptr p1,
Vint n2 =>
eval_compare_null c n2
|
Ocmp c,
Vint n1,
Vptr p2 =>
eval_compare_null c n1
|
Ocmpu c,
Vint n1,
Vint n2 =>
Some (
Val.of_bool(
Int.cmpu c n1 n2))
|
Ocmpf c,
Vfloat f1,
Vfloat f2 =>
Some (
Val.of_bool (
Float.cmp c f1 f2))
|
_,
_,
_ =>
None
end.
Require Import Events.
Definition sem_atomic_statement
(
astmt :
atomic_statement) (
args :
list val) :
option (
pointer *
rmw_instr) :=
match astmt,
args with
|
AScas,
Vptr p ::
n ::
o ::
nil =>
if (
Val.eq_dec o Vundef)
then None
else if (
Val.has_type o Tint)
then if (
Val.eq_dec n Vundef)
then None
else if (
Val.has_type n Tint)
then Some (
p,
rmw_CAS o n)
else None
else None
|
ASlkinc,
Vptr p ::
nil =>
Some (
p,
rmw_ADD (
Vint Int.one))
|
_,
_ =>
None
end.