Project

General

Profile

Revision 3e1d20e0 src/pathConditions.ml

View differences:

src/pathConditions.ml
7 7

  
8 8
let inout_vars = ref [] 
9 9

  
10
let print_tautology_var fmt v =
11
  match (Types.repr v.var_type).Types.tdesc with
12
  | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id
13
  | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
14
  | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
15
  | _ -> Format.fprintf fmt "(true)"
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 (Types.repr v.var_type).Types.tdesc with *)
15
(*   | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *)
16
(*   | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
17
(*   | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
18
(*   | _ -> Format.fprintf fmt "(true)" *)
16 19

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

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

  
23
let rec print_pre fmt nb_pre =
24
  if nb_pre <= 0 then () 
25
  else (
26
    Format.fprintf fmt "pre ";
27
    print_pre fmt (nb_pre-1)
28
  )
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
   
29 39
(*
30
let combine2 f sub1 sub2 = 
31
    let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in
32
    let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in
33
    let common = IdSet.inter elem_e1 elem_e2 in
34
    let sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
35
    let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2 in
36
    (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @
37
      (List.map (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @
38
      (List.map (fun v -> (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common))      )
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))      )
39 49
*)
40 50

  
41 51
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =
......
53 63
    v, f (select v active_subs subs orig)
54 64
  ) (IdSet.elements all)
55 65

  
56
let rec compute_neg_expr cpt_pre expr = 
66

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

  
71
(* Takes the variable on which these coverage criteria will apply, as well as
72
   the expression and its negated version. Returns the expr and the variable
73
   expression, as well as the two new boolean expressions descibing the two
74
   associated modes. *)
75
let mcdc_var vi_as_expr expr expr_neg_vi =
76
  let loc = expr.expr_loc in
77
  let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in
78
  let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in
79
  let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in
80
  let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in
81
  ((expr,vi_as_expr),[expr1;expr2])
82

  
83
  (* Format.printf "%a@." Printers.pp_expr expr1;  *)
84
  (* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
85
  (*   Printers.pp_expr vi_as_expr *)
86
  (*   Printers.pp_expr expr (\*v*\) *)
87
  (*   Printers.pp_expr expr_neg_vi); *)
88
  (* Format.printf "%a@." Printers.pp_expr expr2;  *)
89
  (* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
90
  (*   Printers.pp_expr vi_as_expr *)
91
  (*   Printers.pp_expr expr (\*v*\) *)
92
  (*   Printers.pp_expr expr_neg_vi) *)
93
    
94
let rec compute_neg_expr cpt_pre (expr: LustreSpec.expr) =
95
  let neg_list l = 
96
    List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])
97
  in
57 98
  match expr.expr_desc with
58 99
  | Expr_tuple l -> 
59
    let neg = List.map (compute_neg_expr cpt_pre) l in
60
    combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
61

  
100
     let vl, neg = neg_list l in
101
     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
102
       
62 103
  | Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> (
63 104
    let list = [i; t; e] in
64
    let neg = List.map (compute_neg_expr cpt_pre) list in
65
    combine (fun l ->
105
    let vl, neg = neg_list list in
106
    vl, combine (fun l ->
66 107
      match l with
67 108
      | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
68 109
      | _ -> assert false
69 110
    ) neg list
70 111
  )
71 112
  | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
72
    gen_mcdc_cond_guard i;
113
    let vl = gen_mcdc_cond_guard i in
73 114
    let list = [i; t; e] in
74
    let neg = List.map (compute_neg_expr cpt_pre) list in
75
    combine (fun l ->
115
    let vl', neg = neg_list list in
116
    vl@vl', combine (fun l ->
76 117
      match l with
77 118
      | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
78 119
      | _ -> assert false
79 120
    ) neg list
80 121
  )
81 122
  | Expr_arrow (e1, e2) -> 
82
    let e1' = compute_neg_expr cpt_pre e1 in
83
    let e2' = compute_neg_expr cpt_pre e2 in
84
    combine (fun l -> match l with
85
    | [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
86
    | _ -> assert false
87
    ) [e1'; e2'] [e1; e2]
88
  | Expr_pre e -> 
89
    List.map 
90
      (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } ))
91
      (compute_neg_expr (cpt_pre+1) e)
123
     let vl1, e1' = compute_neg_expr cpt_pre e1 in
124
     let vl2, e2' = compute_neg_expr cpt_pre e2 in
