Changeset 1194 for src/Clight/toCminor.ma
- Timestamp:
- Sep 6, 2011, 5:20:19 PM (8 years ago)
- File:
-
- 1 edited
-
src/Clight/toCminor.ma (modified) (2 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/toCminor.ma
r1139 r1194 3 3 include "Clight/TypeComparison.ma". 4 4 include "utilities/lists.ma". 5 (* 6 let rec mem_vars_expr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝ 7 match e with 8 [ Expr ed ty ⇒ 9 match ed with 10 [ Ederef e1 ⇒ mem_vars_expr mem_vars e1 11 | Eaddrof e1 ⇒ mem_vars_addr mem_vars e1 12 | Eunop _ e1 ⇒ mem_vars_expr mem_vars e1 13 | Ebinop _ e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧ 14 mem_vars_expr mem_vars e2 15 | Ecast _ e1 ⇒ mem_vars_expr mem_vars e1 16 | Econdition e1 e2 e3 ⇒ mem_vars_expr mem_vars e1 ∧ 17 mem_vars_expr mem_vars e2 ∧ 18 mem_vars_expr mem_vars e3 19 | Eandbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧ 20 mem_vars_expr mem_vars e2 21 | Eorbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧ 22 mem_vars_expr mem_vars e2 23 | Efield e1 _ ⇒ mem_vars_expr mem_vars e1 24 | Ecost _ e1 ⇒ mem_vars_expr mem_vars e1 25 | _ ⇒ True 26 ] 27 ] 28 and mem_vars_addr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝ 29 match e with 30 [ Expr ed ty ⇒ 31 match ed with 32 [ Evar x ⇒ mem_set ? mem_vars x = true 33 | Ederef e1 ⇒ mem_vars_expr mem_vars e1 34 | Efield e1 _ ⇒ mem_vars_addr mem_vars e1 35 | _ ⇒ False (* not an lvalue *) 36 ] 37 ]. 38 39 let rec mem_vars_stmt (mem_vars:identifier_set SymbolTag) (s:statement) on s : Prop ≝ 40 match s with 41 [ Sskip ⇒ True 42 | Sassign e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧ 43 mem_vars_expr mem_vars e2 44 | Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ] ∧ 45 mem_vars_expr mem_vars e2 ∧ 46 All ? (mem_vars_expr mem_vars) es 47 | Ssequence s1 s2 ⇒ mem_vars_stmt mem_vars s1 ∧ 48 mem_vars_stmt mem_vars s2 49 | Sifthenelse e1 s1 s2 ⇒ mem_vars_expr mem_vars e1 ∧ 50 mem_vars_stmt mem_vars s1 ∧ 51 mem_vars_stmt mem_vars s2 52 | Swhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧ 53 mem_vars_stmt mem_vars s1 54 | Sdowhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧ 55 mem_vars_stmt mem_vars s1 56 | Sfor s1 e1 s2 s3 ⇒ mem_vars_stmt mem_vars s1 ∧ 57 mem_vars_expr mem_vars e1 ∧ 58 mem_vars_stmt mem_vars s2 ∧ 59 mem_vars_stmt mem_vars s3 60 | Sbreak ⇒ True 61 | Scontinue ⇒ True 62 | Sreturn oe1 ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ] 63 | Sswitch e1 ls ⇒ mem_vars_expr mem_vars e1 ∧ 64 mem_vars_ls mem_vars ls 65 | Slabel _ s1 ⇒ mem_vars_stmt mem_vars s1 66 | Sgoto _ ⇒ True 67 | Scost _ s1 ⇒ mem_vars_stmt mem_vars s1 68 ] 69 and mem_vars_ls (mem_vars:identifier_set SymbolTag) (ls:labeled_statements) on ls : Prop ≝ 70 match ls with 71 [ LSdefault s1 ⇒ mem_vars_stmt mem_vars s1 72 | LScase _ s1 ls1 ⇒ mem_vars_stmt mem_vars s1 ∧ 73 mem_vars_ls mem_vars ls1 74 ]. 75 *) 5 6 (* Identify local variables that must be allocated memory. *) 76 7 77 8 let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝ … … 589 520 ] 590 521 ]. 591 (* 592 definition translate_assign ≝ 593 λvars,e1,e2. 594 do e2' ← translate_expr vars e2; 595 do q ← match access_mode (typeof e2) with 596 [ By_value q ⇒ OK ? q 597 | By_reference r ⇒ OK ? (Mpointer r) 598 | By_nothing ⇒ Error ? (msg BadlyTypedAccess) 599 ]; 600 match e1 with 601 [ Expr ed1 ty1 ⇒ 602 match ed1 with 603 [ Evar id ⇒ 604 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); 605 match c with 606 [ Local ⇒ OK ? (St_assign id e2') 607 | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2') 608 | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2') 609 ] 610 | _ ⇒ 611 do e1' ← translate_addr vars e1; 612 OK ? (St_store q e1' e2') 613 ] 614 ]. 615 *) 522 616 523 definition translate_assign ≝ 617 524 λvars,e1,e2.
Note: See TracChangeset
for help on using the changeset viewer.
