Aorai_test.ml 3.51 KB
Newer Older
1
2
(* Small script to test that the code generated by aorai can be parsed again
 * by frama-c.
Virgile Prevosto's avatar
Virgile Prevosto committed
3
*)
4
5
6

open Kernel

7
module P = Plugin.Register
Virgile Prevosto's avatar
Virgile Prevosto committed
8
9
10
11
12
    (struct
      let name = "aorai testing module"
      let shortname = "aorai-test"
      let help = "utility script for aorai regtests"
    end)
13
14

module TestNumber =
15
  P.Zero
16
17
18
19
    (struct
      let option_name = "-aorai-test-number"
      let help = "test number when multiple tests are run over the same file"
      let arg_name = "n"
Virgile Prevosto's avatar
Virgile Prevosto committed
20
    end)
21
22

module InternalWpShare =
23
  P.Filepath(
Virgile Prevosto's avatar
Virgile Prevosto committed
24
25
26
27
28
29
30
  struct
    let option_name = "-aorai-test-wp-share"
    let help = "use custom wp share dir (when in internal plugin mode)"
    let arg_name = "dir"
    let existence = Filepath.Must_exist
    let file_kind = "wp share directory"
  end)
31
32

module ProveAuxSpec =
33
  P.False(
Virgile Prevosto's avatar
Virgile Prevosto committed
34
35
36
37
38
  struct
    let option_name = "-aorai-test-prove-aux-spec"
    let help = "use WP + alt-ergo to prove that generated spec and body \
                of auxiliary automata functions match"
  end)
39
40
41
42

let ok = ref false

let is_suffix suf str =
43
44
  let lsuf = String.length suf in
  let lstr = String.length str in
45
46
  if lstr <= lsuf then false
  else
47
    let estr = String.sub str (lstr - lsuf) lsuf in
48
49
50
51
52
53
54
    estr = suf

let extend () =
  let myrun =
    let run = !Db.Toplevel.run in
    fun f ->
      let my_project = Project.create "Reparsing" in
55
56
57
58
59
60
61
62
63
64
65
      let wp_compute_kf kf =
        let vcs = Wp.VC.generate_kf kf in
        Wp.VC.command vcs;
        Bag.iter
          (fun vc ->
             if not (Wp.VC.is_proved vc) then
               P.warning "Could not prove %a in automaton function %a"
                 Property.pretty (Wp.VC.get_property vc)
                 Kernel_function.pretty kf)
          vcs
      in
66
67
68
69
70
      let check_auto_func kf =
        let name = Kernel_function.get_name kf in
        if Kernel_function.is_definition kf &&
           (is_suffix "_pre_func" name || is_suffix "_post_func" name)
        then
71
          wp_compute_kf kf
72
73
      in
      run f;
74
75
76
77
78
79
      let tmpdir = Filename.get_temp_dir_name () in
      let tmpdir =
        match Filename.chop_suffix_opt ~suffix:"/" tmpdir with
        | None -> tmpdir
        | Some dir -> dir
      in
80
      let tmpfile =
81
82
83
84
        tmpdir ^ "/aorai_" ^
        Filename.(
          chop_extension (basename (List.hd (Kernel.Files.get()):>string))) ^
        "_" ^ (string_of_int (TestNumber.get ())) ^ ".i"
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
      in
      let () =
        Extlib.safe_at_exit
          (fun () ->
             if Debug.get () >= 1 || not !ok then
               result "Keeping temp file %s" tmpfile
             else Extlib.safe_remove tmpfile)
      in
      let chan = open_out tmpfile in
      let fmt = Format.formatter_of_out_channel chan in
      File.pretty_ast ~prj:(Project.from_unique_name "aorai") ~fmt ();
      close_out chan;
      let selection =
        State_selection.of_list [ InternalWpShare.self; ProveAuxSpec.self ]
      in
      Project.copy ~selection my_project;
      Project.set_current my_project;
102
      Kernel.SymbolicPath.add ("TMPDIR:"^Filename.get_temp_dir_name());
103
      Files.append_after [ Filepath.Normalized.of_string tmpfile ];
Virgile Prevosto's avatar
Virgile Prevosto committed
104
      Kernel.LogicalOperators.on ();
105
106
107
      Constfold.off ();
      Ast.compute();
      if ProveAuxSpec.get () then begin
108
109
110
        if InternalWpShare.is_set() then
          Wp.Wp_parameters.Share.set (InternalWpShare.get());
        Wp.Wp_parameters.Verbose.set 0;
111
        Globals.Functions.iter check_auto_func;
112
113
      end else begin
        File.pretty_ast ();
114
115
116
117
118
119
      end;
      ok:=true (* no error, we can erase the file *)
  in
  Db.Toplevel.run := myrun

let () = extend ()