Ignore:
Timestamp:
Jan 15, 2013, 3:58:12 PM (7 years ago)
Author:
garnier
Message:

Some progress on CL to CM.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2572 r2582  
    336336(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    337337| add_case_pi n ty sz sg ⇒
    338     λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     338    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    339339| add_case_ip n sz sg ty ⇒
    340     λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     340    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddip I16) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))) (fix_ptr_type … e2))
    341341| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    342342].
     
    354354| sub_case_pp n1 n2 ty1 ty2 ⇒
    355355    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
    356     [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2))))))
     356    [ Tint sz sg ⇒
     357      (* XXX we make the constant unsigned to match CL semantics. *)
     358      (* OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2)))))) *)
     359         OK ? (Op1 ?? (Ocastint I16 Unsigned sz sg) (Op2 ??? (Odivu I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Unsigned (repr ? (sizeof ty2))))))     
    357360    | _ ⇒ Error ? (msg TypeMismatch)
    358361    ]
     
    504507    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
    505508  | #n #sz #sg #ty0 #E1 #E2 #E3 destruct >E3 #E4
    506     @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)| % // ]
     509    @(typ_equals … E4) % [ 2: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) | 1: % // ]
    507510  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    508511  ]
     
    792795            [ By_value t ⇒
    793796                OK ? «Mem t (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
    794                                    (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»
     797                                   (Oaddpi …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»
    795798            | By_reference ⇒
    796799(*                do e1' ← region_should_eq r r' ? e1';*)
    797800                OK ? «Op2 ASTptr (ASTint I16 Signed (* XXX efficiency? *)) ASTptr
    798                         (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»
     801                        (Oaddpi …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»
    799802            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    800803            ]
     
    841844          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)*)
    842845             OK ? «Op2 ASTptr (ASTint I16 Signed (* FIXME inefficient?*)) ASTptr
    843                    (Oaddp I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?»
     846                   (Oaddpi I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?»
    844847      | Tunion _ _ ⇒ translate_addr vars e1
    845848      | _ ⇒ Error ? (msg BadlyTypedAccess)
Note: See TracChangeset for help on using the changeset viewer.