Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r485 r487  
    3636  the null pointer) and the float 0.0 are false. *)
    3737
    38 ninductive is_false: val → type → Prop ≝
     38inductive is_false: val → type → Prop ≝
    3939  | is_false_int: ∀sz,sg.
    4040      is_false (Vint zero) (Tint sz sg)
     
    4444      is_false (Vfloat Fzero) (Tfloat sz).
    4545
    46 ninductive is_true: val → type → Prop ≝
     46inductive is_true: val → type → Prop ≝
    4747  | is_true_int_int: ∀n,sz,sg.
    4848      n ≠ zero →
     
    5454      is_true (Vfloat f) (Tfloat sz).
    5555
    56 ninductive bool_of_val : val → type → val → Prop ≝
     56inductive bool_of_val : val → type → val → Prop ≝
    5757  | bool_of_val_true: ∀v,ty.
    5858         is_true v ty →
     
    7070  promoted [e2] to a float. *)
    7171
    72 nlet rec sem_neg (v: val) (ty: type) : option val ≝
     72let rec sem_neg (v: val) (ty: type) : option val ≝
    7373  match ty with
    7474  [ Tint _ _ ⇒
     
    8585  ].
    8686
    87 nlet rec sem_notint (v: val) : option val ≝
     87let rec sem_notint (v: val) : option val ≝
    8888  match v with
    8989  [ Vint n ⇒ Some ? (Vint (xor n mone))
     
    9191  ].
    9292
    93 nlet rec sem_notbool (v: val) (ty: type) : option val ≝
     93let rec sem_notbool (v: val) (ty: type) : option val ≝
    9494  match ty with
    9595  [ Tint _ _ ⇒
     
    113113  ].
    114114
    115 nlet rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     115let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    116116  match classify_add t1 t2 with
    117117  [ add_case_ii ⇒                       (**r integer addition *)
     
    145145].
    146146
    147 nlet rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     147let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    148148  match classify_sub t1 t2 with
    149149  [ sub_case_ii ⇒                (**r integer subtraction *)
     
    179179  ].
    180180
    181 nlet rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     181let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    182182 match classify_mul t1 t2 with
    183183  [ mul_case_ii ⇒
     
    197197].
    198198
    199 nlet rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     199let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    200200  match classify_div t1 t2 with
    201201  [ div_case_I32unsi ⇒
     
    221221  ].
    222222
    223 nlet rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     223let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    224224  match classify_mod t1 t2 with
    225225  [ mod_case_I32unsi ⇒
     
    239239  ].
    240240
    241 nlet rec sem_and (v1,v2: val) : option val ≝
     241let rec sem_and (v1,v2: val) : option val ≝
    242242  match v1 with
    243243  [ Vint n1 ⇒ match v2 with
     
    247247  ].
    248248
    249 nlet rec sem_or (v1,v2: val) : option val ≝
     249let rec sem_or (v1,v2: val) : option val ≝
    250250  match v1 with
    251251  [ Vint n1 ⇒ match v2 with
     
    255255  ].
    256256
    257 nlet rec sem_xor (v1,v2: val) : option val ≝
     257let rec sem_xor (v1,v2: val) : option val ≝
    258258  match v1 with
    259259  [ Vint n1 ⇒ match v2 with
     
    263263  ].
    264264
    265 nlet rec sem_shl (v1,v2: val): option val ≝
     265let rec sem_shl (v1,v2: val): option val ≝
    266266  match v1 with
    267267  [ Vint n1 ⇒ match v2 with
     
    271271  | _ ⇒ None ? ].
    272272
    273 nlet rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝
     273let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝
    274274  match classify_shr t1 t2 with
    275275  [ shr_case_I32unsi ⇒
     
    291291   ].
    292292
    293 nlet rec sem_cmp_mismatch (c: comparison): option val ≝
     293let rec sem_cmp_mismatch (c: comparison): option val ≝
    294294  match c with
    295295  [ Ceq =>  Some ? Vfalse
     
    298298  ].
    299299
    300 nlet rec sem_cmp_match (c: comparison): option val ≝
     300let rec sem_cmp_match (c: comparison): option val ≝
    301301  match c with
    302302  [ Ceq =>  Some ? Vtrue
     
    305305  ].
    306306 
    307 nlet rec sem_cmp (c:comparison)
     307let rec sem_cmp (c:comparison)
    308308                  (v1: val) (t1: type) (v2: val) (t2: type)
    309309                  (m: mem): option val ≝
     
    349349  ].
    350350
    351 ndefinition sem_unary_operation
     351definition sem_unary_operation
    352352            : unary_operation → val → type → option val ≝
    353353  λop,v,ty.
     
    358358  ].
    359359
    360 nlet rec sem_binary_operation
     360let rec sem_binary_operation
    361361    (op: binary_operation)
    362362    (v1: val) (t1: type) (v2: val) (t2:type)
     
    385385  resulting in value [v2].  *)
    386386
    387 nlet rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝
     387let rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝
    388388  match sz with
    389389  [ I8 ⇒ match sg with [ Signed ⇒ sign_ext 8 i | Unsigned ⇒ zero_ext 8 i ]
     
    392392  ].
    393393
    394 nlet rec cast_int_float (si : signedness) (i: int) : float ≝
     394let rec cast_int_float (si : signedness) (i: int) : float ≝
    395395  match si with
    396396  [ Signed ⇒ floatofint i
     
    398398  ].
    399399
    400 nlet rec cast_float_int (si : signedness) (f: float) : int ≝
     400let rec cast_float_int (si : signedness) (f: float) : int ≝
    401401  match si with
    402402  [ Signed ⇒ intoffloat f
     
    404404  ].
    405405
    406 nlet rec cast_float_float (sz: floatsize) (f: float) : float ≝
     406let rec cast_float_float (sz: floatsize) (f: float) : float ≝
    407407  match sz with
    408408  [ F32 ⇒ singleoffloat f
     
    410410  ].
    411411
    412 ninductive type_region : type → region → Prop ≝
     412inductive type_region : type → region → Prop ≝
    413413| type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s
    414414| type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s
     
    416416| type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code.
    417417
    418 ninductive cast : mem → val → type → type → val → Prop ≝
     418inductive cast : mem → val → type → type → val → Prop ≝
    419419  | cast_ii:   ∀m,i,sz2,sz1,si1,si2.            (**r int to int  *)
    420420      cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2)
     
    448448  and function pointers to their definitions.  (See module [Globalenvs].) *)
    449449
    450 ndefinition genv ≝ (genv_t Genv) fundef.
     450definition genv ≝ (genv_t Genv) fundef.
    451451
    452452(* * The local environment maps local variables to block references.
     
    454454  block. *)
    455455
    456 ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
    457 
    458 ndefinition empty_env: env ≝ (empty …).
     456definition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
     457
     458definition empty_env: env ≝ (empty …).
    459459
    460460(* * [load_value_of_type ty m b ofs] computes the value of a datum
     
    464464  reference, the pointer [Vptr b ofs] is returned. *)
    465465
    466 nlet rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝
     466let rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝
    467467  match access_mode ty with
    468468  [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs)
     
    476476  This is allowed only if [ty] indicates an access by value. *)
    477477
    478 nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝
     478let rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝
    479479  match access_mode ty_dest with
    480480  [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v
     
    490490  and memory state. *)
    491491
    492 ninductive alloc_variables: env → mem →
     492inductive alloc_variables: env → mem →
    493493                            list (ident × type) →
    494494                            env → mem → Prop ≝
     
    507507  [m1] is the initial memory state and [m2] the final memory state. *)
    508508
    509 ninductive bind_parameters: env →
     509inductive bind_parameters: env →
    510510                           mem → list (ident × type) → list val →
    511511                           mem → Prop ≝
     
    525525(* * Return the list of blocks in the codomain of [e]. *)
    526526
    527 ndefinition blocks_of_env : env → list block ≝ λe.
     527definition blocks_of_env : env → list block ≝ λe.
    528528  map ?? (λx. snd ?? x) (elements ??? e).
    529529
     
    531531  of the selector expression. *)
    532532
    533 nlet rec select_switch (n: int) (sl: labeled_statements)
     533let rec select_switch (n: int) (sl: labeled_statements)
    534534                       on sl : labeled_statements ≝
    535535  match sl with
     
    540540(* * Turn a labeled statement into a sequence *)
    541541
    542 nlet rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝
     542let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝
    543543  match sl with
    544544  [ LSdefault s ⇒ s
     
    562562  [e] is the current environment and [m] is the current memory state. *)
    563563
    564 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
     564inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
    565565  | eval_Econst_int:   ∀i,ty.
    566566      eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0
     
    648648      eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs tr.
    649649
    650 nlet rec eval_expr_ind (ge:genv) (e:env) (m:mem)
     650let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
    651651  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    652652  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
     
    684684  ].
    685685
    686 ninverter eval_expr_inv_ind for eval_expr : Prop.
    687 
    688 nlet rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
     686inverter eval_expr_inv_ind for eval_expr : Prop.
     687
     688let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
    689689  (P:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
    690690  (lvl:∀id,l,ty,H. P ????? (eval_Evar_local ge e m id l ty H))
     
    706706*)
    707707
    708 ndefinition eval_lvalue_inv_ind :
     708definition eval_lvalue_inv_ind :
    709709  ∀x1: genv.
    710710   ∀x2: env.
     
    755755                                     (refl int x7) (refl trace x8)))
    756756                                  ?)))))))))))))))).
    757 ##[ napply (eval_lvalue_ind x1 x2 x3 (λa,psp,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e2:eq ? x5 psp. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a psp loc ofs tr) … Hterm);
    758   ##[ napply H1 ##| napply H2 ##| napply H3 ##| napply H4 ##| napply H5 ##]
    759 ##| ##*: ##skip
    760 ##] nqed.
    761 
    762 nlet rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
     757[ @(eval_lvalue_ind x1 x2 x3 (λa,psp,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e2:eq ? x5 psp. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a psp loc ofs tr) … Hterm)
     758  [ @H1 | @H2 | @H3 | @H4 | @H5 ]
     759| *: skip
     760] qed.
     761
     762let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
    763763  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    764764  (Q:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
     
    834834  ].
    835835
    836 ndefinition combined_expr_lvalue_ind ≝
     836definition combined_expr_lvalue_ind ≝
    837837λge,e,m,P,Q,eci,ecF,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. 
    838838conj ??
     
    852852  expressions [al] to their values [vl]. *)
    853853
    854 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝
     854inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝
    855855  | eval_Enil:
    856856      eval_exprlist ge e m (nil ?) (nil ?) E0
     
    866866(* * Continuations *)
    867867
    868 ninductive cont: Type :=
     868inductive cont: Type[0] :=
    869869  | Kstop: cont
    870870  | Kseq: statement -> cont -> cont
     
    887887(* * Pop continuation until a call or stop *)
    888888
    889 nlet rec call_cont (k: cont) : cont :=
     889let rec call_cont (k: cont) : cont :=
    890890  match k with
    891891  [ Kseq s k => call_cont k
     
    898898  ].
    899899
    900 ndefinition is_call_cont : cont → Prop ≝ λk.
     900definition is_call_cont : cont → Prop ≝ λk.
    901901  match k with
    902902  [ Kstop => True
     
    907907(* * States *)
    908908
    909 ninductive state: Type :=
     909inductive state: Type[0] :=
    910910  | State:
    911911      ∀f: function.
     
    927927  corresponding to a label *)
    928928
    929 nlet rec find_label (lbl: label) (s: statement) (k: cont)
     929let rec find_label (lbl: label) (s: statement) (k: cont)
    930930                    on s: option (statement × cont) :=
    931931  match s with
     
    977977
    978978(* Strip off outer pointer for use when comparing function types. *)
    979 ndefinition fun_typeof ≝
     979definition fun_typeof ≝
    980980λe. match typeof e with
    981981[ Tvoid ⇒ Tvoid
     
    992992(* XXX: note that cost labels in exprs expose a particular eval order. *)
    993993
    994 ninductive step (ge:genv) : state → trace → state → Prop ≝
     994inductive step (ge:genv) : state → trace → state → Prop ≝
    995995
    996996  | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
     
    11721172  through the execution of a [break], [continue] or [return] statement. *)
    11731173
    1174 ninductive outcome: Type :=
     1174inductive outcome: Type[0] :=
    11751175   | Out_break: outcome                 (**r terminated by [break] *)
    11761176   | Out_continue: outcome              (**r terminated by [continue] *)
     
    11781178   | Out_return: option val -> outcome. (**r terminated by [return] *)
    11791179
    1180 ninductive out_normal_or_continue : outcome -> Prop :=
     1180inductive out_normal_or_continue : outcome -> Prop :=
    11811181  | Out_normal_or_continue_N: out_normal_or_continue Out_normal
    11821182  | Out_normal_or_continue_C: out_normal_or_continue Out_continue.
    11831183
    1184 ninductive out_break_or_return : outcome -> outcome -> Prop :=
     1184inductive out_break_or_return : outcome -> outcome -> Prop :=
    11851185  | Out_break_or_return_B: out_break_or_return Out_break Out_normal
    11861186  | Out_break_or_return_R: ∀ov.
     
    12071207  evaluation. *)
    12081208
    1209 ninductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
     1209inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
    12101210  | exec_Sskip:   ∀e,m.
    12111211      exec_stmt e m Sskip
     
    13681368  trace of observable events performed during the execution. *)
    13691369
    1370 Coninductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
     1370Coinductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
    13711371  | execinf_Scall_none:   ∀e,m,a,al,vf,vargs,f,t.
    13721372      eval_expr e m a vf ->
     
    14751475  without arguments and with an empty continuation. *)
    14761476
    1477 ninductive initial_state (p: clight_program): state -> Prop :=
     1477inductive initial_state (p: clight_program): state -> Prop :=
    14781478  | initial_state_intro: ∀b,f,ge,m0.
    14791479      globalenv Genv ?? p = OK ? ge →
     
    14851485(* * A final state is a [Returnstate] with an empty continuation. *)
    14861486
    1487 ninductive final_state: state -> int -> Prop :=
     1487inductive final_state: state -> int -> Prop :=
    14881488  | final_state_intro: ∀r,m.
    14891489      final_state (Returnstate (Vint r) Kstop m) r.
     
    14941494  behavior. *)
    14951495
    1496 ndefinition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
     1496definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    14971497  ∀ge. globalenv ??? p = OK ? ge →
    14981498  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
     
    15001500(** Big-step execution of a whole program.  *)
    15011501
    1502 ninductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
     1502inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
    15031503  | bigstep_program_terminates_intro: ∀b,f,m1,t,r.
    15041504      let ge := Genv.globalenv p in
     
    15091509      bigstep_program_terminates p t r.
    15101510
    1511 ninductive bigstep_program_diverges (p: program): traceinf -> Prop :=
     1511inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
    15121512  | bigstep_program_diverges_intro: ∀b,f,t.
    15131513      let ge := Genv.globalenv p in
     
    15321532       (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y).
    15331533
    1534 ninductive outcome_state_match
     1534inductive outcome_state_match
    15351535       (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
    15361536  | osm_normal:
Note: See TracChangeset for help on using the changeset viewer.