stmtcompiler_test.ml 4.66 KB
Newer Older
Loïc Correnson's avatar
Loïc Correnson committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
(* test API of StmtSemantics *)

open Wp
open Factory
open Sigs

let mode = `Tree

let run () =
  let setup : Factory.setup = { mheap = Typed MemTyped.NoCast;
                                mvar = Var;
                                cint = Cint.Natural;
                                cfloat = Cfloat.Real} in
  let driver = Driver.load_driver () in
  let model = Factory.instance setup driver in
  let module C = (val (Factory.compiler setup.mheap setup.mvar)) in
  let module Compiler = StmtSemantics.Make(C) in
  let module Cfg = Compiler.Cfg in

  let provers =
    List.fold_right
      (fun pname prvs -> match VCS.prover_of_name pname with
         | None -> prvs
Loïc Correnson's avatar
Loïc Correnson committed
24
         | Some VCS.Tactical -> prvs
Loïc Correnson's avatar
Loïc Correnson committed
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
         | Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
      ["qed"] []
  in

  let spawn goal =
    let result _ prv res =
      Format.printf "[%a] %a@.@\n"
        VCS.pp_prover prv VCS.pp_result res
    in
    let server = ProverTask.server () in
    Prover.spawn goal ~delayed:true ~result provers;
    Task.launch server
  in

  let prove_sequent kf prop_id sequent =
    Format.printf "@[<3>@[%s sequent:@]@ %a@]@."
      (Kernel_function.get_name kf)
      !Conditions.pretty sequent;
    let goal = Wpo.GOAL.make sequent in
    let vc_annot = Wpo.VC_Annot.{
        axioms = None;
        goal;
        tags = []; warn = [];
        deps = Property.Set.empty;
        path = Cil_datatype.Stmt.Set.empty;
        effect = None;
      } in
    let po = Wpo.{
        po_gid = ""; po_sid = ""; po_name = ""; po_leg = "";
        po_idx = Function(kf, None); po_model = model;
        po_pid = prop_id;
        po_formula = Wpo.GoalAnnot vc_annot;
      } in
    Format.printf "@[%a@]" Wpo.pp_goal po;
    spawn po;
    Format.printf "%s@." Wpo.bar ;
  in

  let goal_read acc g =
    let reads = Cfg.P.reads g.Compiler.goal_pred in
    Cfg.Node.Map.union
      (fun _ -> C.M.Sigma.union)
      reads acc
  in

  let prove_goal kf start cfg goal =
    let pred = goal.Compiler.goal_pred in
    let user_reads = goal_read Cfg.Node.Map.empty goal in
    let posts = Cfg.P.nodes pred in
    let name = Kernel_function.get_name kf in
    let (_, nsigmas,sequence) = Compiler.Cfg.compile ~mode ~name start posts user_reads cfg in
    (* Format.printf "Nodes of %a: " Lang.F.pp_pred (Cfg.P.get pred); *)
    let map n _domain =
      (* Format.printf "%a " Cfg.Node.pp n; *)
79
80
      try Cfg.Node.Map.find n nsigmas with Not_found ->
        (* Format.printf "unknown node %a@." Cfg.Node.pp n; *) assert false in
Loïc Correnson's avatar
Loïc Correnson committed
81
82
83
84
85
86
87
88
89
    let pred = Cfg.P.relocate
        (Cfg.Node.Map.map map (Cfg.P.reads pred)) pred in
    (* Format.printf "@."; *)
    let p = (Cfg.P.get pred) in
    let sequent = sequence, p in
    prove_sequent kf goal.Compiler.goal_prop sequent
  in

  (** Test on real Cil functions *)
Loïc Correnson's avatar
Loïc Correnson committed
90
91
92
93
  let _run_test model kf =
    let context = model , WpContext.Kf kf in
    WpContext.on_context context
      begin fun () ->
Loïc Correnson's avatar
Loïc Correnson committed
94
95
96
97
98
99
100
101
102
103
104
105
        let automaton = Interpreted_automata.Compute.get_automaton ~annotations:true kf in
        (* Format.printf "@[%s body cil:%a@]@." fct Printer.pp_block block; *)
        let seq = {Sigs.pre = Cfg.node (); post = Cfg.node ()} in
        let env = Compiler.empty_env kf  in
        let env = Compiler.(env @* [Clabels.here,seq.pre;
                                    Clabels.next,seq.post]) in
        let paths = Compiler.automaton env automaton in
        let cfg, goals = paths.Compiler.paths_cfg, paths.Compiler.paths_goals in
        Format.printf "old way@.";
        Bag.iter
          (prove_goal kf seq.pre cfg)
          goals;
Loïc Correnson's avatar
Loïc Correnson committed
106
      end ()
Loïc Correnson's avatar
Loïc Correnson committed
107
108
  in

Loïc Correnson's avatar
Loïc Correnson committed
109
110
111
112
  let run_test_ia model kf =
    let context = model , WpContext.Kf kf in
    WpContext.on_context context
      begin fun () ->
Loïc Correnson's avatar
Loïc Correnson committed
113
114
        let paths,start = Compiler.compute_kf kf in
        let cfg, goals = paths.Compiler.paths_cfg, paths.Compiler.paths_goals in
François Bobot's avatar
François Bobot committed
115
116
        let fname = Filename.temp_file "cfg_pre_" (Kernel_function.get_name kf) in
        let cout = open_out fname in
Loïc Correnson's avatar
Loïc Correnson committed
117
118
119
120
121
122
        Compiler.Cfg.output_dot cout ~checks:(Bag.map (fun g -> g.Compiler.goal_pred) goals) cfg;
        close_out cout;
        Format.printf "new way@.";
        Bag.iter
          (prove_goal kf start cfg)
          goals;
Loïc Correnson's avatar
Loïc Correnson committed
123
      end ()
Loïc Correnson's avatar
Loïc Correnson committed
124
125
126
127
128
129
130
  in

  let ordered_kf =
    List.sort (fun kf1 kf2 ->
        Cil_datatype.Location.compare
          (Kernel_function.get_location kf1)
          (Kernel_function.get_location kf2)
131
132
133
          (* String.compare *)
          (*   (Kernel_function.get_name kf1) *)
          (*   (Kernel_function.get_name kf2) *)
Loïc Correnson's avatar
Loïc Correnson committed
134
135
136
137
      )
      (Globals.Functions.fold (fun kf acc -> kf::acc) []) in

  List.iter (fun kf ->
Loïc Correnson's avatar
Loïc Correnson committed
138
139
      if Kernel_function.is_definition kf then
        Lang.local (run_test_ia model) kf
Loïc Correnson's avatar
Loïc Correnson committed
140
141
142
143
    )
    ordered_kf

let () =  Db.Main.extend run