Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / pathConditions.ml @ bde99c3f

History | View | Annotate | Download (6.63 KB)

1
open LustreSpec 
2
open Corelang
3
open 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
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)"
16

    
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

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

    
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
  )
29
(*
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))      )
39
*)
40

    
41
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =
42
match active, modified, orig with
43
| true::active_tl, e::modified_tl, _::orig_tl -> (List.assoc v e)::(select v active_tl modified_tl orig_tl)
44
| false::active_tl, _::modified_tl, e::orig_tl -> e::(select v active_tl modified_tl orig_tl)
45
| [], [], [] -> []
46
| _ -> assert false
47
  
48
let combine (f: expr list -> expr ) subs orig : ((expr * int) * expr) list  = 
49
  let elems = List.map (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in
50
  let all = List.fold_right IdSet.union elems IdSet.empty in
51
  List.map (fun v ->
52
    let active_subs = List.map (IdSet.mem v) elems in
53
    v, f (select v active_subs subs orig)
54
  ) (IdSet.elements all)
55

    
56
let rec compute_neg_expr cpt_pre expr = 
57
  match expr.expr_desc with
58
  | 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

    
62
  | Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> 
63
    let list = [i; t; e] in
64
    let neg = List.map (compute_neg_expr cpt_pre) list in
65
    combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
66
  | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
67
    gen_mcdc_cond_guard i;
68
    let list = [i; t; e] in
69
    let neg = List.map (compute_neg_expr cpt_pre) list in
70
    combine (fun [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}) neg list
71
  )
72
  | Expr_arrow (e1, e2) -> 
73
    let e1' = compute_neg_expr cpt_pre e1 in
74
    let e2' = compute_neg_expr cpt_pre e2 in
75
    combine (fun [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }) [e1'; e2'] [e1; e2]
76
  | Expr_pre e -> 
77
    List.map 
78
      (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } ))
79
      (compute_neg_expr (cpt_pre+1) e)
80

    
81
  | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> 
82
    [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
83

    
84
  | Expr_appl (op_name, args, r) -> 
85
    List.map 
86
      (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
87
	(compute_neg_expr cpt_pre args)
88

    
89
  | Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool ->
90
    [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
91
  | _ -> []
92

    
93
and  
94
 gen_mcdc_cond_var v expr =
95
  report ~level:1 (fun fmt -> Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." v Printers.pp_expr expr);
96
  let leafs_n_neg_expr = compute_neg_expr 0 expr in
97
  if List.length leafs_n_neg_expr > 1 then (
98
    List.iter (fun ((vi, nb_pre), expr_neg_vi) -> 
99
      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);
100
      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)
101
    ) leafs_n_neg_expr
102
  )
103

    
104
and gen_mcdc_cond_guard expr =
105
  report ~level:1 (fun fmt -> Format.fprintf fmt".. Generating MC/DC cond for guard %a@." Printers.pp_expr expr);
106
  let leafs_n_neg_expr = compute_neg_expr 0 expr in
107
  if List.length leafs_n_neg_expr > 1 then (
108
    List.iter (fun ((vi, nb_pre), expr_neg_vi) -> 
109
      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);
110
      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)
111
   
112
 ) leafs_n_neg_expr
113
  )
114
  
115

    
116
let rec mcdc_expr cpt_pre expr = 
117
  match expr.expr_desc with
118
  | Expr_tuple l -> List.iter (mcdc_expr cpt_pre) l
119
  | Expr_ite (i,t,e) -> (gen_mcdc_cond_guard i; List.iter (mcdc_expr cpt_pre) [t; e])
120
  | Expr_arrow (e1, e2) -> List.iter (mcdc_expr cpt_pre) [e1; e2]
121
  | Expr_pre e -> mcdc_expr (cpt_pre+1) e 
122
  | Expr_appl (_, args, _) -> mcdc_expr cpt_pre args
123
  | _ -> ()
124

    
125
let mcdc_var_def v expr = 
126
  match (Types.repr expr.expr_type).Types.tdesc with
127
  | Types.Tbool -> gen_mcdc_cond_var v expr
128
  | _ -> mcdc_expr 0 expr
129

    
130
let mcdc_node_eq eq =
131
  match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
132
  | [lhs], Types.Tbool, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
133
  | _::_, Types.Ttuple tl, Expr_tuple rhs -> List.iter2 mcdc_var_def eq.eq_lhs rhs
134
  | _ -> mcdc_expr 0 eq.eq_rhs 
135

    
136
let mcdc_node_stmt stmt =
137
  match stmt with
138
  | Eq eq -> mcdc_node_eq eq
139
  | Aut aut -> assert false
140

    
141
let mcdc_top_decl td = 
142
  match td.top_decl_desc with
143
  | Node nd -> List.iter mcdc_node_stmt nd.node_stmts
144
  | _ -> ()
145

    
146

    
147
let mcdc prog =
148
  (* If main node is provided add silly constraints to show in/out variables in the path condition *)
149
  if !Options.main_node <> "" then (
150
    inout_vars := 
151
      let top = List.find 
152
	(fun td -> 
153
	  match td.top_decl_desc with 
154
	  | Node nd when nd.node_id = !Options.main_node -> true
155
	  | _ -> false) 
156
	prog 
157
      in
158
      match top.top_decl_desc with
159
      | Node nd -> nd.node_inputs @ nd.node_outputs
160
      | _ -> assert false);
161
  List.iter mcdc_top_decl prog
162

    
163
(* Local Variables: *)
164
(* compile-command:"make -C .." *)
165
(* End: *)
166

    
167