Project

General

Profile

Revision 3769b712 src/pathConditions.ml

View differences:

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

  
6 6
module IdSet = Set.Make (struct type t = expr * int let compare = compare end)
......
11 11
   reactivated later *)
12 12
  
13 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 *)
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 18
(*   | _ -> Format.fprintf fmt "(true)" *)
19 19

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

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

  
......
89 89
                                                     corresponds to atom
90 90
                                                     false *)
91 91

  
92
  (* Format.printf "%a@." Printers.pp_expr expr1;  *)
92
  (* Format.printf "%a@." Lustrec.Printers.pp_expr expr1;  *)
93 93
  (* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
94
  (*   Printers.pp_expr vi_as_expr *)
95
  (*   Printers.pp_expr expr (\*v*\) *)
96
  (*   Printers.pp_expr expr_neg_vi); *)
97
  (* Format.printf "%a@." Printers.pp_expr expr2;  *)
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 98
  (* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
99
  (*   Printers.pp_expr vi_as_expr *)
100
  (*   Printers.pp_expr expr (\*v*\) *)
101
  (*   Printers.pp_expr expr_neg_vi) *)
99
  (*   Lustrec.Printers.pp_expr vi_as_expr *)
100
  (*   Lustrec.Printers.pp_expr expr (\*v*\) *)
101
  (*   Lustrec.Printers.pp_expr expr_neg_vi) *)
102 102
    
103
let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) =
103
let rec compute_neg_expr cpt_pre (expr: Lustrec.Lustre_types.expr) =
104 104
  let neg_list l = 
105 105
    List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])
106 106
  in
......
109 109
     let vl, neg = neg_list l in
110 110
     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
111 111
     
112
  | Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> (
112
  | Expr_ite (i,t,e) when (Lustrec.Types.is_bool_type t.expr_type) -> (
113 113
    let list = [i; t; e] in
114 114
    let vl, neg = neg_list list in
115 115
    vl, combine (fun l ->
......
150 150
           (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
151 151
           args'
152 152

  
153
  | Expr_ident _ when (Types.is_bool_type expr.expr_type) ->
153
  | Expr_ident _ when (Lustrec.Types.is_bool_type expr.expr_type) ->
154 154
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
155 155
  | _ -> [] (* empty vars *) , [] 
156 156
and gen_mcdc_cond_var v expr =
157 157
  report ~level:1 (fun fmt ->
158 158
      Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@."
159 159
        v
160
        Printers.pp_expr expr);
160
        Lustrec.Printers.pp_expr expr);
161 161
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
162 162
  let len = List.length leafs_n_neg_expr in 
163 163
  if len >= 1 then (
......
171 171
and gen_mcdc_cond_guard expr =
172 172
  report ~level:1 (fun fmt ->
173 173
      Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
174
        Printers.pp_expr expr);
174
        Lustrec.Printers.pp_expr expr);
175 175
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
176 176
  let len = List.length leafs_n_neg_expr in
177 177
  if len >= 1 then (
......
211 211
  | _ -> []
212 212

  
213 213
let mcdc_var_def v expr = 
214
  if Types.is_bool_type expr.expr_type then
214
  if Lustrec.Types.is_bool_type expr.expr_type then
215 215
     let vl = gen_mcdc_cond_var v expr in
216 216
     vl
217 217
  else
......
220 220
      
221 221
let mcdc_node_eq eq =
222 222
  let vl =
223
    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
    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 224
    | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
225
    | _::_, false, Types.Ttuple tl, Expr_tuple rhs ->
225
    | _::_, false, Lustrec.Types.Ttuple tl, Expr_tuple rhs ->
226 226
       (* We iterate trough pairs, but accumulate variables aside. The resulting
227 227
	  expression shall remain a tuple defintion *)
228 228
       let vl = List.fold_right2 (fun lhs rhs accu ->
......
281 281
	  {annots =  [["PROPERTY"], neg_ee; (* Using negated property to force
282 282
                                               model-checker to produce a
283 283
                                               suitable covering trace *)
284
                      let loc = Location.dummy_loc in
285
		      let valid_e = let open Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in
286
		      ["coverage";"mcdc";v.var_id], expr_to_eexpr (Corelang.expr_of_expr_list loc [e; atom; valid_e])
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 287
		     ];
288 288
	   annot_loc = v.var_loc})
289 289
	 fresh_cov_vars
......
300 300

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

Also available in: Unified diff