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.