125
     vl1@vl2, combine (fun l -> match l with
126
     | [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
127
     | _ -> assert false
128
     ) [e1'; e2'] [e1; e2]
129

  
130
  | Expr_pre e ->
131
     let vl, e' = compute_neg_expr (cpt_pre+1) e in
132
     vl, List.map
133
       (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
92 134

  
93 135
  | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> 
94
    [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
136
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
95 137

  
96
  | Expr_appl (op_name, args, r) -> 
97
    List.map 
98
      (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
99
	(compute_neg_expr cpt_pre args)
138
  | Expr_appl (op_name, args, r) ->
139
     let vl, args' = compute_neg_expr cpt_pre args in
140
     vl, List.map 
141
       (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
142
       args'
100 143

  
101 144
  | Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool ->
102
    [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
103
  | _ -> []
104

  
105
and  
106
 gen_mcdc_cond_var v expr =
107
  report ~level:1 (fun fmt -> Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." v Printers.pp_expr expr);
108
  let leafs_n_neg_expr = compute_neg_expr 0 expr in
145
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
146
  | _ -> [] (* empty vars *) , [] 
147
and gen_mcdc_cond_var v expr =
148
  report ~level:1 (fun fmt ->
149
    Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@."
150
      v
151
      Printers.pp_expr expr);
152
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
109 153
  if List.length leafs_n_neg_expr > 1 then (
110
    List.iter (fun ((vi, nb_pre), expr_neg_vi) -> 
111
      print_path (fun fmt -> Format.fprintf fmt "%a%a and (%s != %a)" print_pre nb_pre Printers.pp_expr vi v Printers.pp_expr expr_neg_vi);
112
      print_path (fun fmt -> Format.fprintf fmt "(not %a%a) and (%s != %a)" print_pre nb_pre Printers.pp_expr vi v Printers.pp_expr expr_neg_vi)
113
    ) leafs_n_neg_expr
154
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
155
      (mcdc_var  (mk_pre nb_pre vi) expr expr_neg_vi)::accu
156
    ) vl leafs_n_neg_expr
114 157
  )
158
  else vl
115 159

  
116 160
and gen_mcdc_cond_guard expr =
117
  report ~level:1 (fun fmt -> Format.fprintf fmt".. Generating MC/DC cond for guard %a@." Printers.pp_expr expr);
118
  let leafs_n_neg_expr = compute_neg_expr 0 expr in
161
  report ~level:1 (fun fmt ->
162
    Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
163
      Printers.pp_expr expr);
164
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
119 165
  if List.length leafs_n_neg_expr > 1 then (
120
    List.iter (fun ((vi, nb_pre), expr_neg_vi) -> 
121
      print_path (fun fmt -> Format.fprintf fmt "%a%a and (%a != %a)" print_pre nb_pre Printers.pp_expr vi Printers.pp_expr expr Printers.pp_expr expr_neg_vi);
122
      print_path (fun fmt -> Format.fprintf fmt  "(not %a%a) and (%a != %a)" print_pre nb_pre  Printers.pp_expr vi Printers.pp_expr expr Printers.pp_expr expr_neg_vi)
123
   
124
 ) leafs_n_neg_expr
125
  )
166
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
167
      (mcdc_var  (mk_pre nb_pre vi) expr expr_neg_vi)::accu
168
    ) vl leafs_n_neg_expr)
169
  else
170
    vl
126 171
  
127 172

  
128 173
let rec mcdc_expr cpt_pre expr = 
129 174
  match expr.expr_desc with
130
  | Expr_tuple l -> List.iter (mcdc_expr cpt_pre) l
131
  | Expr_ite (i,t,e) -> (gen_mcdc_cond_guard i; List.iter (mcdc_expr cpt_pre) [t; e])
132
  | Expr_arrow (e1, e2) -> List.iter (mcdc_expr cpt_pre) [e1; e2]
133
  | Expr_pre e -> mcdc_expr (cpt_pre+1) e 
134
  | Expr_appl (_, args, _) -> mcdc_expr cpt_pre args
135
  | _ -> ()
175
  | Expr_tuple l ->
176
     let vl =
177
       List.fold_right (fun e accu_v ->
178
	 let vl = mcdc_expr cpt_pre e in
179
	 (vl@accu_v))
180
	 l
181
	 []
182
     in
183
     vl
184
  | Expr_ite (i,t,e) ->
185
     let vl_i = gen_mcdc_cond_guard i in
186
     let vl_t = mcdc_expr cpt_pre t in
187
     let vl_e = mcdc_expr cpt_pre e in
188
     vl_i@vl_t@vl_e
189
  | Expr_arrow (e1, e2) ->
190
     let vl1 = mcdc_expr cpt_pre e1 in
191
     let vl2 = mcdc_expr cpt_pre e2 in
192
     vl1@vl2
193
  | Expr_pre e ->
194
     let vl = mcdc_expr (cpt_pre+1) e in
195
     vl
196
  | Expr_appl (f, args, r) ->
197
     let vl = mcdc_expr cpt_pre args in
198
     vl
199
  | _ -> []
136 200

  
137 201
let mcdc_var_def v expr = 
138 202
  match (Types.repr expr.expr_type).Types.tdesc with
139
  | Types.Tbool -> gen_mcdc_cond_var v expr
140
  | _ -> mcdc_expr 0 expr
203
  | Types.Tbool ->
204
     let vl = gen_mcdc_cond_var v expr in
205
     vl
206
  | _ -> let vl = mcdc_expr 0 expr in
207
	 vl
141 208

  
142 209
let mcdc_node_eq eq =
143
  match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
144
  | [lhs], Types.Tbool, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
145
  | _::_, Types.Ttuple tl, Expr_tuple rhs -> List.iter2 mcdc_var_def eq.eq_lhs rhs
146
  | _ -> mcdc_expr 0 eq.eq_rhs 
210
  let vl =
211
    match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
212
    | [lhs], Types.Tbool, _ ->  gen_mcdc_cond_var lhs eq.eq_rhs 
213
    | _::_, Types.Ttuple tl, Expr_tuple rhs ->
214
       (* We iterate trough pairs, but accumulate variables aside. The resulting
215
	  expression shall remain a tuple defintion *)
216
       let vl = List.fold_right2 (fun lhs rhs accu ->
217
	 let v = mcdc_var_def lhs rhs in
218
	 (* we don't care about the expression it. We focus on the coverage
219
	    expressions in v *)
220
	 v@accu
221
       ) eq.eq_lhs rhs []
222
       in
223
       vl
224
    | _ -> mcdc_expr 0 eq.eq_rhs 
225
  in
226
  vl
147 227

  
148 228
let mcdc_node_stmt stmt =
149 229
  match stmt with
150
  | Eq eq -> mcdc_node_eq eq
230
  | Eq eq -> let vl = mcdc_node_eq eq in vl
151 231
  | Aut aut -> assert false
152 232

  
153 233
let mcdc_top_decl td = 
154 234
  match td.top_decl_desc with
155
  | Node nd -> List.iter mcdc_node_stmt nd.node_stmts
156
  | _ -> ()
235
  | Node nd ->
236
     let new_coverage_exprs =
237
       List.fold_right (
238
	 fun s accu_v ->
239
	   let vl' = mcdc_node_stmt s in
240
	   vl'@accu_v
241
       ) nd.node_stmts []
242
     in
243
     (* We add coverage vars as boolean internal flows. TODO *)
244
     let fresh_cov_defs = List.flatten (List.map snd new_coverage_exprs) in
245
     let nb_total = List.length fresh_cov_defs in
246
     let fresh_cov_vars = List.mapi (fun i cov_expr ->
247
       let loc = cov_expr.expr_loc in
248
       Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
249
       let cov_id = Format.flush_str_formatter () in
250
       let cov_var = mkvar_decl loc
251
	 (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None) in
252
       let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
253
       cov_var, cov_def
254
     ) fresh_cov_defs
255
     in
256
     let fresh_vars, fresh_eqs = List.split fresh_cov_vars in
257
     let fresh_annots =
258
       List.map
259
	 (fun v -> {annots =  [["PROPERTY"], expr_to_eexpr (expr_of_vdecl v)]; annot_loc = td.top_decl_loc})
260
	 fresh_vars in
261
     Format.printf "We have %i coverage criteria for node %s@." nb_total nd.node_id;
262
     (* And add them as annotations --%PROPERTY: var TODO *)
263
     {td with top_decl_desc = Node {nd with
264
       node_locals = nd.node_locals@fresh_vars;
265
       node_stmts = nd.node_stmts@fresh_eqs;
266
       node_annot = nd.node_annot@fresh_annots
267
     }}
268
  | _ -> td
157 269

  
158 270

  
159 271
let mcdc prog =
......
170 282
      match top.top_decl_desc with
171 283
      | Node nd -> nd.node_inputs @ nd.node_outputs
172 284
      | _ -> assert false);
173
  List.iter mcdc_top_decl prog
285
  List.map mcdc_top_decl prog
174 286

  
175 287
(* Local Variables: *)
176 288
(* compile-command:"make -C .." *)

Also available in: Unified diff