Changeset 1198


Ignore:
Timestamp:
Sep 8, 2011, 4:04:07 PM (8 years ago)
Author:
campbell
Message:

Clight cast removal (NB: quite different from the prototype).

Location:
src
Files:
3 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r1143 r1198  
    7777  of intermediate languages from ERTL on, we need to recover the arguments
    7878  for the function not only from the registers, but also from the stack.
     79
     8008/09/2011:
     81  The Clight cast simplification algorithm is quite different to the prototype's:
     82  it only needs to do a simple pattern match per recursion and copes with deeper
     83  arithmetic expressions such as (char)((int)x + (int)y + (int)z).
  • src/Clight/TypeComparison.ma

    r891 r1198  
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
    9292λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
     93
     94definition type_eq : type → type → bool ≝
     95λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].
     96
  • src/Clight/test/sum.c.ma

    r1139 r1198  
    6060qed.
    6161
     62include "Clight/SimplifyCasts.ma".
     63
     64example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
     65normalize  (* you can examine the result here *)
     66@refl
     67qed.
     68
    6269include "Clight/toCminor.ma".
    6370include "Cminor/semantics.ma".
    6471
    65 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     72example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
    6673normalize
    6774@refl
     
    7279
    7380example e2: finishes_with (repr I32 74) ? (
    74 do p1 ← clight_to_cminor myprog;
     81do p1 ← clight_to_cminor (simplify_program myprog);
    7582do p2 ← cminor_to_rtlabs p1;
    7683 exec_up_to RTLabs_fullexec p2 1000 [ ]).
Note: See TracChangeset for help on using the changeset viewer.