Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (8 years ago)
Author:
ayache
Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

Location:
Deliverables/D2.2/8051/src/LIN
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/LIN/LIN.mli

    r818 r1462  
    6767  | St_call_id of AST.ident
    6868
     69  (* Call to a function given its address. Parameter are the registers holding
     70     the address of the function. *)
     71  | St_call_ptr of I8051.register * I8051.register
     72
    6973  (* Branch on A accumulator. Parameter is the label to go to when the A
    7074     accumulator is not 0. *)
  • Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

    r818 r1462  
    166166  set_result st vs
    167167
    168 let interpret_call st f =
    169   let ptr = Mem.find_global st.mem f in
     168let interpret_call st ptr =
    170169  match Mem.find_fun_def st.mem ptr with
    171170    | LIN.F_int def ->
     
    271270
    272271    | LIN.St_call_id f ->
    273       interpret_call st f
     272      interpret_call st (Mem.find_global st.mem f)
     273
     274    | LIN.St_call_ptr (f1, f2) ->
     275      let addr = List.map (fun r -> get_reg r st) [f1 ; f2] in
     276      interpret_call st addr
    274277
    275278    | LIN.St_condacc lbl_true ->
  • Deliverables/D2.2/8051/src/LIN/LINPrinter.ml

    r818 r1462  
    5454    Printf.sprintf "movex @DPTR, %s" print_a
    5555  | LIN.St_call_id f -> Printf.sprintf "call \"%s\"" f
     56  | LIN.St_call_ptr (f1, f2) ->
     57    Printf.sprintf "call_ptr [%s ; %s]" (print_reg f1) (print_reg f2)
    5658  | LIN.St_condacc lbl_true ->
    5759    Printf.sprintf "branch %s <> 0, %s" print_a lbl_true
  • Deliverables/D2.2/8051/src/LIN/LINToASM.ml

    r818 r1462  
    4545
    4646
    47 let translate_statement glbls_addr = function
     47let call_ptr_instrs f1 f2 =
     48  [LIN.St_to_acc f1 ;
     49   LIN.St_push ;
     50   LIN.St_to_acc f2 ;
     51   LIN.St_push ;
     52   LIN.St_return]
     53
     54let rec translate_statement glbls_addr set_ra_label = function
    4855  | LIN.St_goto lbl -> [`Jmp lbl]
    4956  | LIN.St_label lbl -> [`Label lbl]
     
    5865  | LIN.St_addr x when List.mem_assoc x glbls_addr ->
    5966    [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))]
    60   | LIN.St_addr x ->
     67  | LIN.St_addr x (* TODO *) ->
    6168    error ("unknown global " ^ x ^ ".")
    6269  | LIN.St_from_acc r ->
     
    94101  | LIN.St_call_id f ->
    95102    [`Call f]
     103  | LIN.St_call_ptr (f1, f2) ->
     104    translate_code glbls_addr set_ra_label
     105      (LIN.St_call_id set_ra_label :: (call_ptr_instrs f1 f2))
    96106  | LIN.St_condacc lbl ->
    97107    [`WithLabel (`JNZ (`Label lbl))]
     
    99109    [`RET]
    100110
    101 let translate_code glbls_addr code =
    102   List.flatten (List.map (translate_statement glbls_addr) code)
     111and translate_code glbls_addr set_ra_label code =
     112  List.flatten (List.map (translate_statement glbls_addr set_ra_label) code)
    103113
    104114
     115let translate_fun_def glbls_addr set_ra_label (id, def) =
     116  let code = match def with
     117  | LIN.F_int code -> translate_code glbls_addr set_ra_label code
     118  | LIN.F_ext ext -> [`NOP] in
     119  (`Label id) :: code
     120
     121(*
    105122let translate_fun_def glbls_addr (id, def) = match def with
    106123  | LIN.F_int code -> (`Label id) :: (translate_code glbls_addr code)
    107124  | LIN.F_ext ext ->
    108125    error ("potential call to unsupported external " ^ ext.AST.ef_tag ^ ".")
     126*)
    109127
    110 let translate_functs glbls_addr exit_label main functs =
     128let fun_set_ra set_ra_label =
     129  let size = 0 (* TODO *) in
     130  [LIN.St_label set_ra_label ;
     131   LIN.St_pop ;
     132   LIN.St_from_acc I8051.st1 ;
     133   LIN.St_pop ;
     134   LIN.St_from_acc I8051.st0 ;
     135   LIN.St_int (I8051.a, size) ;
     136   LIN.St_op2 (I8051.Add, I8051.st0) ;
     137   LIN.St_push ;
     138   LIN.St_op2 (I8051.Addc, I8051.st1) ;
     139   LIN.St_push ;
     140   LIN.St_to_acc I8051.st0 ;
     141   LIN.St_push ;
     142   LIN.St_to_acc I8051.st1 ;
     143   LIN.St_push ;
     144   LIN.St_return]
     145
     146let translate_functs glbls_addr exit_label set_ra_label main functs =
    111147  let preamble = match main with
    112148    | None -> []
     
    116152       `Call main ;
    117153       `Label exit_label ; `Jmp exit_label] in
    118   preamble @
    119   (List.flatten (List.map (translate_fun_def glbls_addr) functs))
     154(*
     155  let fun_set_ra =
     156    translate_code glbls_addr set_ra_label (fun_set_ra set_ra_label) in
     157*)
     158  preamble @ (* fun_set_ra @ *)
     159  (List.flatten (List.map (translate_fun_def glbls_addr set_ra_label) functs))
    120160
    121161
     
    133173  let prog_lbls = prog_labels p in
    134174  let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in
     175  let set_ra_label = Label.Gen.fresh_prefix prog_lbls "_set_ra" in
    135176  let glbls_addr = globals_addr p.LIN.vars in
    136177  let p =
     
    138179      ASM.pexit_label = exit_label ;
    139180      ASM.pcode =
    140         translate_functs glbls_addr exit_label p.LIN.main p.LIN.functs ;
     181        translate_functs glbls_addr exit_label set_ra_label
     182          p.LIN.main p.LIN.functs ;
    141183      ASM.phas_main = p.LIN.main <> None } in
    142184  ASMInterpret.assembly p
Note: See TracChangeset for help on using the changeset viewer.