stmtcompiler_test_rela.ml 5.23 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(* test API of StmtCompiler for relational property verification*)

open Wp
open Factory
open Sigs

let run () =
  let setup : Factory.setup = { mheap = Hoare;
                                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
23
         | Some VCS.Tactical -> prvs
24
25
26
27
28
         | Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
      ["alt-ergo"] []
  in

  let spawn goal =
François Bobot's avatar
François Bobot committed
29
30
31
    let result _ prv res =
      Format.printf "[%a] %a@.@\n"
        VCS.pp_prover prv VCS.pp_result res
32
33
    in
    let server = ProverTask.server () in
François Bobot's avatar
François Bobot committed
34
    Prover.spawn goal ~delayed:true ~result provers;
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
    Task.launch server
  in

  let prove kf 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 funct = Kernel_function.get_definition kf in
    let stmt = List.hd (funct.sbody.bstmts) in
    let pred = Cil_types.{
        pred_name = [];
        pred_loc = funct.svar.vdecl;
        pred_content = Cil_types.Ptrue;
      }
    in
François Bobot's avatar
François Bobot committed
57
58
    let annot = Logic_const.new_code_annotation (AAssert ([],Assert,pred)) in
    let po = Wpo.{
59
        po_gid = "";
François Bobot's avatar
François Bobot committed
60
        po_leg = "";
61
62
63
64
65
66
67
68
69
70
71
72
73
74
        po_sid = "";
        po_name = "";
        po_idx = Function(kf, None);
        po_model = model;
        po_pid = WpPropId.mk_assert_id kf stmt annot;
        po_formula = Wpo.GoalAnnot vc_annot;
      }
    in
    let inter_po = ref po in
    Property_status.iter (fun x ->
        match Wpo.goals_of_property x with
        | h :: _ ->
            inter_po := Wpo.{
                po_gid = "";
François Bobot's avatar
François Bobot committed
75
                po_leg = "";
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
                po_sid = "";
                po_name = "";
                po_idx = Function(kf, None);
                po_model = model;
                po_pid = h.po_pid;
                po_formula = Wpo.GoalAnnot vc_annot;
              }
        | _ -> ()
      );
    spawn !inter_po;
  in

  let reads_formal f sigma =
    let v= C.M.load sigma
        (Ctypes.C_int (Wp.Ctypes.c_int Cil_types.IInt)) (C.M.cvar f)
    in
    let t =
      C.C.cval v
    in t
  in

  let run_test kf =
    let fct = Kernel_function.get_definition kf in
Loïc Correnson's avatar
Loïc Correnson committed
99
100
    WpContext.on_context (model,WpContext.Kf kf)
      begin fun () ->
François Bobot's avatar
François Bobot committed
101
        let block = Interpreted_automata.Compute.get_automaton ~annotations:true kf in
102
103
104
105
106
107
        let formal = List.hd (fct.sformals) in

        (*First call*)
        let seq1 = {Sigs.pre = Cfg.node (); post = Cfg.node ()} in
        let env1 = Compiler.empty_env kf  in
        let env1 = Compiler.(env1 @* [Clabels.here,seq1.pre;Clabels.next,seq1.post]) in
François Bobot's avatar
François Bobot committed
108
109
        let path1 = Compiler.automaton env1 block in
        let cfg1 = path1.Compiler.paths_cfg in
110
        let node1 = Cfg.T.init' seq1.pre (reads_formal formal) in
François Bobot's avatar
François Bobot committed
111
112
113
        let (_,sigma1,sequence1) =
          Compiler.Cfg.compile seq1.pre
            (Cfg.Node.Set.singleton seq1.post) (Cfg.T.reads node1) cfg1 in
114
115
116
117
118
119
120
        let node1 = Cfg.T.relocate sigma1 node1 in
        let term_1 = Cfg.T.get node1 in

        (*Seconde call*)
        let seq2 = {Sigs.pre = Cfg.node (); post = Cfg.node ()} in
        let env2 = Compiler.empty_env kf  in
        let env2 = Compiler.(env2 @* [Clabels.here,seq2.pre;Clabels.next,seq2.post]) in
François Bobot's avatar
François Bobot committed
121
122
        let path2 = Compiler.automaton env2 block in
        let cfg2 = path2.Compiler.paths_cfg in
123
        let node2 = Cfg.T.init' seq2.pre (reads_formal formal) in
François Bobot's avatar
François Bobot committed
124
125
126
127
        let (_,sigma2,sequence2) =
          Compiler.Cfg.compile
            seq2.pre (Cfg.Node.Set.singleton seq2.post)
            (Cfg.T.reads node2) cfg2 in
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
        let node2 = Cfg.T.relocate sigma2 node2 in
        let term_2 = Cfg.T.get node2 in

        let return1 =
          Compiler.result env1
        in
        let return1 = Lang.F.e_var return1 in
        let return2 =
          Compiler.result env2
        in
        let return2 = Lang.F.e_var return2 in
        let pred =
          Lang.F.p_imply (Lang.F.p_lt term_1 term_2) (Lang.F.p_lt return1 return2)
        in
        Format.printf "------The pred %a @." Lang.F.pp_pred pred;
        let sequent =
          (Conditions.concat [sequence1;sequence2]),pred
        in
        Format.printf "#######################################################################@.";
        Format.printf "Sequent: @[%a@]" !Conditions.pretty sequent;
        Format.printf "#######################################################################@.";
        prove kf sequent;
Loïc Correnson's avatar
Loïc Correnson committed
150
      end ()
151
152
153
154
155
156
157
158
159
160
161
  in

  let ordered_kf =
    List.sort (fun kf1 kf2 ->
        String.compare
          (Kernel_function.get_name kf1)
          (Kernel_function.get_name kf2))
      (Globals.Functions.fold (fun kf acc -> kf::acc) []) in

  List.iter (fun kf ->
      if Kernel_function.is_definition kf then
Loïc Correnson's avatar
Loïc Correnson committed
162
        Lang.local run_test kf)
163
164
165
166
    ordered_kf


let () = Db.Main.extend run