Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / tiny / tiny_verifier.ml @ f0195e96

History | View | Annotate | Download (1.75 KB)

1

    
2
let active = ref false
3
let tiny_debug = ref false
4

    
5
    
6
let tiny_run ~basename prog machines =
7
  let node_name =
8
    match !Options.main_node with
9
    | "" -> (
10
      Format.eprintf "Tiny verifier requires a main node.@.";
11
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
12
        (Utils.fprintf_list ~sep:"@ "
13
           (fun fmt m ->
14
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
15
           )
16
        )
17
        machines; 
18
      exit 1
19
    )
20
    | s -> ( (* should have been addessed before *)
21
      match Machine_code_common.get_machine_opt machines s with
22
      | None -> begin
23
          Global.main_node := s;
24
          Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
25
          raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
26
        end
27
      | Some _ -> s
28
    )
29
  in
30
  let m = Machine_code_common.get_machine machines node_name in
31
  let env = (* We add each variables of the node the Tiny env *)
32
    Tiny_utils.machine_to_env m in
33
  let nd = m.mname in
34
  (* Building preamble with some bounds on inputs *)
35
  (* TODO: deal woth contracts, asserts, ... *)
36
  let bounds_inputs = [] in
37
  let ast = Tiny_utils.machine_to_ast bounds_inputs m in
38
  let mems = m.mmemory in
39
  
40
   Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
41

    
42
  ()
43
  
44
  
45
module Verifier =
46
  (struct
47
    include VerifierType.Default
48
    let name = "tiny"
49
    let options =
50
      [
51
        "-debug", Arg.Set tiny_debug, "tiny debug"
52
      ]
53
      
54
    let activate () =
55
      active := true;
56
      (* Options.global_inline := true;
57
       * Options.optimization := 0;
58
       * Options.const_unfold := true; *)
59
      ()
60
      
61
    let is_active () = !active
62
    let run = tiny_run
63
            
64
            
65
  end: VerifierType.S)
66