Changeset 816 for src/Clight


Ignore:
Timestamp:
May 19, 2011, 3:06:42 PM (9 years ago)
Author:
campbell
Message:

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

Location:
src/Clight
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r776 r816  
    322322        | _ ⇒ None ? ]
    323323      | _ ⇒ None ? ]
    324   | cmp_case_ipip
     324  | cmp_case_ii
    325325      match v1 with
    326326      [ Vint n1 ⇒ match v2 with
     
    328328         | _ ⇒ None ?
    329329         ]
    330       | Vptr r1 b1 p1 ofs1 ⇒
     330      | _ ⇒ None ?     
     331      ]
     332  | cmp_case_pp ⇒
     333      match v1 with
     334      [ Vptr r1 b1 p1 ofs1 ⇒
    331335        match v2 with
    332336        [ Vptr r2 b2 p2 ofs2 ⇒
  • src/Clight/Csyntax.ma

    r797 r816  
    830830inductive classify_cmp_cases : Type[0] ≝
    831831  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
    832   | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
     832  | cmp_case_ii: classify_cmp_cases  (**r int, int*)
     833  | cmp_case_pp: classify_cmp_cases  (**r ptr|array , ptr|array*)
    833834  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
    834835  | cmp_default: classify_cmp_cases . (**r other *)
     
    840841    [ Tint i2 s2 ⇒
    841842      classify_32un_aux ? i1 s1 cmp_case_I32unsi
    842         (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
     843        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ii)
    843844    | _ ⇒ cmp_default ]
    844845  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
    845846  | Tpointer _ _ ⇒
    846847    match ty2 with
    847     [ Tint _ _ ⇒ cmp_case_ipip
    848     | Tpointer _ _ ⇒ cmp_case_ipip
    849     | Tarray _ _ _ ⇒ cmp_case_ipip
     848    [ Tpointer _ _ ⇒ cmp_case_pp
     849    | Tarray _ _ _ ⇒ cmp_case_pp
    850850    | _ ⇒ cmp_default ]
    851851  | Tarray _ _ _ ⇒
    852852    match ty2 with
    853     [ Tint _ _ ⇒ cmp_case_ipip
    854     | Tpointer _ _ ⇒ cmp_case_ipip
    855     | Tarray _ _ _ ⇒ cmp_case_ipip
     853    [ Tpointer _ _ ⇒ cmp_case_pp
     854    | Tarray _ _ _ ⇒ cmp_case_pp
    856855    | _ ⇒ cmp_default ]
    857856  | _ ⇒ cmp_default
  • src/Clight/test/search.ma

    r748 r816  
    193193@refl
    194194qed.
     195
     196include "Clight/toCminor.ma".
     197include "Cminor/semantics.ma".
     198
     199example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     200normalize
     201@refl
     202qed.
     203
     204include "Cminor/toRTLabs.ma".
     205include "RTLabs/semantics.ma".
     206
     207example e2: finishes_with (repr 3) ? (
     208do p1 ← clight_to_cminor myprog;
     209do p2 ← cminor_to_rtlabs p1;
     210 exec_up_to RTLabs_fullexec p2 1000 [ ]).
     211normalize
     212@refl
     213qed.
Note: See TracChangeset for help on using the changeset viewer.