Changeset 1194


Ignore:
Timestamp:
Sep 6, 2011, 5:20:19 PM (8 years ago)
Author:
campbell
Message:

Remove old, commented out code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1139 r1194  
    33include "Clight/TypeComparison.ma".
    44include "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. *)
    767
    778let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
     
    589520        ]
    590521    ].
    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
    616523definition translate_assign ≝
    617524λvars,e1,e2.
Note: See TracChangeset for help on using the changeset viewer.