lustrec / src / pathConditions.ml @ 7ecfca04
History  View  Annotate  Download (6.67 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 [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_unary_call Location.dummy_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_unary_call Location.dummy_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 s = 
137 
match s with Eq eq > mcdc_node_eq eq  _ > assert false (* should have been removed by now *) 
138 

139 
let mcdc_top_decl td = 
140 
match td.top_decl_desc with 
141 
 Node nd > List.iter mcdc_node_stmt nd.node_stmts 
142 
 _ > () 
143  
144  
145 
let mcdc prog = 
146 
(* If main node is provided add silly constraints to show in/out variables in the path condition *) 
147 
if !Options.main_node <> "" then ( 
148 
inout_vars := 
149 
let top = List.find 
150 
(fun td > 
151 
match td.top_decl_desc with 
152 
 Node nd when nd.node_id = !Options.main_node > true 
153 
 _ > false) 
154 
prog 
155 
in 
156 
match top.top_decl_desc with 
157 
 Node nd > nd.node_inputs @ nd.node_outputs 
158 
 _ > assert false); 
159 
List.iter mcdc_top_decl prog 
160  
161 
(* Local Variables: *) 
162 
(* compilecommand:"make C .." *) 
163 
(* End: *) 
164  
165 
