Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / pathConditions.ml @ 3769b712

History | View | Annotate | Download (12 KB)

1
open Lustrec.Lustre_types 
2
open Lustrec.Corelang
3
open Lustrec.Log
4
open Format
5

    
6
module IdSet = Set.Make (struct type t = expr * int let compare = compare end)
7

    
8
let inout_vars = ref [] 
9

    
10
(* This was used to add inout variables in the final signature. May have to be
11
   reactivated later *)
12
  
13
(* let print_tautology_var fmt v = *)
14
(*   match (Lustrec.Types.repr v.var_type).Lustrec.Types.tdesc with *)
15
(*   | Lustrec.Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *)
16
(*   | Lustrec.Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
17
(*   | Lustrec.Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
18
(*   | _ -> Format.fprintf fmt "(true)" *)
19

    
20
(* let print_path arg = match !inout_vars with *)
21
(*   | [] -> Format.printf "%t@." arg   *)
22
(*   | l -> Format.printf "%t and %a@." arg (Lustrec.Utils.fprintf_list ~sep:" and " (fun fmt elem -> print_tautology_var fmt elem)) l *)
23

    
24
let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ]
25

    
26
(* Used when we were printing the expression directly. Now we are constructing
27
   them as regular expressions.
28

    
29
   let rec print_pre fmt nb_pre = if nb_pre <= 0 then () else ( Format.fprintf
30
   fmt "pre "; print_pre fmt (nb_pre-1) )
31
*)
32
  
33
let rec mk_pre n e =
34
  if n <= 0 then
35
    e
36
  else
37
    mkexpr e.expr_loc (Expr_pre e)
38
   
39
(*
40
   let combine2 f sub1 sub2 = 
41
   let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in
42
   let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in
43
   let common = IdSet.inter elem_e1 elem_e2 in
44
   let sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
45
   let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2 in
46
   (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @
47
   (List.map (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @
48
   (List.map (fun v -> (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common))      )
49
*)
50

    
51
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =
52
match active, modified, orig with
53
| true::active_tl, e::modified_tl, _::orig_tl -> (List.assoc v e)::(select v active_tl modified_tl orig_tl)
54
| false::active_tl, _::modified_tl, e::orig_tl -> e::(select v active_tl modified_tl orig_tl)
55
| [], [], [] -> []
56
| _ -> assert false
57
  
58
let combine (f: expr list -> expr ) subs orig : ((expr * int) * expr) list  = 
59
  let elems = List.map (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in
60
  let all = List.fold_right IdSet.union elems IdSet.empty in
61
  List.map (fun v ->
62
    let active_subs = List.map (IdSet.mem v) elems in
63
    v, f (select v active_subs subs orig)
64
  ) (IdSet.elements all)
65

    
66

    
67
(* In a previous version, the printer was introducing fake
68
   description, ie tautologies, over inout variables to make sure they
69
   were not suppresed by some other algorithms *)
70

    
71
(* Takes the variable on which these coverage criteria will apply, as
72
   well as the expression and its negated version. Returns the expr
73
   and the variable expression, as well as the two new boolean
74
   expressions descibing the two associated modes. *)
75
let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =
76
  let loc = expr.expr_loc in
77
  let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in
78
  let expr1, expr2 =
79
    if nb_elems > 1 then 
80
      let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in
81
      let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in
82
      let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in
83
      expr1, expr2
84
    else
85
      vi_as_expr, not_vi_as_expr
86
  in
87
  ((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom
88
                                                     true while expr2
89
                                                     corresponds to atom
90
                                                     false *)
91

    
92
  (* Format.printf "%a@." Lustrec.Printers.pp_expr expr1;  *)
93
  (* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
94
  (*   Lustrec.Printers.pp_expr vi_as_expr *)
95
  (*   Lustrec.Printers.pp_expr expr (\*v*\) *)
96
  (*   Lustrec.Printers.pp_expr expr_neg_vi); *)
97
  (* Format.printf "%a@." Lustrec.Printers.pp_expr expr2;  *)
98
  (* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
99
  (*   Lustrec.Printers.pp_expr vi_as_expr *)
100
  (*   Lustrec.Printers.pp_expr expr (\*v*\) *)
101
  (*   Lustrec.Printers.pp_expr expr_neg_vi) *)
102
    
103
let rec compute_neg_expr cpt_pre (expr: Lustrec.Lustre_types.expr) =
104
  let neg_list l = 
105
    List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])
106
  in
107
  match expr.expr_desc with
108
  | Expr_tuple l -> 
109
     let vl, neg = neg_list l in
110
     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
111
     
112
  | Expr_ite (i,t,e) when (Lustrec.Types.is_bool_type t.expr_type) -> (
113
    let list = [i; t; e] in
114
    let vl, neg = neg_list list in
115
    vl, combine (fun l ->
116
            match l with
117
            | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
118
            | _ -> assert false
119
          ) neg list
120
  )
121
  | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
122
    let vl = gen_mcdc_cond_guard i in
123
    let list = [i; t; e] in
124
    let vl', neg = neg_list list in
125
    vl@vl', combine (fun l ->
126
                match l with
127
                | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
128
                | _ -> assert false
129
              ) neg list
130
  )
131
  | Expr_arrow (e1, e2) -> 
132
     let vl1, e1' = compute_neg_expr cpt_pre e1 in
133
     let vl2, e2' = compute_neg_expr cpt_pre e2 in
134
     vl1@vl2, combine (fun l -> match l with
135
                                | [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
136
                                | _ -> assert false
137
                ) [e1'; e2'] [e1; e2]
138

    
139
  | Expr_pre e ->
140
     let vl, e' = compute_neg_expr (cpt_pre+1) e in
141
     vl, List.map
142
           (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
143

    
144
  | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> 
145
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
146

    
147
  | Expr_appl (op_name, args, r) ->
148
     let vl, args' = compute_neg_expr cpt_pre args in
149
     vl, List.map 
150
           (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
151
           args'
152

    
153
  | Expr_ident _ when (Lustrec.Types.is_bool_type expr.expr_type) ->
154
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
155
  | _ -> [] (* empty vars *) , [] 
156
and gen_mcdc_cond_var v expr =
157
  report ~level:1 (fun fmt ->
158
      Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@."
159
        v
160
        Lustrec.Printers.pp_expr expr);
161
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
162
  let len = List.length leafs_n_neg_expr in 
163
  if len >= 1 then (
164
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
165
        (mcdc_var  (mk_pre nb_pre vi) len expr expr_neg_vi)::accu
166
      ) vl leafs_n_neg_expr
167
  )
168
  else
169
    vl
170

    
171
and gen_mcdc_cond_guard expr =
172
  report ~level:1 (fun fmt ->
173
      Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
174
        Lustrec.Printers.pp_expr expr);
175
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
176
  let len = List.length leafs_n_neg_expr in
177
  if len >= 1 then (
178
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
179
        (mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu
180
      ) vl leafs_n_neg_expr)
181
  else
182
    vl
183
  
184

    
185
let rec mcdc_expr cpt_pre expr = 
186
  match expr.expr_desc with
187
  | Expr_tuple l ->
188
     let vl =
189
       List.fold_right (fun e accu_v ->
190
	 let vl = mcdc_expr cpt_pre e in
191
	 (vl@accu_v))
192
	 l
193
	 []
194
     in
195
     vl
196
  | Expr_ite (i,t,e) ->
197
     let vl_i = gen_mcdc_cond_guard i in
198
     let vl_t = mcdc_expr cpt_pre t in
199
     let vl_e = mcdc_expr cpt_pre e in
200
     vl_i@vl_t@vl_e
201
  | Expr_arrow (e1, e2) ->
202
     let vl1 = mcdc_expr cpt_pre e1 in
203
     let vl2 = mcdc_expr cpt_pre e2 in
204
     vl1@vl2
205
  | Expr_pre e ->
206
     let vl = mcdc_expr (cpt_pre+1) e in
207
     vl
208
  | Expr_appl (f, args, r) ->
209
     let vl = mcdc_expr cpt_pre args in
210
     vl
211
  | _ -> []
212

    
213
let mcdc_var_def v expr = 
214
  if Lustrec.Types.is_bool_type expr.expr_type then
215
     let vl = gen_mcdc_cond_var v expr in
216
     vl
217
  else
218
    let vl = mcdc_expr 0 expr in
219
    vl
220
      
221
let mcdc_node_eq eq =
222
  let vl =
223
    match eq.eq_lhs, Lustrec.Types.is_bool_type eq.eq_rhs.expr_type, (Lustrec.Types.repr eq.eq_rhs.expr_type).Lustrec.Types.tdesc, eq.eq_rhs.expr_desc with
224
    | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
225
    | _::_, false, Lustrec.Types.Ttuple tl, Expr_tuple rhs ->
226
       (* We iterate trough pairs, but accumulate variables aside. The resulting
227
	  expression shall remain a tuple defintion *)
228
       let vl = List.fold_right2 (fun lhs rhs accu ->
229
	 let v = mcdc_var_def lhs rhs in
230
	 (* we don't care about the expression it. We focus on the coverage
231
	    expressions in v *)
232
	 v@accu
233
       ) eq.eq_lhs rhs []
234
       in
235
       vl
236
    | _ -> mcdc_expr 0 eq.eq_rhs 
237
  in
238
  vl
239

    
240
let mcdc_node_stmt stmt =
241
  match stmt with
242
  | Eq eq -> let vl = mcdc_node_eq eq in vl
243
  | Aut aut -> assert false
244

    
245
let mcdc_top_decl td = 
246
  match td.top_decl_desc with
247
  | Node nd ->
248
     let new_coverage_exprs =
249
       List.fold_right (
250
	   fun s accu_v ->
251
	   let vl' = mcdc_node_stmt s in
252
	   vl'@accu_v
253
	 ) nd.node_stmts []
254
     in
255
     (* We add coverage vars as boolean internal flows. *)
256
     let fresh_cov_defs = List.flatten (List.map (fun ((_, atom), expr_l) -> List.map (fun (atom_valid, case) -> atom, atom_valid, case) expr_l) new_coverage_exprs) in
257
     let nb_total = List.length fresh_cov_defs in
258
     let fresh_cov_vars = List.mapi (fun i (atom, atom_valid, cov_expr) ->
259
				     let loc = cov_expr.expr_loc in
260
				     Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
261
				     let cov_id = Format.flush_str_formatter () in
262
				     let cov_var = mkvar_decl loc
263
							      (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in
264
				     let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
265
				     cov_var, cov_def, atom, atom_valid
266
				    ) fresh_cov_defs
267
     in
268
     let fresh_vars, fresh_eqs =
269
       List.fold_right
270
	 (fun (v,eq,_,_) (accuv, accueq)-> v::accuv, eq::accueq )
271
	 fresh_cov_vars
272
	 ([], [])
273
     in
274
     let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for
275
			   kind2, and regular ones to keep track of the nature
276
			   of the annotations. *)
277
       List.map
278
	 (fun (v, _, atom, atom_valid) ->
279
	  let e = expr_of_vdecl v in
280
	  let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in
281
	  {annots =  [["PROPERTY"], neg_ee; (* Using negated property to force
282
                                               model-checker to produce a
283
                                               suitable covering trace *)
284
                      let loc = Lustrec.Location.dummy_loc in
285
		      let valid_e = let open Lustrec.Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in
286
		      ["coverage";"mcdc";v.var_id], expr_to_eexpr (Lustrec.Corelang.expr_of_expr_list loc [e; atom; valid_e])
287
		     ];
288
	   annot_loc = v.var_loc})
289
	 fresh_cov_vars
290
     in
291
     Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id;
292
     (* And add them as annotations --%PROPERTY: var TODO *)
293
     {td with top_decl_desc = Node {nd with
294
				     node_locals = nd.node_locals@fresh_vars;
295
				     node_stmts = nd.node_stmts@fresh_eqs;
296
				     node_annot = nd.node_annot@fresh_annots
297
				   }}
298
  | _ -> td
299

    
300

    
301
let mcdc prog =
302
  (* If main node is provided add silly constraints to show in/out variables in the path condition *)
303
  if !Lustrec.Options.main_node <> "" then (
304
    inout_vars := 
305
      let top = List.find 
306
	(fun td -> 
307
	  match td.top_decl_desc with 
308
	  | Node nd when nd.node_id = !Lustrec.Options.main_node -> true
309
	  | _ -> false) 
310
	prog 
311
      in
312
      match top.top_decl_desc with
313
      | Node nd -> nd.node_inputs @ nd.node_outputs
314
      | _ -> assert false);
315
  List.map mcdc_top_decl prog
316

    
317

    
318
    
319
(* Local Variables: *)
320
(* compile-command:"make -C .." *)
321
(* End: *)
322

    
323