Changeset 1462 for Deliverables/D2.2


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
Files:
35 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/distributed_files

    r1099 r1462  
    174174src/clight/clightLabelling.ml
    175175src/clight/clightLabelling.mli
     176src/clight/clightLustre.ml
     177src/clight/clightLustre.mli
     178src/clight/clightLustreMain.ml
     179src/clight/clightLustreMain.mli
    176180src/clight/clightParser.ml
    177181src/clight/clightParser.mli
  • Deliverables/D2.2/8051/src/ASM/ASM.mli

    r619 r1462  
    123123    { code        : BitVectors.byte list ;
    124124      cost_labels : string BitVectors.WordMap.t ;
     125      labels      : BitVectors.word StringTools.Map.t ;
    125126      exit_addr   : BitVectors.word ;
    126127      has_main    : bool }
  • Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

    r818 r1462  
    10461046      | #instruction as i -> assembly1 i) p.ASM.pcode) in
    10471047 { ASM.code = code ; ASM.cost_labels = costs ;
     1048   ASM.labels = StringTools.Map.empty ;
    10481049   ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
    10491050;;
  • Deliverables/D2.2/8051/src/ERTL/ERTL.mli

    r818 r1462  
    144144  | St_call_id of AST.ident * int * Label.t
    145145
     146  (* Call to a function given its address. Parameters are the registers holding
     147     the address of the function, the number of arguments of the function, and
     148     the label of the next statement. *)
     149  | St_call_ptr of Register.t * Register.t * int * Label.t
     150
    146151(*
    147   (* Call to a function given its address. Parameters are registers holding the
    148      address of the function, the arguments of the function, the destination
    149      registers, and the label of the next statement. *)
    150   | St_call_ptr of registers * register list * registers * Label.t
    151 
    152152  (* Tail call to a function given its name. Parameters are the name of the
    153      function, and the number of arguments of the function. *)
     153    function, and the number of arguments of the function. *)
    154154  | St_tailcall_id of AST.ident * int
    155155
  • Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

    r818 r1462  
    193193  st
    194194
     195let make_addr st r1 r2 = List.map (fun r -> get_reg (Psd r) st) [r1 ; r2]
     196
    195197
    196198module InterpretExternal = Primitive.Interpret (Mem)
     
    216218  change_pc st next_pc
    217219
    218 let interpret_call lbls_offs st f ra =
    219   let ptr = Mem.find_global st.mem f in
     220let interpret_call lbls_offs st ptr ra =
     221  (* let ptr = Mem.find_global st.mem f in *)
    220222  match Mem.find_fun_def st.mem ptr with
    221223    | ERTL.F_int def ->
     
    353355
    354356    | ERTL.St_load (destr, addr1, addr2, lbl) ->
    355       let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
     357      let addr = make_addr st addr1 addr2 in
    356358      let v = Mem.load st.mem chunk addr in
    357359      let st = add_reg (Psd destr) v st in
     
    359361
    360362    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
    361       let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
     363      let addr = make_addr st addr1 addr2 in
    362364      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
    363365      let st = change_mem st mem in
     
    365367
    366368    | ERTL.St_call_id (f, _, lbl) ->
    367       interpret_call lbls_offs st f lbl
     369      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     370
     371    | ERTL.St_call_ptr (f1, f2, _, lbl) ->
     372      interpret_call lbls_offs st (make_addr st f1 f2) lbl
    368373
    369374    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

    r818 r1462  
    116116      lbl
    117117  | ERTL.St_call_id (f, nb_args, lbl) ->
    118     Printf.sprintf "call \"%s\", %d --> %s"
    119       f
     118    Printf.sprintf "call \"%s\", %d --> %s" f nb_args lbl
     119  | ERTL.St_call_ptr (f1, f2, nb_args, lbl) ->
     120    Printf.sprintf "call_ptr [%s ; %s], %d --> %s"
     121      (Register.print f1)
     122      (Register.print f2)
    120123      nb_args
    121124      lbl
    122125(*
    123   | ERTL.St_call_ptr (f, args, dstrs, lbl) ->
    124     Printf.sprintf "call_ptr %s, %s, %s --> %s"
    125       (print_ptr f)
    126       (print_args args)
    127       (print_return dstrs)
    128       lbl
    129126  | ERTL.St_tailcall_id (f, nb_args) ->
    130127    Printf.sprintf "tailcall \"%s\", %d"
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r818 r1462  
    283283        LTL.St_call_id (f, l)
    284284
     285      | ERTL.St_call_ptr (f1, f2, _, l) ->
     286        let l =
     287          read f2 (fun hdw2 ->
     288            LTL.St_skip
     289              (read f1 (fun hdw1 -> LTL.St_call_ptr (hdw1, hdw2, l)))) in
     290        LTL.St_skip l
     291
    285292      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    286293        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
  • Deliverables/D2.2/8051/src/ERTL/liveness.ml

    r818 r1462  
    3838  | St_load (_, _, _, l)
    3939  | St_store (_, _, _, l)
    40   | St_call_id (_, _, l) ->
     40  | St_call_id (_, _, l)
     41  | St_call_ptr (_, _, _, l) ->
    4142    Label.Set.singleton l
    4243  | St_cond (_, l1, l2) ->
     
    145146  | St_hdw_to_hdw (r, _, _) ->
    146147    L.hsingleton r
    147   | St_call_id _ ->
     148  | St_call_id _ | St_call_ptr _  ->
    148149      (* Potentially destroys all caller-save hardware registers. *)
    149150    Register.Set.empty, I8051.caller_saved
     
    179180    (* Reads the hardware registers that are used to pass parameters. *)
    180181    Register.Set.empty,
     182    set_of_list (MiscPottier.prefix nparams I8051.parameters)
     183  | St_call_ptr (r1, r2, nparams, _) ->
     184    (* Reads the hardware registers that are used to pass parameters. *)
     185    Register.Set.of_list [r1 ; r2],
    181186    set_of_list (MiscPottier.prefix nparams I8051.parameters)
    182187  | St_get_hdw (_, r, _)
     
    230235  | St_store _
    231236  | St_call_id _
     237  | St_call_ptr _
    232238  | St_cond _
    233239  | St_return _ ->
  • Deliverables/D2.2/8051/src/ERTL/uses.ml

    r818 r1462  
    3939    count r uses
    4040  | St_move (r1, r2, _)
    41   | St_op1 (_, r1, r2, _) ->
     41  | St_op1 (_, r1, r2, _)
     42  | St_call_ptr (r1, r2, _, _) ->
    4243    count r1 (count r2 uses)
    4344  | St_opaccsA (_, r1, r2, r3, _)
  • 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
  • Deliverables/D2.2/8051/src/LTL/LTL.mli

    r818 r1462  
    7575  | St_call_id of AST.ident * Label.t
    7676
     77  (* Call to a function given its address. Parameters are the registers holding
     78     the address of the function, and the label of the next statement. *)
     79  | St_call_ptr of I8051.register * I8051.register * Label.t
     80
    7781  (* Branch on A accumulator. Parameters are the label to go to when the A
    7882     accumulator is not 0, and the label to go to when the A accumulator is
  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r818 r1462  
    196196  change_pc st next_pc
    197197
    198 let interpret_call lbls_offs st f ra =
    199   let ptr = Mem.find_global st.mem f in
     198let interpret_call lbls_offs st ptr ra =
    200199  match Mem.find_fun_def st.mem ptr with
    201200    | LTL.F_int def ->
     
    303302
    304303    | LTL.St_call_id (f, lbl) ->
    305       interpret_call lbls_offs st f lbl
     304      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     305
     306    | LTL.St_call_ptr (f1, f2, lbl) ->
     307      let addr = List.map (fun r -> get_reg r st) [f1 ; f2] in
     308      interpret_call lbls_offs st addr lbl
    306309
    307310    | LTL.St_condacc (lbl_true, lbl_false) ->
  • Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

    r818 r1462  
    5555    Printf.sprintf "movex @DPTR, %s --> %s" print_a lbl
    5656  | LTL.St_call_id (f, lbl) -> Printf.sprintf "call \"%s\" --> %s" f lbl
     57  | LTL.St_call_ptr (f1, f2, lbl) ->
     58    Printf.sprintf "call_ptr [%s ; %s] --> %s" (print_reg f1) (print_reg f2) lbl
    5759  | LTL.St_condacc (lbl_true, lbl_false) ->
    5860    Printf.sprintf "branch %s <> 0 --> %s, %s" print_a lbl_true lbl_false
  • Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml

    r818 r1462  
    5050  | LTL.St_call_id (f, _) ->
    5151    LIN.St_call_id f
     52  | LTL.St_call_ptr (f1, f2, _) ->
     53    LIN.St_call_ptr (f1, f2)
    5254
    5355  (* Conditional branch statement. In [LIN], control implicitly
  • Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml

    r818 r1462  
    130130        | LTL.St_load l
    131131        | LTL.St_store l
    132         | LTL.St_call_id (_, l) ->
     132        | LTL.St_call_id (_, l)
     133        | LTL.St_call_ptr (_, _, l) ->
    133134
    134135          visit l
  • Deliverables/D2.2/8051/src/LTL/branch.ml

    r818 r1462  
    8080    | LTL.St_call_id (f, l) ->
    8181      LTL.St_call_id (f, rep l)
     82    | LTL.St_call_ptr (f1, f2, l) ->
     83      LTL.St_call_ptr (f1, f2, rep l)
    8284    | LTL.St_condacc (lbl_true, lbl_false) ->
    8385      LTL.St_condacc (rep lbl_true, rep lbl_false)
  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r818 r1462  
    4848    ERTL.St_store (addr1, addr2, srcrs, lbl)
    4949  | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
     50  | ERTL.St_call_ptr (f1, f2, nb_args, _) ->
     51    ERTL.St_call_ptr (f1, f2, nb_args, lbl)
    5052  | ERTL.St_cond _ as inst -> inst
    5153  | ERTL.St_return _ as inst -> inst
     
    293295   below. When the called function returns, we put the result where the calling
    294296   function expect it to be. *)
    295 let translate_call_id f args ret_regs start_lbl dest_lbl def =
     297let translate_call stmt args ret_regs start_lbl dest_lbl def =
    296298  let nb_args = List.length args in
    297299  add_translates
     
    299301      adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @
    300302     set_params args @
    301      [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ;
     303     [adds_graph [stmt nb_args] ;
    302304      adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ;
    303305      fetch_result ret_regs ;
     
    358360
    359361  | RTL.St_call_id (f, args, ret_regs, lbl') ->
    360     translate_call_id f args ret_regs lbl lbl' def
    361 
    362   | RTL.St_call_ptr _ ->
    363     assert false (* TODO *)
     362    let stmt nb_args = ERTL.St_call_id (f, nb_args, lbl) in
     363    translate_call stmt args ret_regs lbl lbl' def
     364
     365  | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl') ->
     366    let stmt nb_args = ERTL.St_call_ptr (f1, f2, nb_args, lbl) in
     367    translate_call stmt args ret_regs lbl lbl' def
    364368
    365369  (*
     
    438442    | ERTL.St_load (_, _, _, lbl)
    439443    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
     444    | ERTL.St_call_ptr (_, _, _, lbl)
    440445    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
    441446      ->
  • Deliverables/D2.2/8051/src/acc.ml

    r818 r1462  
    2323*)
    2424let process filename =
    25   let _ = Printf.eprintf "Processing %s.\n%!" filename in
    26   let src_language    = Options.get_source_language () in
    27   let tgt_language    = Options.get_target_language () in
    28   let input_ast       = Languages.parse src_language filename in
    29   let input_ast       = Languages.add_runtime input_ast in
    30   let input_ast       = Languages.labelize input_ast in
     25  let _ = Printf.printf "Processing %s.\n%!" filename in
     26  let src_language = Options.get_source_language () in
     27  let tgt_language = Options.get_target_language () in
     28  let is_lustre_file = Options.is_lustre_file () in
     29  let remove_lustre_externals = Options.is_remove_lustre_externals () in
     30  let input_ast =
     31    Languages.parse ~is_lustre_file ~remove_lustre_externals
     32      src_language filename in
     33  let input_ast = Languages.add_runtime input_ast in
     34  let input_ast = Languages.labelize input_ast in
    3135  let (exact_output, output_filename) = match Options.get_output_files () with
    3236    | None -> (false, filename)
    3337    | Some filename' -> (true, filename') in
    3438  let save ?(suffix="") ast =
    35     Languages.save exact_output output_filename suffix ast
     39    Languages.save
     40      (Options.is_asm_pretty ()) exact_output output_filename suffix ast
    3641  in
    3742  let target_asts =
     
    4550  if Options.annotation_requested () then
    4651    begin
    47       let (annotated_input_ast, cost_id, cost_incr) =
     52      let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
    4853        Languages.annotate input_ast final_ast in (
    4954          save ~suffix:"-annotated" annotated_input_ast;
    50           Languages.save_cost output_filename cost_id cost_incr);
     55          Languages.save_cost exact_output output_filename cost_id cost_incr
     56            extern_cost_variables);
    5157    end;
    5258                                             
     
    5460    List.iter save intermediate_asts;
    5561
    56   if Options.interpretation_requested () || Options.is_debug_enabled () then
     62  if Options.interpretations_requested () then
    5763    begin
    5864      let asts = target_asts in
     
    6268      Checker.same_traces (List.combine asts label_traces);
    6369      Printf.eprintf "OK.\n%!";
    64     end
     70    end;
     71
     72  if Options.interpretation_requested () then
     73    ignore (Languages.interpret (Options.is_debug_enabled ()) final_ast)
     74
     75let lustre_test filename =
     76  let lustre_test       = match Options.get_lustre_test () with
     77    | None -> assert false (* do not use on this argument *)
     78    | Some lustre_test -> lustre_test in
     79  let lustre_test_cases = Options.get_lustre_test_cases () in
     80  let lustre_test_cycles = Options.get_lustre_test_cycles () in
     81  let lustre_test_min_int = Options.get_lustre_test_min_int () in
     82  let lustre_test_max_int = Options.get_lustre_test_max_int () in
     83  let src_language      = Languages.Clight in
     84  let tgt_language      = Languages.Clight in
     85  let input_ast         = Languages.parse src_language filename in
     86  let input_ast         =
     87    Languages.add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
     88      lustre_test_min_int lustre_test_max_int input_ast in
     89  let (exact_output, output_filename) = match Options.get_output_files () with
     90    | None -> (false, filename)
     91    | Some filename' -> (true, filename') in
     92  let save ast =
     93    Languages.save
     94      (Options.is_asm_pretty ()) exact_output output_filename "" ast in
     95  let target_asts = Languages.compile false src_language tgt_language input_ast
     96  in
     97  let final_ast, _ = Misc.ListExt.cut_last target_asts in
     98  save input_ast ;
     99  save final_ast
    65100
    66101let _ =
    67102  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
    68   else List.iter process input_files
     103  else
     104    if Options.get_lustre_test () <> None then List.iter lustre_test input_files
     105    else List.iter process input_files
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

    r818 r1462  
    130130  let Clight.Expr (e, t) = e in
    131131  match e with
    132     | Clight.Ecost (lbl, e) when CostLabel.Map.find lbl cost_mapping = 0 ->
     132    | Clight.Ecost (lbl, e)
     133        when CostLabel.Map.mem lbl cost_mapping &&
     134             CostLabel.Map.find lbl cost_mapping = 0 ->
    133135        e
    134136    | _ ->
     
    300302  (cost_incr, Clight.Internal cfun)
    301303
     304(* Create a fresh uninitialized cost variable for each external function. This
     305   will be used by the Cost plug-in of the Frama-C platform. *)
     306
     307let extern_cost_variables make_unique functs =
     308  let prefix = "_cost_of_" in
     309  let f (decls, map) (_, def) = match def with
     310    | Clight.Internal _ -> (decls, map)
     311    | Clight.External (id, _, _) ->
     312      let new_var = make_unique (prefix ^ id) in
     313      (decls @ [cost_decl new_var], StringTools.Map.add id new_var map) in
     314  List.fold_left f ([], StringTools.Map.empty) functs
     315
    302316let save_tmp tmp_file s =
    303317  let cout = open_out tmp_file in
     
    316330  (* Create a fresh 'cost' variable. *)
    317331  let names = names p in
    318   let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
     332  let make_unique = StringTools.make_unique names in
     333  let cost_id = make_unique cost_id_prefix in
    319334  let cost_decl = cost_decl cost_id in
     335
     336  (* Create a fresh uninitialized global variable for each extern function. *)
     337  let (extern_cost_decls, extern_cost_variables) =
     338    extern_cost_variables make_unique p.Clight.prog_funct in
    320339
    321340  (* Define an increment function for the cost variable. *)
     
    330349
    331350  (* Glue all this together. *)
    332   let prog_vars = cost_decl :: p.Clight.prog_vars in
     351  let prog_vars = cost_decl :: extern_cost_decls @ p.Clight.prog_vars in
    333352  let prog_funct = cost_incr_def :: prog_funct in
    334353  let p' =
     
    343362  let res = ClightParser.process tmp_file in
    344363  Misc.SysExt.safe_remove tmp_file ;
    345   (res, cost_id, cost_incr)
     364  (res, cost_id, cost_incr, extern_cost_variables)
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r818 r1462  
    66    Then, each cost label in the program is replaced by an increment of the cost
    77    variable, following the mapping [cost_map]. The function also returns the
    8     name of the cost variable and the name of the cost increment function. *)
     8    name of the cost variable, the name of the cost increment function, and a
     9    fresh uninitialized global (cost) variable associated to each extern
     10    function. *)
    911
    1012val instrument : Clight.program -> int CostLabel.Map.t ->
    11                  Clight.program * string * string
     13                 Clight.program * string * string * string StringTools.Map.t
    1214
    1315val cost_labels : Clight.program -> CostLabel.Set.t
  • Deliverables/D2.2/8051/src/clight/clightParser.ml

    r818 r1462  
    1 let process file =
    2   let tmp_file1 = Filename.temp_file "cparser1" ".c"
    3   and tmp_file2 = Filename.temp_file "cparser2" ".i"
     1
     2let process ?is_lustre_file ?remove_lustre_externals file =
     3  let temp_dir = Filename.dirname file in
     4  let tmp_file1 = Filename.temp_file ~temp_dir "cparser1" ".c"
     5  and tmp_file2 = Filename.temp_file ~temp_dir "cparser2" ".i"
    46  and prepro_opts = [] in
    57
     
    810    try
    911      let oc = open_out tmp_file1 in
     12      if is_lustre_file = Some true || remove_lustre_externals = Some true then
     13        output_string oc "#include<string.h>";
    1014      output_string oc Primitive.prototypes ;
    1115      close_out oc
     
    1519       (Filename.quote file) (Filename.quote tmp_file1)) in
    1620  if rc <> 0 then (
     21    (*
    1722    Misc.SysExt.safe_remove tmp_file1;
     23    *)
    1824    failwith "Error adding primitive prototypes."
    1925  );
     
    2632       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
    2733  if rc <> 0 then (
     34    (*
    2835    Misc.SysExt.safe_remove tmp_file1;
    2936    Misc.SysExt.safe_remove tmp_file2;
     37    *)
    3038    failwith "Error calling gcc."
    3139  );
     
    3341  (* C to Cil *)
    3442  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
    35   Misc.SysExt.safe_remove tmp_file1;
    36   Misc.SysExt.safe_remove tmp_file2;
    3743  match r with
    3844    | None -> failwith "Error during C parsing."
     
    4147      (match ClightFromC.convertProgram p with
    4248        | None -> failwith "Error during C to Clight pass."
    43         | Some(pp) -> pp
    44       )
     49        | Some(pp) ->
     50          Misc.SysExt.safe_remove tmp_file1;
     51          Misc.SysExt.safe_remove tmp_file2;
     52          if remove_lustre_externals = Some true then ClightLustre.simplify pp
     53          else pp)
  • Deliverables/D2.2/8051/src/clight/clightParser.mli

    r486 r1462  
     1
    12(** This module implements a parser for [C] based on [gcc] and
    23    [CIL]. *)
    34
    4 (** [process filename] parses the contents of [filename] to obtain
    5     an abstract syntax tree that represents a Clight program. *)
    6 val process : string -> Clight.program
     5(** [process ?is_lustre_file ?remove_lustre_externals filename] parses the
     6    contents of [filename] to obtain an abstract syntax tree that represents a
     7    Clight program. *)
     8val process :
     9  ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
     10  string -> Clight.program
  • Deliverables/D2.2/8051/src/clight/clightSwitch.ml

    r818 r1462  
    66let type_of (Clight.Expr (_, t)) = t
    77
    8 let rec simplify_switch e cases stmts = match cases, stmts with
    9   | Clight.LSdefault _, stmt :: _ -> stmt
    10   | Clight.LScase (i, _, lbl_stmts), stmt :: stmts ->
    11     let next_cases = simplify_switch e lbl_stmts stmts in
    12     let ret_type = Clight.Tint (Clight.I32, AST.Signed) in
    13     let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in
    14     let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in
    15     Clight.Sifthenelse (test, stmt, next_cases)
    16   | _ -> assert false (* do not use on these arguments *)
    178
    189let f_expr e _ = e
    1910
    20 let f_stmt stmt sub_exprs_res sub_stmts_res = match stmt, sub_stmts_res with
    21   | Clight.Sswitch (e, cases), sub_stmts -> simplify_switch e cases sub_stmts
    22   | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     11let f_stmt lbl stmt sub_exprs_res sub_stmts_res =
     12  match stmt, sub_stmts_res with
     13    | Clight.Sbreak, _ -> Clight.Sgoto lbl
     14    | Clight.Swhile _, _ | Clight.Sdowhile _, _
     15    | Clight.Sfor _, _ | Clight.Sswitch _, _ -> stmt
     16    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
    2317
    24 let simplify_statement = ClightFold.statement2 f_expr f_stmt
     18let replace_undeep_break lbl = ClightFold.statement2 f_expr (f_stmt lbl)
    2519
    26 let simplify_fundef = function
     20
     21let add_starting_lbl fresh stmt =
     22  let lbl = fresh () in
     23  (lbl, Clight.Slabel (lbl, stmt))
     24
     25let add_starting_lbl_list fresh stmts = List.map (add_starting_lbl fresh) stmts
     26
     27let add_ending_goto lbl stmt =
     28  Clight.Ssequence (stmt, Clight.Slabel (lbl, Clight.Sskip))
     29
     30let make_sequence stmts =
     31  let f sequence stmt = Clight.Ssequence (sequence, stmt) in
     32  List.fold_left f Clight.Sskip stmts
     33
     34let simplify_switch fresh e cases stmts =
     35  let exit_lbl = fresh () in
     36  let (lbls, stmts) = List.split (add_starting_lbl_list fresh stmts) in
     37  let stmts = List.map (replace_undeep_break exit_lbl) stmts in
     38  let rec aux cases lbls = match cases, lbls with
     39    | Clight.LSdefault _, lbl :: _ -> [Clight.Sgoto lbl]
     40    | Clight.LScase (i, _, cases), lbl :: lbls ->
     41      let next_cases = aux cases lbls in
     42      let ret_type = Clight.Tint (Clight.I32, AST.Signed) in
     43      let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in
     44      let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in
     45      Clight.Sifthenelse (test, Clight.Sgoto lbl, Clight.Sskip) :: next_cases
     46    | _ ->
     47      (* Do not use on these arguments: wrong list size. *)
     48      assert false in
     49  add_ending_goto exit_lbl (make_sequence ((aux cases lbls) @ stmts))
     50
     51let f_expr e _ = e
     52
     53let f_stmt fresh stmt sub_exprs_res sub_stmts_res =
     54  match stmt, sub_stmts_res with
     55    | Clight.Sswitch (e, cases), sub_stmts ->
     56      simplify_switch fresh e cases sub_stmts
     57    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     58
     59let simplify_statement fresh = ClightFold.statement2 f_expr (f_stmt fresh)
     60
     61let simplify_fundef fresh = function
    2762  | Clight.Internal cfun ->
    28     let cfun =
    29       { cfun with Clight.fn_body = simplify_statement cfun.Clight.fn_body } in
    30     Clight.Internal cfun
     63    let fn_body = simplify_statement fresh cfun.Clight.fn_body in
     64    Clight.Internal { cfun with Clight.fn_body = fn_body }
    3165  | fundef -> fundef
    3266
    3367let simplify p =
    34   let f (id, fundef) = (id, simplify_fundef fundef) in
     68  let labels = ClightAnnotator.all_labels p in
     69  let fresh = StringTools.make_fresh labels "_tmp_switch" in
     70  let f (id, fundef) = (id, simplify_fundef fresh fundef) in
    3571  { p with Clight.prog_funct = List.map f p.Clight.prog_funct }
  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r818 r1462  
    217217let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset))
    218218
    219 let sort_globals stack_vars globals var_locs =
     219let sort_globals stack_vars globals functs var_locs =
    220220  let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in
     221  let f_functs (id, fundef) =
     222    let (params, return) =  match fundef with
     223      | Clight.Internal cfun ->
     224        (List.map snd cfun.Clight.fn_params, cfun.Clight.fn_return)
     225      | Clight.External (_, params, return) -> (params, return) in
     226    (id, Clight.Tfunction (params, return)) in
     227  let functs = List.map f_functs functs in
     228  let globals = globals @ functs in
    221229  sort_vars Global None stack_vars globals var_locs
    222230
     
    225233   globals. *)
    226234
    227 let sort_variables globals cfun =
     235let sort_variables globals functs cfun =
    228236  let stack_vars = stack_vars cfun in
    229237  let var_locs = empty_var_locs in
    230   let var_locs = sort_globals stack_vars globals var_locs in
     238  let var_locs = sort_globals stack_vars globals functs var_locs in
    231239  let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in
    232240  let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in
     
    439447
    440448and translate_addrof_ident res_type var_locs id =
     449  assert (mem_var_locs id var_locs) ;
    441450  match find_var_locs id var_locs with
    442     | (Local, _) | (Param, _) -> assert false (* type error *)
     451    | (Local, _) | (Param, _) -> assert false (* location error *)
    443452    | (LocalStack off, _) | (ParamStack off, _) ->
    444453      Cminor.Expr (add_stack off, res_type)
     
    585594  fold_var_locs f var_locs body
    586595
    587 let translate_internal fresh globals cfun =
    588   let var_locs = sort_variables globals cfun in
     596let translate_internal fresh globals functs cfun =
     597  let var_locs = sort_variables globals functs cfun in
    589598  let params =
    590599    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
     
    602611                   AST.res = type_return_of_ctype return } }
    603612
    604 let translate_funct fresh globals (id, def) =
     613let translate_funct fresh globals functs (id, def) =
    605614  let def = match def with
    606     | Clight.Internal ff -> Cminor.F_int (translate_internal fresh globals ff)
     615    | Clight.Internal ff ->
     616      Cminor.F_int (translate_internal fresh globals functs ff)
    607617    | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in
    608618  (id, def)
     
    610620let translate p =
    611621  let fresh = ClightAnnotator.make_fresh "_tmp" p in
     622  let translate_funct =
     623    translate_funct fresh p.Clight.prog_vars p.Clight.prog_funct in
    612624  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
    613     Cminor.functs =
    614       List.map (translate_funct fresh p.Clight.prog_vars) p.Clight.prog_funct ;
     625    Cminor.functs = List.map translate_funct p.Clight.prog_funct ;
    615626    Cminor.main = p.Clight.prog_main }
  • Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

    r1421 r1462  
    243243         | Some(v) -> Some(v)
    244244      )
    245   | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
    246   | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
    247   | St_exit(_)                  -> None
    248   | St_switch(_,_,_)            -> None
    249   | St_return(_)                -> None
    250   | St_label(l,s) when l = lbl  -> Some((s,k))
    251   | St_goto(_)                  -> None
    252   | St_cost(_,s) | St_label(_,s)-> fdlbl k s
     245  | St_loop(s)                     -> fdlbl (Ct_cont(St_loop(s),k)) s
     246  | St_block(s)                    -> fdlbl (Ct_endblock(k)) s
     247  | St_exit(_)                     -> None
     248  | St_switch(_,_,_)               -> None
     249  | St_return(_)                   -> None
     250  | St_label(l,s) when l = lbl     -> Some((s,k))
     251  | St_goto(_)                     -> None
     252  | St_cost (_,s) | St_label (_,s) -> fdlbl k s
    253253  in match fdlbl k st with
    254254      None -> assert false (*Wrong label*)
  • Deliverables/D2.2/8051/src/dev_test.ml

    r818 r1462  
    2323    in
    2424    let actions =
    25       [(print, Languages.save false filename "") ;
     25      [(print, Languages.save false false filename "") ;
    2626       (interpret, (fun p -> ignore (Languages.interpret debug p)))] in
    2727    List.iter (fun (b, f') -> if b then List.iter (f f') ps else ()) actions
  • Deliverables/D2.2/8051/src/languages.ml

    r818 r1462  
    5151  | language -> [to_string language]
    5252
    53 let parse = function
     53let parse ?is_lustre_file ?remove_lustre_externals = function
    5454  | Clight ->
    55     fun filename -> AstClight (ClightParser.process filename)
     55    fun filename ->
     56      AstClight
     57        (ClightParser.process ?is_lustre_file ?remove_lustre_externals filename)
    5658
    5759(*
     
    111113
    112114let ltl_to_lin = function
    113   | AstLTL p -> 
     115  | AstLTL p ->
    114116    AstLIN (LTLToLIN.translate p)
    115117  | _ -> assert false
    116118
    117119let lin_to_asm = function
    118   | AstLIN p -> 
     120  | AstLIN p ->
    119121    AstASM (LINToASM.translate p)
    120122  | _ -> assert false
     
    210212let instrument costs_mapping = function
    211213  | AstClight p ->
    212     let (p', cost_id, cost_incr) = ClightAnnotator.instrument p costs_mapping in
    213     (AstClight p', cost_id, cost_incr)
     214    let (p', cost_id, cost_incr, extern_cost_variables) =
     215      ClightAnnotator.instrument p costs_mapping in
     216    (AstClight p', cost_id, cost_incr, extern_cost_variables)
    214217(*
    215218  | AstCminor p ->
     
    222225         "Instrumentation is not implemented for source language `%s'."
    223226         (to_string (language_of_ast p)));
    224     (p, "", "")
    225 
    226 let annotate input_ast final = 
     227    (p, "", "", StringTools.Map.empty)
     228
     229let annotate input_ast final =
    227230  let costs_mapping = compute_costs final in
    228231  instrument costs_mapping input_ast
    229232
    230 let string_output = function
     233let string_output asm_pretty = function
    231234  | AstClight p ->
    232235    [ClightPrinter.print_program p]
     
    244247    [LINPrinter.print_program p]
    245248  | AstASM p ->
    246     [Pretty.print_program p ; ASMPrinter.print_program p]
    247 
    248 let save exact_output filename suffix ast =
     249    (if asm_pretty then [Pretty.print_program p]
     250     else ["Pretty print not requested"]) @
     251    [ASMPrinter.print_program p]
     252
     253let save asm_pretty exact_output filename suffix ast =
    249254  let ext_chopped_filename =
    250255    if exact_output then filename
     
    259264    if exact_output then ext_filenames
    260265    else List.map Misc.SysExt.alternative ext_filenames in
    261   let output_strings = string_output ast in
     266  let output_strings = string_output asm_pretty ast in
    262267  let f filename s =
    263268    let cout = open_out filename in
     
    267272  List.iter2 f output_filenames output_strings
    268273
    269 let save_cost filename cost_id cost_incr =
     274let save_cost exact_name filename cost_id cost_incr extern_cost_variables =
     275  let filename =
     276    if exact_name then filename
     277    else
     278      try Filename.chop_extension filename
     279      with Invalid_argument ("Filename.chop_extension") -> filename in
    270280  let cout = open_out (filename ^ ".cerco") in
     281  let f fun_name cost_var =
     282    output_string cout (fun_name ^ " " ^ cost_var ^ "\n") in
    271283  output_string cout (cost_id ^ "\n");
    272284  output_string cout (cost_incr ^ "\n");
     285  StringTools.Map.iter f extern_cost_variables;
    273286  flush cout;
    274287  close_out cout
     
    291304  | AstASM p ->
    292305    ASMInterpret.interpret debug p
     306
     307let add_lustre_main
     308    lustre_test lustre_test_cases lustre_test_cycles
     309    lustre_test_min_int lustre_test_max_int = function
     310  | AstClight p ->
     311    AstClight
     312      (ClightLustreMain.add lustre_test lustre_test_cases lustre_test_cycles
     313         lustre_test_min_int lustre_test_max_int p)
     314  | _ ->
     315    Error.global_error "during main generation"
     316      "Lustre testing is only available with C programs."
  • Deliverables/D2.2/8051/src/languages.mli

    r818 r1462  
    3434val language_of_ast : ast -> name
    3535
    36 (** [parse name] returns the parsing function of the language
    37     [name]. *)
    38 val parse : name -> (string -> ast)
     36(** [parse ?is_lustre_file ?remove_lustre_externals name] returns the parsing
     37    function of the language [name]. *)
     38val parse : ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
     39  name -> (string -> ast)
    3940
    4041(** {2 Compilation} *)
     
    6667
    6768(** [annotate input_ast target_ast] inserts cost annotations into the input AST
    68     from the (final) target AST. It also returns the name of the cost variable
    69     and the name of the cost increment function. *)
    70 val annotate : ast -> ast -> (ast * string * string)
     69    from the (final) target AST. It also returns the name of the cost variable,
     70    the name of the cost increment function, and a the name of a fresh
     71    uninitialized global variable for each external function. *)
     72val annotate : ast -> ast -> (ast * string * string * string StringTools.Map.t)
    7173
    7274(** [interpret debug ast] runs the program [ast] from the default initial
     
    7678(** {2 Serialization} *)
    7779
    78 (** [save exact_output filename input_ast] pretty prints [input_ast] in a file
    79     whose name is prefixed by [filename] and whose extension is deduced from the
    80     language of the AST. If [exact_output] is false then the written file will
    81     be fresh. *)
    82 val save : bool -> string -> string -> ast -> unit
     80(** [save asm_pretty exact_output filename input_ast] prints [input_ast] in a
     81    file whose name is prefixed by [filename] and whose extension is deduced
     82    from the language of the AST. If [exact_output] is false then the written
     83    file will be fresh. If [asm_pretty] is true, then an additional
     84    pretty-printed assembly file is output. *)
     85val save : bool -> bool -> string -> string -> ast -> unit
    8386
    84 (** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
    85     cost variable and then the name [cost_incr] of the cost increment function
    86     in a seperate line in the file prefixed by [filename] and extended with
     87(** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
     88    prints the name [cost_id] of the cost variable, then the name [cost_incr] of
     89    the cost increment function, and the entries of the mapping
     90    [extern_cost_variables] (key first, then binding, seperated by a space) in a
     91    seperate line in the file prefixed by [filename] and extended with
    8792    ".cost". If the file already exists, it is overwritten. *)
    88 val save_cost : string -> string -> string -> unit
     93val save_cost : bool -> string -> string -> string ->
     94  string StringTools.Map.t -> unit
    8995
    9096(** [from_string s] parses [s] as an intermediate language name. *)
     
    9399(** [to_string n] prints [n] as a string. *)
    94100val to_string   : name -> string
     101
     102(** [add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
     103    lustre_test_min_int lustre_test_max_int ast] adds a main function that tests
     104    a Lustre step function to a Clight AST. The file [lustre_test] contains
     105    CerCo information (e.g. the name of the cost variable). The integer
     106    [lustre_test_cases] is the number of test cases that are performed, and the
     107    integer [lustre_test_cycles] is the number of cycles per test
     108    case. [lustre_test_min_int] (resp. [lustre_test_max_int]) is the minimum
     109    (resp. maximum) integer value randomly generated during testing, and. *)
     110val add_lustre_main : string -> int -> int -> int -> int -> ast -> ast
  • Deliverables/D2.2/8051/src/options.ml

    r740 r1462  
    4040let interpretation_requested () = !interpretation_flag
    4141
     42let interpretations_flag         = ref false
     43let request_interpretations      = (:=) interpretations_flag
     44let interpretations_requested () = !interpretations_flag
     45
    4246let debug_flag                  = ref false
    4347let set_debug                   = (:=) debug_flag
    4448let is_debug_enabled ()         = !debug_flag
     49
     50let asm_pretty_flag             = ref false
     51let set_asm_pretty              = (:=) asm_pretty_flag
     52let is_asm_pretty ()            = !asm_pretty_flag
     53
     54let lustre_flag                 = ref false
     55let set_lustre_file             = (:=) lustre_flag
     56let is_lustre_file ()           = !lustre_flag
     57
     58let remove_lustre_externals       = ref false
     59let set_remove_lustre_externals   = (:=) remove_lustre_externals
     60let is_remove_lustre_externals () = !remove_lustre_externals
     61
     62let lustre_test                 = ref None
     63let set_lustre_test s           = lustre_test := Some s
     64let get_lustre_test ()          = !lustre_test
     65
     66let lustre_test_cases           = ref 100
     67let set_lustre_test_cases       = (:=) lustre_test_cases
     68let get_lustre_test_cases ()    = !lustre_test_cases
     69
     70let lustre_test_cycles          = ref 100
     71let set_lustre_test_cycles      = (:=) lustre_test_cycles
     72let get_lustre_test_cycles ()   = !lustre_test_cycles
     73
     74let lustre_test_min_int         = ref (-1000)
     75let set_lustre_test_min_int     = (:=) lustre_test_min_int
     76let get_lustre_test_min_int ()  = !lustre_test_min_int
     77
     78let lustre_test_max_int         = ref 1000
     79let set_lustre_test_max_int     = (:=) lustre_test_max_int
     80let get_lustre_test_max_int ()  = !lustre_test_max_int
    4581
    4682(*
     
    5591
    5692let options = OptionsParsing.register [
     93(*
    5794  "-s", Arg.String set_source_language,
    5895  " Choose the source language between:";
    5996  extra_doc " Clight, Cminor";
    6097  extra_doc " [default is C]";
     98*)
    6199
    62100  "-l", Arg.String set_target_language,
     
    71109  " Interpret the compiled code.";
    72110
     111  "-is", Arg.Set interpretations_flag,
     112  " Interpret all the compilation passes.";
     113
    73114  "-d", Arg.Set debug_flag,
    74115  " Debugging mode.";
     
    76117  "-o", Arg.String set_output_files,
    77118  " Prefix of the output files.";
     119
     120  "-asm-pretty", Arg.Set asm_pretty_flag,
     121  " Output a pretty-printed assembly file.";
     122
     123  "-lustre", Arg.Set lustre_flag,
     124  " Input file is a Lustre file.";
     125
     126  "-remove-lustre-externals", Arg.Set remove_lustre_externals,
     127  " Remove Lustre externals.";
     128
     129  "-lustre-test", Arg.String set_lustre_test,
     130  " Input file is a Lustre file, testing requested.";
     131
     132  "-lustre-test-cases", Arg.Int set_lustre_test_cases,
     133  " Set the number of test cases when testing a Lustre";
     134  extra_doc " file.";
     135  extra_doc " [default is 100]";
     136
     137  "-lustre-test-cycles", Arg.Int set_lustre_test_cycles,
     138  " Set the number of cycles for each case when testing";
     139  extra_doc " a Lustre file.";
     140  extra_doc " [default is 100]";
     141
     142  "-lustre-test-min-int", Arg.Int set_lustre_test_min_int,
     143  " Random int minimum value when testing a Lustre file.";
     144  extra_doc " [default is -1000]";
     145
     146  "-lustre-test-max-int", Arg.Int set_lustre_test_max_int,
     147  " Random int maximum value when testing a Lustre file.";
     148  extra_doc " [default is 1000]";
    78149
    79150(*
  • Deliverables/D2.2/8051/src/options.mli

    r740 r1462  
    99val get_target_language : unit -> Languages.name
    1010
    11 (** {2 Interpretation requests} *)
     11(** {2 Interpretation request} *)
    1212val request_interpretation   : bool -> unit
    1313val interpretation_requested : unit -> bool
     14
     15(** {2 Interpretation requests} *)
     16val request_interpretations   : bool -> unit
     17val interpretations_requested : unit -> bool
    1418
    1519(** {2 Annotation requests} *)
     
    2832val is_debug_enabled : unit -> bool
    2933
     34(** {2 Assembly pretty print} *)
     35val set_asm_pretty : bool -> unit
     36val is_asm_pretty  : unit -> bool
     37
     38(** {2 Lustre file} *)
     39val set_lustre_file : bool -> unit
     40val is_lustre_file  : unit -> bool
     41
     42(** {2 Remove Lustre externals} *)
     43val set_remove_lustre_externals : bool -> unit
     44val is_remove_lustre_externals  : unit -> bool
     45
     46(** {2 Lustre file and test requested} *)
     47val set_lustre_test : string -> unit
     48val get_lustre_test : unit -> string option
     49
     50(** {2 Lustre file: number of test cases} *)
     51val set_lustre_test_cases : int -> unit
     52val get_lustre_test_cases : unit -> int
     53
     54(** {2 Lustre file: number of cycles for each case} *)
     55val set_lustre_test_cycles : int -> unit
     56val get_lustre_test_cycles : unit -> int
     57
     58(** {2 Lustre file: random int minimum value} *)
     59val set_lustre_test_min_int : int -> unit
     60val get_lustre_test_min_int : unit -> int
     61
     62(** {2 Lustre file: random int maximum value} *)
     63val set_lustre_test_max_int : int -> unit
     64val get_lustre_test_max_int : unit -> int
     65
    3066(*
    3167(** {2 Print results requests} *)
  • Deliverables/D2.2/8051/src/utilities/stringSig.mli

    r818 r1462  
    99  val compare : t -> t -> int
    1010
    11   module Set : Set.S with type elt = t
     11  module Set : sig
     12    include Set.S with type elt = t
     13    val of_list : elt list -> t
     14    val unionl : t list -> t
     15  end
    1216
    1317  module Map : Map.S with type key = t
     
    2125
    2226  val make_unique : Set.t -> (string -> string)
     27  val make_fresh  : Set.t -> string -> (unit -> string)
    2328
    2429end
  • Deliverables/D2.2/8051/src/utilities/stringTools.ml

    r818 r1462  
    77
    88
    9 module Set = Set.Make (String)
     9module Set = struct
     10  include Set.Make (String)
     11  let of_list l =
     12    let f res e = add e res in
     13    List.fold_left f empty l
     14  let unionl l = List.fold_left union empty l
     15end
    1016
    1117
     
    5056    res in
    5157  unique
     58
     59let make_fresh set prefix =
     60  let fresh_prefix = Gen.fresh_prefix set prefix in
     61  let universe = Gen.new_universe fresh_prefix in
     62  (fun () -> Gen.fresh universe)
Note: See TracChangeset for help on using the changeset viewer.