Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/pathConditions.ml
1
open Lustre_types 
1
open Lustre_types
2 2
open Corelang
3 3
open Log
4 4

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

  
7
let inout_vars = ref [] 
8
  let compare = compare
9
end)
10

  
11
let inout_vars = ref []
8 12

  
9 13
(* This was used to add inout variables in the final signature. May have to be
10 14
   reactivated later *)
11
  
15

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

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

  
23
let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ]
28
let rel_op = [ "="; "!="; "<"; "<="; ">"; ">=" ]
24 29

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

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

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

  
38
(* let combine2 f sub1 sub2 = let elem_e1 = List.fold_right IdSet.add (List.map
39
   fst sub1) IdSet.empty in let elem_e2 = List.fold_right IdSet.add (List.map
40
   fst sub2) IdSet.empty in let common = IdSet.inter elem_e1 elem_e2 in let
41
   sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
42
   let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2
43
   in (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @ (List.map
44
   (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @ (List.map (fun v -> (v,
45
   {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)})
46
   (IdSet.elements common)) ) *)
65 47

  
66
(* In a previous version, the printer was introducing fake
67
   description, ie tautologies, over inout variables to make sure they
68
   were not suppresed by some other algorithms *)
48
let rec select (v : expr * int) (active : bool list)
49
    (modified : ((expr * int) * expr) list list) (orig : expr list) =
50
  match active, modified, orig with
51
  | true :: active_tl, e :: modified_tl, _ :: orig_tl ->
52
    List.assoc v e :: select v active_tl modified_tl orig_tl
53
  | false :: active_tl, _ :: modified_tl, e :: orig_tl ->
54
    e :: select v active_tl modified_tl orig_tl
55
  | [], [], [] ->
56
    []
57
  | _ ->
58
    assert false
69 59

  
70
(* Takes the variable on which these coverage criteria will apply, as
71
   well as the expression and its negated version. Returns the expr
72
   and the variable expression, as well as the two new boolean
73
   expressions descibing the two associated modes. *)
60
let combine (f : expr list -> expr) subs orig : ((expr * int) * expr) list =
61
  let elems =
62
    List.map
63
      (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty)
64
      subs
65
  in
66
  let all = List.fold_right IdSet.union elems IdSet.empty in
67
  List.map
68
    (fun v ->
69
      let active_subs = List.map (IdSet.mem v) elems in
70
      v, f (select v active_subs subs orig))
71
    (IdSet.elements all)
72

  
73
(* In a previous version, the printer was introducing fake description, ie
74
   tautologies, over inout variables to make sure they were not suppresed by
75
   some other algorithms *)
76

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

  
95
(* Format.printf "%a@." Printers.pp_expr expr1;  *)
96
(* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
97
(*   Printers.pp_expr vi_as_expr *)
98
(*   Printers.pp_expr expr (\*v*\) *)
99
(*   Printers.pp_expr expr_neg_vi); *)
100
(* Format.printf "%a@." Printers.pp_expr expr2;  *)
101
(* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
102
(*   Printers.pp_expr vi_as_expr *)
103
(*   Printers.pp_expr expr (\*v*\) *)
104
(*   Printers.pp_expr expr_neg_vi) *)
90 105

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

  
135
    ( vl @ vl',
136
      combine
137
        (fun l ->
138
          match l with
139
          | [ i'; t'; e' ] ->
140
            { expr with expr_desc = Expr_ite (i', t', e') }
141
          | _ ->
142
            assert false)
143
        neg list )
144
  | Expr_arrow (e1, e2) ->
145
    let vl1, e1' = compute_neg_expr cpt_pre e1 in
146
    let vl2, e2' = compute_neg_expr cpt_pre e2 in
147
    ( vl1 @ vl2,
148
      combine
149
        (fun l ->
150
          match l with
151
          | [ x; y ] ->
152
            { expr with expr_desc = Expr_arrow (x, y) }
153
          | _ ->
154
            assert false)
155
        [ e1'; e2' ] [ e1; e2 ] )
138 156
  | Expr_pre e ->
139
     let vl, e' = compute_neg_expr (cpt_pre+1) e in
140
     vl, List.map
141
           (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
142

  
157
    let vl, e' = compute_neg_expr (cpt_pre + 1) e in
158
    ( vl,
159
      List.map (fun (v, negv) -> v, { expr with expr_desc = Expr_pre negv }) e'
160
    )
143 161
  | Expr_appl (op_name, _, _) when List.mem op_name rel_op ->
144
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
145

  
162
    [], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ]
146 163
  | Expr_appl (op_name, args, r) ->
147
     let vl, args' = compute_neg_expr cpt_pre args in
148
     vl, List.map 
149
           (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
150
           args'
164
    let vl, args' = compute_neg_expr cpt_pre args in
165
    ( vl,
166
      List.map
167
        (fun (v, negv) ->
168
          v, { expr with expr_desc = Expr_appl (op_name, negv, r) })
169
        args' )
170
  | Expr_ident _ when Types.is_bool_type expr.expr_type ->
171
    [], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ]
172
  | _ ->
173
    [] (* empty vars *), []
151 174

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

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

  
184
let rec mcdc_expr cpt_pre expr = 
202
let rec mcdc_expr cpt_pre expr =
185 203
  match expr.expr_desc with
186 204
  | Expr_tuple l ->
187
     let vl =
188
       List.fold_right (fun e accu_v ->
189
	 let vl = mcdc_expr cpt_pre e in
190
	 (vl@accu_v))
191
	 l
192
	 []
193
     in
194
     vl
195
  | Expr_ite (i,t,e) ->
196
     let vl_i = gen_mcdc_cond_guard i in
197
     let vl_t = mcdc_expr cpt_pre t in
198
     let vl_e = mcdc_expr cpt_pre e in
199
     vl_i@vl_t@vl_e
205
    let vl =
206
      List.fold_right
207
        (fun e accu_v ->
208
          let vl = mcdc_expr cpt_pre e in
209
          vl @ accu_v)
210
        l []
211
    in
212
    vl
213
  | Expr_ite (i, t, e) ->
214
    let vl_i = gen_mcdc_cond_guard i in
215
    let vl_t = mcdc_expr cpt_pre t in
216
    let vl_e = mcdc_expr cpt_pre e in
217
    vl_i @ vl_t @ vl_e
200 218
  | Expr_arrow (e1, e2) ->
201
     let vl1 = mcdc_expr cpt_pre e1 in
202
     let vl2 = mcdc_expr cpt_pre e2 in
203
     vl1@vl2
219
    let vl1 = mcdc_expr cpt_pre e1 in
220
    let vl2 = mcdc_expr cpt_pre e2 in
221
    vl1 @ vl2
204 222
  | Expr_pre e ->
205
     let vl = mcdc_expr (cpt_pre+1) e in
206
     vl
223
    let vl = mcdc_expr (cpt_pre + 1) e in
224
    vl
207 225
  | Expr_appl (_, args, _) ->
208
     let vl = mcdc_expr cpt_pre args in
209
     vl
210
  | _ -> []
226
    let vl = mcdc_expr cpt_pre args in
227
    vl
228
  | _ ->
229
    []
211 230

  
212
let mcdc_var_def v expr = 
231
let mcdc_var_def v expr =
213 232
  if Types.is_bool_type expr.expr_type then
214
     let vl = gen_mcdc_cond_var v expr in
215
     vl
233
    let vl = gen_mcdc_cond_var v expr in
234
    vl
216 235
  else
217 236
    let vl = mcdc_expr 0 expr in
218 237
    vl
219
      
238

  
220 239
let mcdc_node_eq eq =
221 240
  let vl =
222
    match eq.eq_lhs, Types.is_bool_type eq.eq_rhs.expr_type, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
223
    | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
224
    | _::_, false, Types.Ttuple _, Expr_tuple rhs ->
225
       (* We iterate trough pairs, but accumulate variables aside. The resulting
226
	  expression shall remain a tuple defintion *)
227
       let vl = List.fold_right2 (fun lhs rhs accu ->
228
	 let v = mcdc_var_def lhs rhs in
229
	 (* we don't care about the expression it. We focus on the coverage
230
	    expressions in v *)
231
	 v@accu
232
       ) eq.eq_lhs rhs []
233
       in
234
       vl
235
    | _ -> mcdc_expr 0 eq.eq_rhs 
241
    match
242
      ( eq.eq_lhs,
243
        Types.is_bool_type eq.eq_rhs.expr_type,
244
        (Types.repr eq.eq_rhs.expr_type).Types.tdesc,
245
        eq.eq_rhs.expr_desc )
246
    with
247
    | [ lhs ], true, _, _ ->
248
      gen_mcdc_cond_var lhs eq.eq_rhs
249
    | _ :: _, false, Types.Ttuple _, Expr_tuple rhs ->
250
      (* We iterate trough pairs, but accumulate variables aside. The resulting
251
         expression shall remain a tuple defintion *)
252
      let vl =
253
        List.fold_right2
254
          (fun lhs rhs accu ->
255
            let v = mcdc_var_def lhs rhs in
256
            (* we don't care about the expression it. We focus on the coverage
257
               expressions in v *)
258
            v @ accu)
259
          eq.eq_lhs rhs []
260
      in
261
      vl
262
    | _ ->
263
      mcdc_expr 0 eq.eq_rhs
236 264
  in
237 265
  vl
238 266

  
239 267
let mcdc_node_stmt stmt =
240 268
  match stmt with
241
  | Eq eq -> let vl = mcdc_node_eq eq in vl
242
  | Aut _ -> assert false
269
  | Eq eq ->
270
    let vl = mcdc_node_eq eq in
271
    vl
272
  | Aut _ ->
273
    assert false
243 274

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

  
278
    let new_coverage_exprs =
279
      List.fold_right
280
        (fun s accu_v ->
281
          let vl' = mcdc_node_stmt s in
282
          vl' @ accu_v)
283
        nd.node_stmts []
284
    in
285
    (* We add coverage vars as boolean internal flows. *)
286
    let fresh_cov_defs =
287
      List.flatten
288
        (List.map
289
           (fun ((_, atom), expr_l) ->
290
             List.map (fun (atom_valid, case) -> atom, atom_valid, case) expr_l)
291
           new_coverage_exprs)
292
    in
293
    let nb_total = List.length fresh_cov_defs in
294
    let fresh_cov_vars =
295
      List.mapi
296
        (fun i (atom, atom_valid, cov_expr) ->
297
          let loc = cov_expr.expr_loc in
298
          Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
299
          let cov_id = Format.flush_str_formatter () in
300
          let cov_var =
301
            mkvar_decl loc
302
              ( cov_id,
303
                mktyp loc Tydec_bool,
304
                mkclock loc Ckdec_any,
305
                false,
306
                None,
307
                None )
308
          in
309
          let cov_def = Eq (mkeq loc ([ cov_id ], cov_expr)) in
310
          cov_var, cov_def, atom, atom_valid)
311
        fresh_cov_defs
312
    in
313
    let fresh_vars, fresh_eqs =
314
      List.fold_right
315
        (fun (v, eq, _, _) (accuv, accueq) -> v :: accuv, eq :: accueq)
316
        fresh_cov_vars ([], [])
317
    in
318
    let fresh_annots =
319
      (* We produce two sets of annotations: PROPERTY ones for kind2, and
320
         regular ones to keep track of the nature of the annotations. *)
321
      List.map
322
        (fun (v, _, atom, atom_valid) ->
323
          let e = expr_of_vdecl v in
324
          let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [ e ]) in
325
          {
326
            annots =
327
              [
328
                [ "PROPERTY" ], neg_ee;
329
                (* Using negated property to force model-checker to produce a
330
                   suitable covering trace *)
331
                (let loc = Location.dummy_loc in
332
                 let valid_e =
333
                   let open Corelang in
334
                   mkexpr loc (Expr_const (const_of_bool atom_valid))
335
                 in
336
                 ( [ "coverage"; "mcdc"; v.var_id ],
337
                   expr_to_eexpr
338
                     (Corelang.expr_of_expr_list loc [ e; atom; valid_e ]) ));
339
              ];
340
            annot_loc = v.var_loc;
341
          })
342
        fresh_cov_vars
343
    in
344
    Format.printf "%i coverage criteria generated for node %s@ " nb_total
345
      nd.node_id;
346
    (* And add them as annotations --%PROPERTY: var TODO *)
347
    {
348
      td with
349
      top_decl_desc =
350
        Node
351
          {
352
            nd with
353
            node_locals = nd.node_locals @ fresh_vars;
354
            node_stmts = nd.node_stmts @ fresh_eqs;
355
            node_annot = nd.node_annot @ fresh_annots;
356
          };
357
    }
358
  | _ ->
359
    td
299 360

  
300 361
let mcdc prog =
301
  (* If main node is provided add silly constraints to show in/out variables in the path condition *)
302
  if !Options.main_node <> "" then (
303
    inout_vars := 
304
      let top = List.find 
305
	(fun td -> 
306
	  match td.top_decl_desc with 
307
	  | Node nd when nd.node_id = !Options.main_node -> true
308
	  | _ -> false) 
309
	prog 
310
      in
311
      match top.top_decl_desc with
312
      | Node nd -> nd.node_inputs @ nd.node_outputs
313
      | _ -> assert false);
362
  (* If main node is provided add silly constraints to show in/out variables in
363
     the path condition *)
364
  (if !Options.main_node <> "" then
365
   inout_vars :=
366
     let top =
367
       List.find
368
         (fun td ->
369
           match td.top_decl_desc with
370
           | Node nd when nd.node_id = !Options.main_node ->
371
             true
372
           | _ ->
373
             false)
374
         prog
375
     in
376
     match top.top_decl_desc with
377
     | Node nd ->
378
       nd.node_inputs @ nd.node_outputs
379
     | _ ->
380
       assert false);
314 381
  List.map mcdc_top_decl prog
315 382

  
316

  
317
    
318 383
(* Local Variables: *)
319 384
(* compile-command:"make -C .." *)
320 385
(* End: *)
321

  
322
    

Also available in: Unified diff