Ignore:
Timestamp:
Apr 4, 2012, 6:48:23 PM (8 years ago)
Author:
campbell
Message:

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1680 r1872  
    526526    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
    527527    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
    528     let f ≝ add_fresh_to_graph … (St_op2 op dst r1 r2) f ?? in
     528    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
    529529    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
    530530    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
    531531      «pi1 … f, ?»
    532 | Mem _ _ q e' ⇒ λEnv,dst.
     532| Mem t _ e' ⇒ λEnv,dst.
    533533    let ❬f,r❭ ≝ choose_reg … e' f Env in
    534     let f ≝ add_fresh_to_graph … (St_load q r dst) f ?? in
     534    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
    535535    let f ≝ add_expr … env ? e' Env f «r,?» in
    536536      «pi1 … f, ?»
     
    682682    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
    683683    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
    684 | St_store _ _ q e1 e2 ⇒ λEnv.
     684| St_store t _ e1 e2 ⇒ λEnv.
    685685    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
    686686    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
    687     let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in
     687    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
    688688    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
    689689    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
     
    752752      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    753753      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
    754       let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in
     754      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmpu I8 Unsigned Ceq) (* signed? *) br r cr) f ?? in
    755755      let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
    756756        OK ? «pi1 … f, ?») (OK ? f) tab;
Note: See TracChangeset for help on using the changeset viewer.