Changeset 2752 for src


Ignore:
Timestamp:
Feb 28, 2013, 2:36:34 PM (7 years ago)
Author:
mckinna
Message:

Fixed TODO regarding length of list_instr
Added ASM/CodeMemory.ma to incorporate miscellany on program size, memory etc.
Added final(?) error message

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2745 r2752  
    33include "Clight/switchRemoval.ma".
    44include "Clight/toCminor.ma".
    5 include "Cminor/initialisation.ma".
    65include "Cminor/toRTLabs.ma".
    76include "RTLabs/CostCheck.ma".
     
    4241          lin_to_asm p.
    4342
    44 (* JHM: minimum needed for assembler to typecheck *)
    45 (* JHM: moved from ASMCostsSplit.ma               *)
    46 (* JHM: should move elsewhere in ASM/             *)
    47 definition object_code ≝ list Byte.
    48 definition costlabel_map ≝ BitVectorTrie costlabel 16.
     43(* JHM: object_code and program_size_ok defns added *)
     44include "ASM/CodeMemory.ma".
    4945
    5046include "ASM/Policy.ma".
     
    5652   let 〈sigma,policy〉≝ sigma_policy in
    5753   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
    58 
     54   
    5955definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
    6056λp.
    6157  let 〈preamble, list_instr〉 ≝ p in
    62   (* TODO: fail if p is too large. *)
     58  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) (program_ok_opt ? list_instr);
    6359  let p' ≝ 〈preamble, list_instr〉 in
    6460  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
     
    6662  let pol ≝ λppc. \snd sigma_pol ppc in
    6763  OK ? (assembly p sigma pol).
    68 cases daemon
     64  % [1: @list_instr_ok | cases daemon]
    6965qed.
    7066
Note: See TracChangeset for help on using the changeset viewer.