Changeset 1352


Ignore:
Timestamp:
Oct 11, 2011, 12:45:16 PM (8 years ago)
Author:
sacerdot
Message:

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1350 r1352  
    44
    55include "basics/jmeq.ma".
     6include alias "basics/logic.ma".
    67
    78(* A "single execution" - where all of the input values are made explicit. *)
  • src/Clight/TypeComparison.ma

    r1350 r1352  
    8787        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    8888        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    89 ]. try destruct // (*Wilmer:XXXX*) cases daemon qed.
     89]. (*Wilmer:XXXX try destruct //*) cases daemon qed.
    9090
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
  • src/Cminor/semantics.ma

    r1351 r1352  
    1 
    21include "common/Events.ma".
    32include "common/Mem.ma".
     
    76
    87include "Cminor/syntax.ma".
     8include alias "basics/logic.ma".
    99
    1010definition env ≝ identifier_map SymbolTag val.
  • src/ERTL/ERTLToLTL.ma

    r1282 r1352  
    199199    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
    200200    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
    201       〈add_graph globals original_label (sequential (ltl_params globals) globals (INT globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
     201      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT ? globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
    202202
    203203definition translate_statement:
  • src/RTL/RTLToERTL.ma

    r1322 r1352  
    118118    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
    119119    let defaults ≝ map … f_default restl in
    120       adds_graph ertl_params1 (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     120      adds_graph ertl_params1 ? (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    121121  ].
    122122
  • src/RTLabs/RTLabsToRTL.ma

    r1343 r1352  
    55include "common/Graphs.ma".
    66include "joint/TranslateUtils.ma".
     7include alias "ASM/BitVector.ma".
     8include alias "arithmetics/nat.ma".
    79
    810let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
  • src/joint/TranslateUtils.ma

    r1284 r1352  
    5858definition adds_graph ≝
    5959 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
    60   add_translates … (map (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
     60  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
  • src/joint/semantics.ma

    r1329 r1352  
    285285        ! st ← pair_reg_move … st dst_src ;
    286286          ret ? 〈E0, next … l st〉
    287       (*CSC: XXX bug here dest unused *)
    288287      | CALL_ID id argsno dest ⇒
    289288        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    292291          [ Internal fn ⇒
    293292            ! st ← save_ra … st l;
    294               let st ≝ save_frame … st in
     293              let st ≝ save_frame … dest st in
    295294              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     295+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
     296+ ALLOCARE LO STACK FRAME
    296297              let l' ≝ joint_if_entry … fn in
    297298             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
     
    307308          ]]
    308309    | RETURN ⇒
     310+ CHIAMARE UNA FUNZIONE PER ANDARE A SOSTITUIRE IL VALORE TROVATO NEL REGISTRO
     311DI RITORNO DELLA FUNZIONE AL POSTO GIUSTO
     312+ DEALLOCARE LO STACK FRAME
    309313      ! st ← pop_frame … st;
    310314      ! 〈st,pch〉 ← pop … st;
Note: See TracChangeset for help on using the changeset viewer.