lustrec / src / pathConditions.ml @ 37419cf4
History  View  Annotate  Download (6.81 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_pre1) 
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 l > 
66 
match l with 
67 
 [i'; t'; e'] > {expr with expr_desc = Expr_ite(i', t', e')} 
68 
 _ > assert false 
69 
) neg list 
70 
) 
71 
 Expr_ite (i,t,e) > ( (* We return the guard as a new guard *) 
72 
gen_mcdc_cond_guard i; 
73 
let list = [i; t; e] in 
74 
let neg = List.map (compute_neg_expr cpt_pre) list in 
75 
combine (fun l > 
76 
match l with 
77 
 [i'; t'; e'] > {expr with expr_desc = Expr_ite(i', t', e')} 
78 
 _ > assert false 
79 
) neg list 
80 
) 
81 
 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) 
92  
93 
 Expr_appl (op_name, args, r) when List.mem op_name rel_op > 
94 
[(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] 
95  
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) 
100  
101 
 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 
109 
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 
114 
) 
115  
116 
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 
119 
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 
) 
126 

127  
128 
let rec mcdc_expr cpt_pre expr = 
129 
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 
 _ > () 
136  
137 
let mcdc_var_def v expr = 
138 
match (Types.repr expr.expr_type).Types.tdesc with 
139 
 Types.Tbool > gen_mcdc_cond_var v expr 
140 
 _ > mcdc_expr 0 expr 
141  
142 
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 
147  
148 
let mcdc_node_stmt stmt = 
149 
match stmt with 
150 
 Eq eq > mcdc_node_eq eq 
151 
 Aut aut > assert false 
152  
153 
let mcdc_top_decl td = 
154 
match td.top_decl_desc with 
155 
 Node nd > List.iter mcdc_node_stmt nd.node_stmts 
156 
 _ > () 
157  
158  
159 
let mcdc prog = 
160 
(* If main node is provided add silly constraints to show in/out variables in the path condition *) 
161 
if !Options.main_node <> "" then ( 
162 
inout_vars := 
163 
let top = List.find 
164 
(fun td > 
165 
match td.top_decl_desc with 
166 
 Node nd when nd.node_id = !Options.main_node > true 
167 
 _ > false) 
168 
prog 
169 
in 
170 
match top.top_decl_desc with 
171 
 Node nd > nd.node_inputs @ nd.node_outputs 
172 
 _ > assert false); 
173 
List.iter mcdc_top_decl prog 
174  
175 
(* Local Variables: *) 
176 
(* compilecommand:"make C .." *) 
177 
(* End: *) 
178  
179 
