diff options
Diffstat (limited to 'backend/CminorSel.v')
-rw-r--r-- | backend/CminorSel.v | 329 |
1 files changed, 196 insertions, 133 deletions
diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 331105e..859c46e 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -12,6 +12,7 @@ Require Import Cminor. Require Import Op. Require Import Globalenvs. Require Import Switch. +Require Import Smallstep. (** * Abstract syntax *) @@ -19,7 +20,10 @@ Require Import Switch. functions, statements and expressions. However, CminorSel uses machine-dependent operations, addressing modes and conditions, as defined in module [Op] and used in lower-level intermediate - languages ([RTL] and below). Moreover, a variant [condexpr] of [expr] + languages ([RTL] and below). Moreover, to express sharing of + sub-computations, a "let" binding is provided (constructions + [Elet] and [Eletvar]), using de Bruijn indices to refer to "let"-bound + variables. Finally, a variant [condexpr] of [expr] is used to represent expressions which are evaluated for their boolean value only and not their exact value. *) @@ -28,12 +32,9 @@ Inductive expr : Set := | Evar : ident -> expr | Eop : operation -> exprlist -> expr | Eload : memory_chunk -> addressing -> exprlist -> expr - | Estore : memory_chunk -> addressing -> exprlist -> expr -> expr - | Ecall : signature -> expr -> exprlist -> expr | Econdition : condexpr -> expr -> expr -> expr | Elet : expr -> expr -> expr | Eletvar : nat -> expr - | Ealloc : expr -> expr with condexpr : Set := | CEtrue: condexpr @@ -46,12 +47,15 @@ with exprlist : Set := | Econs: expr -> exprlist -> exprlist. (** Statements are as in Cminor, except that the condition of an - if/then/else conditional is a [condexpr]. *) + if/then/else conditional is a [condexpr], and the [Sstore] construct + uses a machine-dependent addressing mode. *) Inductive stmt : Set := | Sskip: stmt - | Sexpr: expr -> stmt | Sassign : ident -> expr -> stmt + | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt + | Scall : option ident -> signature -> expr -> exprlist -> stmt + | Salloc : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -87,6 +91,7 @@ Definition funsig (fd: fundef) := *) Definition genv := Genv.t fundef. +Definition letenv := list val. Section RELSEM. @@ -96,101 +101,68 @@ Variable ge: genv. of Cminor. Refer to the description of Cminor semantics for the meaning of the parameters of the predicates. One additional predicate is introduced: - [eval_condexpr ge sp le e m a t m' b], meaning that the conditional + [eval_condexpr ge sp e m le a b], meaning that the conditional expression [a] evaluates to the boolean [b]. *) -Inductive eval_expr: - val -> letenv -> env -> - mem -> expr -> trace -> mem -> val -> Prop := - | eval_Evar: - forall sp le e m id v, +Section EVAL_EXPR. + +Variable sp: val. +Variable e: env. +Variable m: mem. + +Inductive eval_expr: letenv -> expr -> val -> Prop := + | eval_Evar: forall le id v, PTree.get id e = Some v -> - eval_expr sp le e m (Evar id) E0 m v - | eval_Eop: - forall sp le e m op al t m1 vl v, - eval_exprlist sp le e m al t m1 vl -> - eval_operation ge sp op vl m1 = Some v -> - eval_expr sp le e m (Eop op al) t m1 v - | eval_Eload: - forall sp le e m chunk addr al t m1 v vl a, - eval_exprlist sp le e m al t m1 vl -> - eval_addressing ge sp addr vl = Some a -> - Mem.loadv chunk m1 a = Some v -> - eval_expr sp le e m (Eload chunk addr al) t m1 v - | eval_Estore: - forall sp le e m chunk addr al b t t1 m1 vl t2 m2 m3 v a, - eval_exprlist sp le e m al t1 m1 vl -> - eval_expr sp le e m1 b t2 m2 v -> - eval_addressing ge sp addr vl = Some a -> - Mem.storev chunk m2 a v = Some m3 -> - t = t1 ** t2 -> - eval_expr sp le e m (Estore chunk addr al b) t m3 v - | eval_Ecall: - forall sp le e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f, - eval_expr sp le e m a t1 m1 vf -> - eval_exprlist sp le e m1 bl t2 m2 vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - eval_funcall m2 f vargs t3 m3 vres -> - t = t1 ** t2 ** t3 -> - eval_expr sp le e m (Ecall sig a bl) t m3 vres - | eval_Econdition: - forall sp le e m a b c t t1 m1 v1 t2 m2 v2, - eval_condexpr sp le e m a t1 m1 v1 -> - eval_expr sp le e m1 (if v1 then b else c) t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr sp le e m (Econdition a b c) t m2 v2 - | eval_Elet: - forall sp le e m a b t t1 m1 v1 t2 m2 v2, - eval_expr sp le e m a t1 m1 v1 -> - eval_expr sp (v1::le) e m1 b t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr sp le e m (Elet a b) t m2 v2 - | eval_Eletvar: - forall sp le e m n v, + eval_expr le (Evar id) v + | eval_Eop: forall le op al vl v, + eval_exprlist le al vl -> + eval_operation ge sp op vl m = Some v -> + eval_expr le (Eop op al) v + | eval_Eload: forall le chunk addr al vl vaddr v, + eval_exprlist le al vl -> + eval_addressing ge sp addr vl = Some vaddr -> + Mem.loadv chunk m vaddr = Some v -> + eval_expr le (Eload chunk addr al) v + | eval_Econdition: forall le a b c v1 v2, + eval_condexpr le a v1 -> + eval_expr le (if v1 then b else c) v2 -> + eval_expr le (Econdition a b c) v2 + | eval_Elet: forall le a b v1 v2, + eval_expr le a v1 -> + eval_expr (v1 :: le) b v2 -> + eval_expr le (Elet a b) v2 + | eval_Eletvar: forall le n v, nth_error le n = Some v -> - eval_expr sp le e m (Eletvar n) E0 m v - | eval_Ealloc: - forall sp le e m a t m1 n m2 b, - eval_expr sp le e m a t m1 (Vint n) -> - Mem.alloc m1 0 (Int.signed n) = (m2, b) -> - eval_expr sp le e m (Ealloc a) t m2 (Vptr b Int.zero) - -with eval_condexpr: - val -> letenv -> env -> - mem -> condexpr -> trace -> mem -> bool -> Prop := - | eval_CEtrue: - forall sp le e m, - eval_condexpr sp le e m CEtrue E0 m true - | eval_CEfalse: - forall sp le e m, - eval_condexpr sp le e m CEfalse E0 m false - | eval_CEcond: - forall sp le e m cond al t1 m1 vl b, - eval_exprlist sp le e m al t1 m1 vl -> - eval_condition cond vl m1 = Some b -> - eval_condexpr sp le e m (CEcond cond al) t1 m1 b - | eval_CEcondition: - forall sp le e m a b c t t1 m1 vb1 t2 m2 vb2, - eval_condexpr sp le e m a t1 m1 vb1 -> - eval_condexpr sp le e m1 (if vb1 then b else c) t2 m2 vb2 -> - t = t1 ** t2 -> - eval_condexpr sp le e m (CEcondition a b c) t m2 vb2 - -with eval_exprlist: - val -> letenv -> env -> - mem -> exprlist -> trace -> mem -> list val -> Prop := - | eval_Enil: - forall sp le e m, - eval_exprlist sp le e m Enil E0 m nil - | eval_Econs: - forall sp le e m a bl t t1 m1 v t2 m2 vl, - eval_expr sp le e m a t1 m1 v -> - eval_exprlist sp le e m1 bl t2 m2 vl -> - t = t1 ** t2 -> - eval_exprlist sp le e m (Econs a bl) t m2 (v :: vl) + eval_expr le (Eletvar n) v + +with eval_condexpr: letenv -> condexpr -> bool -> Prop := + | eval_CEtrue: forall le, + eval_condexpr le CEtrue true + | eval_CEfalse: forall le, + eval_condexpr le CEfalse false + | eval_CEcond: forall le cond al vl b, + eval_exprlist le al vl -> + eval_condition cond vl m = Some b -> + eval_condexpr le (CEcond cond al) b + | eval_CEcondition: forall le a b c vb1 vb2, + eval_condexpr le a vb1 -> + eval_condexpr le (if vb1 then b else c) vb2 -> + eval_condexpr le (CEcondition a b c) vb2 + +with eval_exprlist: letenv -> exprlist -> list val -> Prop := + | eval_Enil: forall le, + eval_exprlist le Enil nil + | eval_Econs: forall le a1 al v1 vl, + eval_expr le a1 v1 -> eval_exprlist le al vl -> + eval_exprlist le (Econs a1 al) (v1 :: vl). -with eval_funcall: +Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop + with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop + with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop. + +End EVAL_EXPR. + +Inductive eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := | eval_funcall_internal: @@ -212,20 +184,37 @@ with exec_stmt: | exec_Sskip: forall sp e m, exec_stmt sp e m Sskip E0 e m Out_normal - | exec_Sexpr: - forall sp e m a t m1 v, - eval_expr sp nil e m a t m1 v -> - exec_stmt sp e m (Sexpr a) t e m1 Out_normal | exec_Sassign: - forall sp e m id a t m1 v, - eval_expr sp nil e m a t m1 v -> - exec_stmt sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal + forall sp e m id a v, + eval_expr sp e m nil a v -> + exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal + | exec_Sstore: + forall sp e m chunk addr al b vl v vaddr m', + eval_exprlist sp e m nil al vl -> + eval_expr sp e m nil b v -> + eval_addressing ge sp addr vl = Some vaddr -> + Mem.storev chunk m vaddr v = Some m' -> + exec_stmt sp e m (Sstore chunk addr al b) E0 e m' Out_normal + | exec_Scall: + forall sp e m optid sig a bl vf vargs f t m' vres e', + eval_expr sp e m nil a vf -> + eval_exprlist sp e m nil bl vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + eval_funcall m f vargs t m' vres -> + e' = set_optvar optid vres e -> + exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal + | exec_Salloc: + forall sp e m id a n m' b, + eval_expr sp e m nil a (Vint n) -> + Mem.alloc m 0 (Int.signed n) = (m', b) -> + exec_stmt sp e m (Salloc id a) + E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal | exec_Sifthenelse: - forall sp e m a s1 s2 t t1 m1 v1 t2 e2 m2 out, - eval_condexpr sp nil e m a t1 m1 v1 -> - exec_stmt sp e m1 (if v1 then s1 else s2) t2 e2 m2 out -> - t = t1 ** t2 -> - exec_stmt sp e m (Sifthenelse a s1 s2) t e2 m2 out + forall sp e m a s1 s2 v t e' m' out, + eval_condexpr sp e m nil a v -> + exec_stmt sp e m (if v then s1 else s2) t e' m' out -> + exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out | exec_Sseq_continue: forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out, exec_stmt sp e m s1 t1 e1 m1 Out_normal -> @@ -256,41 +245,115 @@ with exec_stmt: forall sp e m n, exec_stmt sp e m (Sexit n) E0 e m (Out_exit n) | exec_Sswitch: - forall sp e m a cases default t1 m1 n, - eval_expr sp nil e m a t1 m1 (Vint n) -> + forall sp e m a cases default n, + eval_expr sp e m nil a (Vint n) -> exec_stmt sp e m (Sswitch a cases default) - t1 e m1 (Out_exit (switch_target n default cases)) + E0 e m (Out_exit (switch_target n default cases)) | exec_Sreturn_none: forall sp e m, exec_stmt sp e m (Sreturn None) E0 e m (Out_return None) | exec_Sreturn_some: - forall sp e m a t m1 v, - eval_expr sp nil e m a t m1 v -> - exec_stmt sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)) + forall sp e m a v, + eval_expr sp e m nil a v -> + exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)) | exec_Stailcall: - forall sp e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f, - eval_expr (Vptr sp Int.zero) nil e m a t1 m1 vf -> - eval_exprlist (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs -> + forall sp e m sig a bl vf vargs f t m' vres, + eval_expr (Vptr sp Int.zero) e m nil a vf -> + eval_exprlist (Vptr sp Int.zero) e m nil bl vargs -> Genv.find_funct ge vf = Some f -> funsig f = sig -> - eval_funcall (Mem.free m2 sp) f vargs t3 m3 vres -> - t = t1 ** t2 ** t3 -> - exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m3 (Out_tailcall_return vres). + eval_funcall (Mem.free m sp) f vargs t m' vres -> + exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m' (Out_tailcall_return vres). + +Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop + with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop. + +(** Coinductive semantics for divergence. *) + +CoInductive evalinf_funcall: + mem -> fundef -> list val -> traceinf -> Prop := + | evalinf_funcall_internal: + forall m f vargs m1 sp e t, + Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> + set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> + execinf_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t -> + evalinf_funcall m (Internal f) vargs t -Scheme eval_expr_ind5 := Minimality for eval_expr Sort Prop - with eval_condexpr_ind5 := Minimality for eval_condexpr Sort Prop - with eval_exprlist_ind5 := Minimality for eval_exprlist Sort Prop - with eval_funcall_ind5 := Minimality for eval_funcall Sort Prop - with exec_stmt_ind5 := Minimality for exec_stmt Sort Prop. +(** [execinf_stmt ge sp e m s t] means that statement [s] diverges. + [e] is the initial environment, [m] is the initial memory state, + and [t] the trace of observable events performed during the execution. *) + +with execinf_stmt: + val -> env -> mem -> stmt -> traceinf -> Prop := + | execinf_Scall: + forall sp e m optid sig a bl vf vargs f t, + eval_expr sp e m nil a vf -> + eval_exprlist sp e m nil bl vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + evalinf_funcall m f vargs t -> + execinf_stmt sp e m (Scall optid sig a bl) t + | execinf_Sifthenelse: + forall sp e m a s1 s2 v t, + eval_condexpr sp e m nil a v -> + execinf_stmt sp e m (if v then s1 else s2) t -> + execinf_stmt sp e m (Sifthenelse a s1 s2) t + | execinf_Sseq_1: + forall sp e m t s1 s2, + execinf_stmt sp e m s1 t -> + execinf_stmt sp e m (Sseq s1 s2) t + | execinf_Sseq_2: + forall sp e m t s1 t1 e1 m1 s2 t2, + exec_stmt sp e m s1 t1 e1 m1 Out_normal -> + execinf_stmt sp e1 m1 s2 t2 -> + t = t1 *** t2 -> + execinf_stmt sp e m (Sseq s1 s2) t + | execinf_Sloop_body: + forall sp e m s t, + execinf_stmt sp e m s t -> + execinf_stmt sp e m (Sloop s) t + | execinf_Sloop_loop: + forall sp e m s t t1 e1 m1 t2, + exec_stmt sp e m s t1 e1 m1 Out_normal -> + execinf_stmt sp e1 m1 (Sloop s) t2 -> + t = t1 *** t2 -> + execinf_stmt sp e m (Sloop s) t + | execinf_Sblock: + forall sp e m s t, + execinf_stmt sp e m s t -> + execinf_stmt sp e m (Sblock s) t + | execinf_Stailcall: + forall sp e m sig a bl vf vargs f t, + eval_expr (Vptr sp Int.zero) e m nil a vf -> + eval_exprlist (Vptr sp Int.zero) e m nil bl vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + evalinf_funcall (Mem.free m sp) f vargs t -> + execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t. End RELSEM. -Definition exec_program (p: program) (t: trace) (r: val) : Prop := - let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in - exists b, exists f, exists m, - Genv.find_symbol ge p.(prog_main) = Some b /\ - Genv.find_funct_ptr ge b = Some f /\ - funsig f = mksignature nil (Some Tint) /\ - eval_funcall ge m0 f nil t m r. +(** Execution of a whole program: [exec_program p beh] + holds if the application of [p]'s main function to no arguments + in the initial memory state for [p] has [beh] as observable + behavior. *) +Inductive exec_program (p: program): program_behavior -> Prop := + | program_terminates: + forall b f t m r, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = mksignature nil (Some Tint) -> + eval_funcall ge m0 f nil t m (Vint r) -> + exec_program p (Terminates t r) + | program_diverges: + forall b f t, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = mksignature nil (Some Tint) -> + evalinf_funcall ge m0 f nil t -> + exec_program p (Diverges t). |