Changeset 2754


Ignore:
Timestamp:
Mar 1, 2013, 10:26:31 AM (7 years ago)
Author:
sacerdot
Message:
  1. WARNING: I commented out one of James's function used in compiler.ma because it was undefined (partial commit). To be restored.
  2. The type of labelled_object_code programs now has a symbol table, used to generate the intensional events function call/return.
Location:
src
Files:
11 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2708 r2754  
    984984
    985985definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
    986 definition preamble ≝ list (Identifier × Word).
     986(* The first associative list assigns symbol names to addresses in data memory.
     987   The second associative list assigns to Identifiers meant to be entry points
     988   of functions the name of the function (that lives in a different namespace) *)
     989definition preamble ≝ list (Identifier × Word) × (list (Identifier × ident)).
    987990definition assembly_program ≝ list instruction.
    988991definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
     992
     993definition object_code ≝ list Byte.
     994definition costlabel_map ≝ BitVectorTrie costlabel 16.
     995definition symboltable_type ≝ BitVectorTrie ident 16.
     996definition labelled_object_code ≝ object_code × (costlabel_map × symboltable_type).
    989997
    990998(* labels & instructions *)
  • src/ASM/ASMCostsSplit.ma

    r2665 r2754  
    317317   
    318318definition compute_costs ≝
    319   λprogram: list Byte.
     319  λprogram: object_code.
    320320  λcost_labels: BitVectorTrie costlabel 16.
    321321  λcost_labels_injective:
     
    328328
    329329definition ASM_cost_map :
    330   ∀p: (list Byte) × (BitVectorTrie costlabel 16).
     330  ∀p: labelled_object_code.
    331331  let code_memory ≝ load_code_memory (\fst p) in
    332   let a_s ≝ ASM_abstract_status code_memory (\snd p) in
     332  let a_s ≝ ASM_abstract_status code_memory (\fst (\snd p)) in
    333333  ? → as_cost_map a_s ≝
    334334  λp.
    335335  λcost_labels_injective.
    336   let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in
     336  let cost_map ≝ compute_costs (\fst p) (\fst (\snd p)) cost_labels_injective in
    337337  λl_sig.
    338338  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
  • src/ASM/Assembly.ma

    r2707 r2754  
    808808    ∀sigma: Word → Word.
    809809    ∀policy: Word → bool.
    810       Σres:list Byte × (BitVectorTrie costlabel 16).
     810      Σres:labelled_object_code.
    811811       sigma_policy_specification p sigma policy →
    812812       let 〈preamble,instr_list〉 ≝ p in
     
    871871    in
    872872     〈reverse … revcode,
    873       fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
     873      〈fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??),
     874       foldl ??
     875        (λsymboltable,newident_oldident.
     876          let ppc ≝ lookup_labels (\fst newident_oldident) in
     877           insert … (sigma ppc) (\snd newident_oldident) symboltable) (Stub ??) (\snd preamble)〉〉.
    874878  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    875879    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
     
    10281032
    10291033definition assembly_unlabelled_program:
    1030     assembly_program → option (list Byte × (BitVectorTrie Identifier 16))
     1034    assembly_program → option labelled_object_code
    10311035  λp.
    1032     Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
     1036    Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, 〈Stub …, Stub …〉〉).
  • src/ASM/CodeMemory.ma

    r2750 r2754  
    247247(* ***** Object-code ***** JHM: push elsewherein ASM/*.ma? *)
    248248
    249 definition object_code ≝ list Byte.
    250 
    251249inductive nat_bounded : nat → nat → Type[0] ≝
    252250| nat_ok : ∀n,m:nat. nat_bounded n (n+m)
  • src/ASM/CostsProof.ma

    r2671 r2754  
    283283
    284284include alias "ASM/BitVectorTrie.ma".
    285 
    286 (*
    287 let rec compute_cost_trace_label_label
    288   (cm: BitVectorTrie Byte 16)
    289   (cost_labels: BitVectorTrie costlabel 16)
    290    (trace_ends_flag: trace_ends_with_ret)
    291     (start_status: Status cm) (final_status: Status cm)
    292       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
    293         start_status final_status) on the_trace:
    294          list (Σk:costlabel. ∃pc: Word. lookup_opt … pc cost_labels = Some … k) ≝
    295   match the_trace with
    296   [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    297      let pc ≝ program_counter ? cm initial in
    298      let label ≝
    299       match lookup_opt … pc cost_labels return λx: option ?. x ≠ None … → costlabel with
    300       [ None ⇒ λabs. ⊥
    301       | Some l ⇒ λ_. l ] labelled_proof in
    302       (mk_Sig ?? label ?)::compute_cost_trace_any_label cm cost_labels ends_flag initial final … given_trace
    303   ]
    304 and compute_cost_trace_any_label
    305   (cm: BitVectorTrie Byte 16)
    306   (cost_labels: BitVectorTrie costlabel 16)
    307   (trace_ends_flag: trace_ends_with_ret)
    308    (start_status: Status cm) (final_status: Status cm)
    309      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    310        on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
    311   match the_trace with
    312   [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    313   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    314       compute_cost_trace_label_return … call_trace
    315   | tal_base_return the_status _ _ _ ⇒ [ ]
    316   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    317      _ _ _ call_trace _ final_trace ⇒
    318       let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
    319       let final_cost_trace ≝ compute_cost_trace_any_label cm cost_labels end_flag … final_trace in
    320         call_cost_trace @ final_cost_trace
    321   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    322        compute_cost_trace_any_label cm cost_labels end_flag
    323         status_init status_end tail_trace
    324   ]
    325 and compute_cost_trace_label_return
    326   (cm: BitVectorTrie Byte 16)
    327   (cost_labels: BitVectorTrie costlabel 16)
    328   (start_status: Status cm) (final_status: Status cm)
    329     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
    330       on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
    331   match the_trace with
    332   [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label cm … trace_to_lift
    333   | tlr_step initial labelled final labelled_trace ret_trace ⇒
    334       let labelled_cost ≝ compute_cost_trace_label_label cm … labelled_trace in
    335       let return_cost ≝ compute_cost_trace_label_return cm … ret_trace in
    336         labelled_cost @ return_cost
    337   ].
    338  [1:
    339   %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
    340    whd in match (as_costed ??); whd in match (as_label ??); normalize nodelta
    341    cases (lookup_opt costlabel … (program_counter … initial) cost_labels)
    342    normalize
    343   [ #abs cases abs #absurd @⊥ @absurd % | // ]
    344  | cases abs #absurd @absurd % ]
    345 qed.
    346 *)
    347 
    348285include alias "arithmetics/nat.ma".
    349286include alias "basics/logic.ma".
    350 
    351287include alias "arithmetics/bigops.ma".
    352288
     
    737673
    738674lemma tech_cost_sum_eq_as_cost :
    739   ∀compiled_code: (list Byte) × (BitVectorTrie costlabel 16).
    740   let cost_labels ≝ \snd compiled_code in
     675  ∀compiled_code: labelled_object_code.
     676  let cost_labels ≝ \fst (\snd compiled_code) in
    741677  ∀cost_labels_injective:
    742678   (∀pc,pc',l.
    743      lookup_opt … pc (\snd  compiled_code) = Some … l
    744      → lookup_opt … pc' (\snd  compiled_code) = Some … l → pc = pc').
    745   let cost_map ≝ compute_costs (\fst compiled_code) (\snd compiled_code) cost_labels_injective in
     679     lookup_opt … pc cost_labels = Some … l
     680     → lookup_opt … pc' cost_labels = Some … l → pc = pc').
     681  let cost_map ≝ compute_costs (\fst compiled_code) (\fst (\snd compiled_code)) cost_labels_injective in
    746682  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    747683  ∀trace.
  • src/ASM/Fetch.ma

    r2516 r2754  
    182182
    183183definition load_code_memory0:
    184  ∀program: list Byte. Σres: BitVectorTrie Byte 16.
     184 ∀program: object_code. Σres: BitVectorTrie Byte 16.
    185185  let program_size ≝ |program| in
    186186   program_size ≤ 2^16 →
     
    220220qed.
    221221
    222 definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
     222definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
    223223 λprogram.load_code_memory0 program.
    224224
    225225lemma load_code_memory_ok:
    226  ∀program: list Byte.
     226 ∀program: object_code.
    227227  let program_size ≝ |program| in
    228228   program_size ≤ 2^16 →
  • src/ASM/Interpret2.ma

    r2516 r2754  
    3737(* Transition system on the object code *)
    3838
    39 (*CSC: move this definition elsewhere *)
    40 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
    41 
    42 definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
     39definition make_global: labelled_object_code → BitVectorTrie costlabel 16 ≝ \snd.
    4340
    4441definition execute_1_instruction:
     
    5552definition exec: trans_system io_out io_in ≝
    5653 mk_trans_system … is_final execute_1_instruction.
     54*)
     55
     56axiom exec: trans_system io_out io_in.
    5757
    5858definition ASM_fullexec: fullexec io_out io_in ≝
    59  mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).
    60 *)
     59 mk_fullexec ??? exec make_global ?(*(λp.OK … (load (\fst p) (initialise_status … (Stub ??))))*).
     60
    6161axiom ASM_fullexec: fullexec io_out io_in.
  • src/ASM/Status.ma

    r2710 r2754  
    10891089      let 〈carry, sum〉 ≝ half_add … addr size in
    10901090        〈add ? ? datalabels name addr, sum〉)
    1091           〈empty_map …, zero 16〉 the_preamble).
     1091          〈empty_map …, zero 16〉 (\fst the_preamble)).
  • src/BACKEND_BROKEN_FILES

    r2715 r2754  
    1010
    1111ASM/AssemblyProofSplitSplit.ma:   nuove istruzioni
    12   ASM/AssemblyProofSpli.ma:       nuove istruzioni
     12  ASM/AssemblyProofSplit.ma:       nuove istruzioni
    1313    ASM/AssemblyProof.ma:         nuove istruzioni
    1414      ASM/StatusProofSplit.ma     nuove istruzioni
  • src/LIN/LINToASM.ma

    r2708 r2754  
    352352    ].
    353353
     354definition get_symboltable :
     355  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
     356  λglobals,u.
     357  let imap ≝ ident_map … u in
     358  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
     359  〈u, foldi ??? f imap [ ]〉.
     360
    354361definition lin_to_asm : lin_program → pseudo_assembly_program ≝
    355362  λp.
     
    364371     ! main ← Identifier_of_ident … (prog_main … p) ;
    365372     let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     373     ! symboltable ← get_symboltable … ;
    366374     (* atm no data identifier is used in the code, so preamble must be empty *)
    367      return 〈[ ], code〉).
     375     return 〈[ ], symboltable, code〉).
  • src/compiler.ma

    r2753 r2754  
    4141          lin_to_asm p.
    4242
    43 (* JHM: object_code and program_size_ok defns added *)
    44 include "ASM/CodeMemory.ma".
    45 
    4643include "ASM/Policy.ma".
    4744(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
     
    5350   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
    5451   
    55 definition assembler : pseudo_assembly_program → res (object_code × costlabel_map)
     52definition assembler : pseudo_assembly_program → res labelled_object_code
    5653λp.
    5754  let 〈preamble, list_instr〉 ≝ p in
    58   ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) (program_ok_opt ? list_instr);
     55  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*);
    5956  let p' ≝ 〈preamble, list_instr〉 in
    6057  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
     
    6259  let pol ≝ λppc. \snd sigma_pol ppc in
    6360  OK ? (assembly p sigma pol).
    64   % [1: @list_instr_ok | cases daemon]
     61  (* % [1: @list_instr_ok | cases daemon] *) cases daemon
    6562qed.
    6663
     
    103100
    104101definition compile : clight_program →
    105   res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
     102  res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
    106103λp.
    107104  ! 〈init_cost,p',p〉 ← front_end p;
     
    112109    p'
    113110    (load_code_memory (\fst p))
    114     (\snd p)
     111    (\fst (\snd p))
    115112    k
    116113    in
Note: See TracChangeset for help on using the changeset viewer.