Commit c6d2ef0c authored by xleroy's avatar xleroy
Browse files

Make Clight independent of CompCert C.

Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent f7693b3d
......@@ -98,18 +98,20 @@ $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.v
$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo
$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo
cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo
cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo
cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo
cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo
cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo
cfrontend/Ctypes.vo cfrontend/Ctypes.glob: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo
cfrontend/Cop.vo cfrontend/Cop.glob: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo
cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo common/Smallstep.vo
cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo
cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo
cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo
cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo
cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo
cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo
cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo
cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo
......
......@@ -22,13 +22,14 @@ option) any later version:
backend/CMtypecheck.ml common/Mem.v
backend/CMtypecheck.mli common/Smallstep.v
cfrontend/C2C.ml common/Switch.v
cfrontend/Csem.v common/Values.v
cfrontend/Csyntax.v lib/Coqlib.v
cfrontend/Cstrategy.v lib/Floats.v
cfrontend/Clight.v lib/Integers.v
cfrontend/PrintCsyntax.ml lib/Maps.v
cfrontend/PrintClight.ml lib/Parmov.v
lib/Camlcoq.ml
cfrontend/Cop.v common/Values.v
cfrontend/Ctypes.v lib/Coqlib.v
cfrontend/Csem.v lib/Floats.v
cfrontend/Csyntax.v lib/Integers.v
cfrontend/Cstrategy.v lib/Maps.v
cfrontend/Clight.v lib/Parmov.v
cfrontend/PrintCsyntax.ml lib/Camlcoq.ml
cfrontend/PrintClight.ml
all files in the runtime/ directory
all files in the cparser/ directory
......
......@@ -90,7 +90,7 @@ BACKEND=\
# C front-end modules (in cfrontend/)
CFRONTEND=Csyntax.v Csem.v Cstrategy.v Cexec.v \
CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \
Initializers.v Initializersproof.v \
SimplExpr.v SimplExprspec.v SimplExprproof.v \
Clight.v Cshmgen.v Cshmgenproof.v \
......
......@@ -22,6 +22,8 @@ open Builtins
open Camlcoq
open AST
open Values
open Ctypes
open Cop
open Csyntax
open Initializers
......@@ -723,7 +725,7 @@ let convertGlobvar env (sto, id, ty, optinit) =
let init' =
match optinit with
| None ->
if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')]
if sto = C.Storage_extern then [] else [Init_space(Ctypes.sizeof ty')]
| Some i ->
convertInitializer env ty i in
let align =
......
......@@ -25,6 +25,8 @@ Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Determinism.
Require Import Ctypes.
Require Import Cop.
Require Import Csyntax.
Require Import Csem.
Require Cstrategy.
......
......@@ -28,12 +28,11 @@ Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Csyntax.
Require Import Csem.
Require Import Ctypes.
Require Import Cop.
(** * Abstract syntax *)
(** ** Expressions *)
(** Clight expressions correspond to the "pure" subset of C expressions.
......@@ -84,8 +83,9 @@ Definition typeof (e: expr) : type :=
(** Clight statements are similar to those of Compcert C, with the addition
of assigment (of a rvalue to a lvalue), assignment to a temporary,
and function call (with assignment of the result to a temporary).
The three C loops are replaced by a single infinite loop [Sloop s1 s2]
that executes [s1] then [s2] repeatedly. A [continue] in [s1] branches to [s2]. *)
The three C loops are replaced by a single infinite loop [Sloop s1
s2] that executes [s1] then [s2] repeatedly. A [continue] in [s1]
branches to [s2]. *)
Definition label := ident.
......@@ -145,16 +145,6 @@ Inductive fundef : Type :=
| Internal: function -> fundef
| External: external_function -> typelist -> type -> fundef.
(** ** Programs *)
(** A program is a collection of named functions, plus a collection
of named global variables, carrying their types and optional initialization
data. See module [AST] for more details. *)
Definition program : Type := AST.program fundef type.
(** * Operations over types *)
(** The type of a function definition. *)
Definition type_of_function (f: function) : type :=
......@@ -166,6 +156,14 @@ Definition type_of_fundef (f: fundef) : type :=
| External id args res => Tfunction args res
end.
(** ** Programs *)
(** A program is a collection of named functions, plus a collection
of named global variables, carrying their types and optional initialization
data. See module [AST] for more details. *)
Definition program : Type := AST.program fundef type.
(** * Operational semantics *)
(** The semantics uses two environments. The global environment
......@@ -174,9 +172,9 @@ Definition type_of_fundef (f: fundef) : type :=
Definition genv := Genv.t fundef type.
(** The local environment maps local variables to block references
and types. The current value of the variable is stored in the associated memory
block. *)
(** The local environment maps local variables to block references and
types. The current value of the variable is stored in the
associated memory block. *)
Definition env := PTree.t (block * type). (* map variable -> location & type *)
......@@ -226,6 +224,25 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' ->
assign_loc ty m b ofs (Vptr b' ofs') m'.
(** Allocation of function-local variables.
[alloc_variables e1 m1 vars e2 m2] allocates one memory block
for each variable declared in [vars], and associates the variable
name with this block. [e1] and [m1] are the initial local environment
and memory state. [e2] and [m2] are the final local environment
and memory state. *)
Inductive alloc_variables: env -> mem ->
list (ident * type) ->
env -> mem -> Prop :=
| alloc_variables_nil:
forall e m,
alloc_variables e m nil e m
| alloc_variables_cons:
forall e m id ty vars m1 b1 m2 e2,
Mem.alloc m 0 (sizeof ty) = (m1, b1) ->
alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 ->
alloc_variables e m ((id, ty) :: vars) e2 m2.
(** Initialization of local variables that are parameters to a function.
[bind_parameters e m1 params args m2] stores the values [args]
in the memory blocks corresponding to the variables [params].
......@@ -252,6 +269,14 @@ Fixpoint create_undef_temps (temps: list (ident * type)) : temp_env :=
| (id, t) :: temps' => PTree.set id Vundef (create_undef_temps temps')
end.
(** Return the list of blocks in the codomain of [e], with low and high bounds. *)
Definition block_of_binding (id_b_ty: ident * (block * type)) :=
match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end.
Definition blocks_of_env (e: env) : list (block * Z * Z) :=
List.map block_of_binding (PTree.elements e).
(** Optional assignment to a temporary *)
Definition set_opttemp (optid: option ident) (v: val) (le: temp_env) :=
......
This diff is collapsed.
......@@ -25,528 +25,11 @@ Require Import AST.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Ctypes.
Require Import Cop.
Require Import Csyntax.
Require Import Smallstep.
(** * Semantics of type-dependent operations *)
(** Semantics of casts. [sem_cast v1 t1 t2 = Some v2] if value [v1],
viewed with static type [t1], can be cast to type [t2],
resulting in value [v2]. *)
Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
match sz, sg with
| I8, Signed => Int.sign_ext 8 i
| I8, Unsigned => Int.zero_ext 8 i
| I16, Signed => Int.sign_ext 16 i
| I16, Unsigned => Int.zero_ext 16 i
| I32, _ => i
| IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one
end.
Definition cast_int_float (si : signedness) (i: int) : float :=
match si with
| Signed => Float.floatofint i
| Unsigned => Float.floatofintu i
end.
Definition cast_float_int (si : signedness) (f: float) : option int :=
match si with
| Signed => Float.intoffloat f
| Unsigned => Float.intuoffloat f
end.
Definition cast_float_float (sz: floatsize) (f: float) : float :=
match sz with
| F32 => Float.singleoffloat f
| F64 => f
end.
Function sem_cast (v: val) (t1 t2: type) : option val :=
match classify_cast t1 t2 with
| cast_case_neutral =>
match v with
| Vint _ | Vptr _ _ => Some v
| _ => None
end
| cast_case_i2i sz2 si2 =>
match v with
| Vint i => Some (Vint (cast_int_int sz2 si2 i))
| _ => None
end
| cast_case_f2f sz2 =>
match v with
| Vfloat f => Some (Vfloat (cast_float_float sz2 f))
| _ => None
end
| cast_case_i2f si1 sz2 =>
match v with
| Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
| _ => None
end
| cast_case_f2i sz2 si2 =>
match v with
| Vfloat f =>
match cast_float_int si2 f with
| Some i => Some (Vint (cast_int_int sz2 si2 i))
| None => None
end
| _ => None
end
| cast_case_f2bool =>
match v with
| Vfloat f =>
Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one))
| _ => None
end
| cast_case_p2bool =>
match v with
| Vint i => Some (Vint (cast_int_int IBool Signed i))
| Vptr _ _ => Some (Vint Int.one)
| _ => None
end
| cast_case_struct id1 fld1 id2 fld2 =>
if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
| cast_case_union id1 fld1 id2 fld2 =>
if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
| cast_case_void =>
Some v
| cast_case_default =>
None
end.
(** Interpretation of values as truth values.
Non-zero integers, non-zero floats and non-null pointers are
considered as true. The integer zero (which also represents
the null pointer) and the float 0.0 are false. *)
Definition bool_val (v: val) (t: type) : option bool :=
match classify_bool t with
| bool_case_i =>
match v with
| Vint n => Some (negb (Int.eq n Int.zero))
| _ => None
end
| bool_case_f =>
match v with
| Vfloat f => Some (negb (Float.cmp Ceq f Float.zero))
| _ => None
end
| bool_case_p =>
match v with
| Vint n => Some (negb (Int.eq n Int.zero))
| Vptr b ofs => Some true
| _ => None
end
| bool_default => None
end.
(** The following [sem_] functions compute the result of an operator
application. Since operators are overloaded, the result depends
both on the static types of the arguments and on their run-time values.
For binary operations, the "usual binary conversions", adapted to a 32-bit
platform, state that:
- If both arguments are of integer type, an integer operation is performed.
For operations that behave differently at unsigned and signed types
(e.g. division, modulus, comparisons), the unsigned operation is selected
if at least one of the arguments is of type "unsigned int32", otherwise
the signed operation is performed.
- If both arguments are of float type, a float operation is performed.
We choose to perform all float arithmetic in double precision,
even if both arguments are single-precision floats.
- If one argument has integer type and the other has float type,
we convert the integer argument to float, then perform the float operation.
*)
Function sem_neg (v: val) (ty: type) : option val :=
match classify_neg ty with
| neg_case_i sg =>
match v with
| Vint n => Some (Vint (Int.neg n))
| _ => None
end
| neg_case_f =>
match v with
| Vfloat f => Some (Vfloat (Float.neg f))
| _ => None
end
| neg_default => None
end.
Function sem_notint (v: val) (ty: type): option val :=
match classify_notint ty with
| notint_case_i sg =>
match v with
| Vint n => Some (Vint (Int.xor n Int.mone))
| _ => None
end
| notint_default => None
end.
Function sem_notbool (v: val) (ty: type) : option val :=
match classify_bool ty with
| bool_case_i =>
match v with
| Vint n => Some (Val.of_bool (Int.eq n Int.zero))
| _ => None
end
| bool_case_f =>
match v with
| Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero))
| _ => None
end
| bool_case_p =>
match v with
| Vint n => Some (Val.of_bool (Int.eq n Int.zero))
| Vptr _ _ => Some Vfalse
| _ => None
end
| bool_default => None
end.
Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_add t1 t2 with
| add_case_ii sg => (**r integer addition *)
match v1, v2 with
| Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
| _, _ => None
end
| add_case_ff => (**r float addition *)
match v1, v2 with
| Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2))
| _, _ => None
end
| add_case_if sg => (**r int plus float *)
match v1, v2 with
| Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2))
| _, _ => None
end
| add_case_fi sg => (**r float plus int *)
match v1, v2 with
| Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2)))
| _, _ => None
end
| add_case_pi ty _ => (**r pointer plus integer *)
match v1,v2 with
| Vptr b1 ofs1, Vint n2 =>
Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
| _, _ => None
end
| add_case_ip ty _ => (**r integer plus pointer *)
match v1,v2 with
| Vint n1, Vptr b2 ofs2 =>
Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
| _, _ => None
end
| add_default => None
end.
Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_sub t1 t2 with
| sub_case_ii sg => (**r integer subtraction *)
match v1,v2 with
| Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
| _, _ => None
end
| sub_case_ff => (**r float subtraction *)
match v1,v2 with
| Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2))
| _, _ => None
end
| sub_case_if sg => (**r int minus float *)
match v1, v2 with
| Vint n1, Vfloat n2 => Some (Vfloat (Float.sub (cast_int_float sg n1) n2))
| _, _ => None
end
| sub_case_fi sg => (**r float minus int *)
match v1, v2 with
| Vfloat n1, Vint n2 => Some (Vfloat (Float.sub n1 (cast_int_float sg n2)))
| _, _ => None
end
| sub_case_pi ty => (**r pointer minus integer *)
match v1,v2 with
| Vptr b1 ofs1, Vint n2 =>
Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
| _, _ => None
end
| sub_case_pp ty => (**r pointer minus pointer *)
match v1,v2 with
| Vptr b1 ofs1, Vptr b2 ofs2 =>
if zeq b1 b2 then
if Int.eq (Int.repr (sizeof ty)) Int.zero then None
else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty))))
else None
| _, _ => None
end
| sub_default => None
end.
Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_mul t1 t2 with
| mul_case_ii sg =>
match v1,v2 with
| Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2))
| _, _ => None
end
| mul_case_ff =>
match v1,v2 with
| Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
| _, _ => None
end
| mul_case_if sg =>
match v1, v2 with
| Vint n1, Vfloat n2 => Some (Vfloat (Float.mul (cast_int_float sg n1) n2))
| _, _ => None
end
| mul_case_fi sg =>
match v1, v2 with
| Vfloat n1, Vint n2 => Some (Vfloat (Float.mul n1 (cast_int_float sg n2)))
| _, _ => None
end
| mul_default =>
None
end.
Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_div t1 t2 with
| div_case_ii Unsigned =>
match v1,v2 with
| Vint n1, Vint n2 =>
if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
| _,_ => None
end
| div_case_ii Signed =>
match v1,v2 with
| Vint n1, Vint n2 =>
if Int.eq n2 Int.zero
|| Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
then None else Some (Vint(Int.divs n1 n2))
| _,_ => None
end
| div_case_ff =>
match v1,v2 with
| Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2))
| _, _ => None
end
| div_case_if sg =>
match v1, v2 with
| Vint n1, Vfloat n2 => Some (Vfloat (Float.div (cast_int_float sg n1) n2))
| _, _ => None
end
| div_case_fi sg =>
match v1, v2 with
| Vfloat n1, Vint n2 => Some (Vfloat (Float.div n1 (cast_int_float sg n2)))
| _, _ => None
end
| div_default =>
None
end.
Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_binint t1 t2 with
| binint_case_ii Unsigned =>
match v1, v2 with
| Vint n1, Vint n2 =>
if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
| _, _ => None
end
| binint_case_ii Signed =>
match v1,v2 with
| Vint n1, Vint n2 =>
if Int.eq n2 Int.zero
|| Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
then None else Some (Vint (Int.mods n1 n2))
| _, _ => None
end
| binint_default =>
None
end.
Function sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_binint t1 t2 with
| binint_case_ii sg =>
match v1, v2 with
| Vint n1, Vint n2 => Some (Vint(Int.and n1 n2))
| _, _ => None
end
| binint_default => None
end.
Function sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_binint t1 t2 with
| binint_case_ii sg =>
match v1, v2 with
| Vint n1, Vint n2 => Some (Vint(Int.or n1 n2))
| _, _ => None
end
| binint_default => None
end.
Function sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_binint t1 t2 with
| binint_case_ii sg =>
match v1, v2 with
| Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2))
| _, _ => None
end
| binint_default => None
end.
Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
match classify_shift t1 t2 with
| shift_case_ii sg =>
match v1, v2 with
| Vint n1, Vint n2 =>
if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None
| _, _ => None
end
| shift_default => None
end.
Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val :=
match classify_shift t1 t2 with
| shift_case_ii Unsigned =>
match v1,v2 with
| Vint n1, Vint n2 =>
if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
| _,_ => None