Library val
The arithmetic operations and bit operations over the machine integer
The type of unary operations
The type of binary operations
Inductive bop:=
| oplus
| ominus
| omulti
| odiv
| olshift
| orshift
| oand
| oor
| obitand
| obitor
| oeq
| olt.
The semantics of unary and binary operations over values.
Definition notint (v: val) : option val :=
match v with
| Vint32 n => Some (Vint32 (Int.notbool n))
| _ => None
end.
Definition negint (v: val) : option val :=
match v with
| Vint32 n => Some (Vint32 (Int.not n))
| _ => None
end.
Definition uop_eval (v:val) (op1:uop):=
match op1 with
| oppsite => notint v
| negation => negint v
end.
Definition uop_type (t : type) (op1 : uop):=
match t with
| Tint8 => Some Tint8
| Tint16=> Some Tint16
| Tint32=> Some Tint32
| _ =>None
end.
Definition add (v1 v2: val) (t1 t2:type): option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 =>Some( Vint32(Int.add n1 n2))
| Vptr (b1, ofs1), Vint32 n2 =>
match t1 with
| Tptr t => Some( Vptr (b1, (Int.add ofs1 (Int.mul n2 (Int.repr (Z_of_nat (typelen t)))))))
| _ => None
end
| Vint32 n1, Vptr (b2, ofs2) =>
match t2 with
| Tptr t => Some( Vptr (b2, (Int.add ofs2 (Int.mul n1 (Int.repr (Z_of_nat (typelen t)))))))
| _ => None
end
| _, _ => None
end.
Definition sub (v1 v2: val) (t1:type): option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 => Some (Vint32(Int.sub n1 n2))
| Vptr (b1, ofs1), Vint32 n2 =>
match t1 with
| Tptr t => Some( Vptr (b1, (Int.sub ofs1 (Int.mul n2 (Int.repr (Z_of_nat (typelen t)))))))
| _ => None
end
| _, _ => None
end.
Definition mul (v1 v2: val): option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 => Some (Vint32(Int.mul n1 n2))
| _, _ => None
end.
Definition divs (v1 v2: val): option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 =>
if Int.eq n2 Int.zero
|| Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
then None
else Some(Vint32(Int.divs n1 n2))
| _, _ => None
end.
Definition and (v1 v2: val): option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 => Some (Vint32(Int.and n1 n2))
| _, _ => None
end.
Definition or (v1 v2: val): option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 =>Some ( Vint32(Int.or n1 n2))
| _, _ => None
end.
Definition shl (v1 v2: val):option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 =>
if Int.ltu n2 Int.iwordsize
then Some(Vint32(Int.shl n1 n2))
else None
| _, _ => None
end.
Definition shr (v1 v2: val):option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 =>
if Int.ltu n2 Int.iwordsize
then Some(Vint32(Int.shru n1 n2))
else None
| _, _ => None
end.
Definition val_eq (v1 v2:val):option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 =>
if (Int.eq n1 n2)
then Some(Vint32 (Int.one))
else Some(Vint32 (Int.zero))
| Vptr (b1, ofs1), Vptr (b2, ofs2) =>
if peq b1 b2 then (if (Int.eq ofs1 ofs2)
then Some(Vint32 (Int.one))
else Some(Vint32 (Int.zero)))
else Some(Vint32 (Int.zero))
| Vnull, Vptr (b,ofs) => Some (Vint32 (Int.zero))
| Vptr (b,ofs), Vnull => Some (Vint32 (Int.zero))
| Vnull, Vnull => Some (Vint32 (Int.one))
| _, _ => None
end.
Definition cmpu :=
fun (c : comparison) (x y : int32) =>
match c with
| Ceq => Int.eq x y
| Cne => negb (Int.eq x y)
| Clt => Int.ltu x y
| Cle => negb (Int.ltu y x)
| Cgt => Int.ltu y x
| Cge => negb (Int.ltu x y)
end.
Definition cmp_val (c: comparison) (v1 v2: val): option val :=
match v1, v2 with
| Vint32 n1, Vint32 n2 =>
if (cmpu c n1 n2)
then Some(Vint32 (Int.one))
else Some(Vint32 (Int.zero))
| _, _ => None
end.
Definition bool_and (v1 v2:val) : option val:=
match v1,v2 with
|Vint32 n1,Vint32 n2=>
if Int.ltu Int.zero n1 && Int.ltu Int.zero n2
then Some(Vint32 Int.one)
else Some(Vint32 Int.zero)
|_, _ =>None
end.
Definition bool_or (v1 v2:val) : option val:=
match v1,v2 with
|Vint32 n1,Vint32 n2=>
if Int.ltu Int.zero n1 || Int.ltu Int.zero n2
then Some(Vint32 Int.one)
else Some(Vint32 Int.zero)
|_, _ =>None
end.
Definition bop_eval (v1 v2:val) (t1 t2:type) (op1:bop) :=
match op1 with
| oplus => add v1 v2 t1 t2
| ominus => sub v1 v2 t1
| omulti => mul v1 v2
| odiv => divs v1 v2
| olshift => shl v1 v2
| orshift => shr v1 v2
| oand => bool_and v1 v2
| oor => bool_or v1 v2
| obitand => and v1 v2
| obitor => or v1 v2
| oeq => val_eq v1 v2
| olt => cmp_val Clt v1 v2
end.
Definition bop_int_type (t1 t2:type):=
match t1,t2 with
| Tint8, Tint8 => Some Tint8
| Tint8, Tint16 => Some Tint16
| Tint8, Tint32 => Some Tint32
| Tint16, Tint8 => Some Tint16
| Tint16, Tint16 => Some Tint16
| Tint16, Tint32 => Some Tint32
| Tint32, Tint8 => Some Tint32
| Tint32, Tint16 => Some Tint32
| Tint32, Tint32 => Some Tint32
| _, _ =>None
end.
Definition cmp_int_type (t1 t2:type):=
match t1,t2 with
| Tint8, Tint8 => Some Tint32
| Tint8, Tint16 => Some Tint32
| Tint8, Tint32 => Some Tint32
| Tint16, Tint8 => Some Tint32
| Tint16, Tint16 => Some Tint32
| Tint16, Tint32 => Some Tint32
| Tint32, Tint8 => Some Tint32
| Tint32, Tint16 => Some Tint32
| Tint32, Tint32 => Some Tint32
| _, _ =>None
end.
Definition bop_type (t1 t2:type) (op1:bop):=
match op1 with
| oplus => match t1 with
| Tptr t => match t2 with
| Tint8 => Some (Tptr t)
| Tint16 => Some (Tptr t)
| Tint32 => Some (Tptr t)
| _ => None
end
| Tint8 => match t2 with
|Tptr t => Some (Tptr t)
| _ => bop_int_type t1 t2
end
| Tint16 => match t2 with
|Tptr t => Some (Tptr t)
| _ => bop_int_type t1 t2
end
| Tint32 => match t2 with
|Tptr t => Some (Tptr t)
| _ => bop_int_type t1 t2
end
| _ => None
end
| ominus => match t1 with
| Tptr t => match t2 with
| Tint8 => Some (Tptr t)
| Tint16 => Some (Tptr t)
| Tint32 => Some (Tptr t)
| _ => None
end
| _ => bop_int_type t1 t2
end
| omulti => bop_int_type t1 t2
| odiv => bop_int_type t1 t2
| olshift => bop_int_type t1 t2
| orshift => bop_int_type t1 t2
| oand => bop_int_type t1 t2
| oor => bop_int_type t1 t2
| obitand => bop_int_type t1 t2
| obitor => bop_int_type t1 t2
| oeq => match t1 with
| Tptr t => match t2 with
| Tptr t´ => Some Tint32
| Tnull => Some Tint32
| Tcom_ptr x => Some Tint32
| _ => None
end
| Tcom_ptr x => match t2 with
| Tptr t´ => Some Tint32
| Tnull => Some Tint32
| Tcom_ptr x´ => Some Tint32
| _ => None
end
| Tnull => match t2 with
| Tptr t´ => Some Tint32
| Tcom_ptr x => Some Tint32
| Tnull => Some Tint32
| _ => None
end
| _ => cmp_int_type t1 t2
end
| olt =>cmp_int_type t1 t2
end.