## lustrec / src / pathConditions.ml @ ef8a361a

History | View | Annotate | Download (6.81 KB)

1 | 40d33d55 | xavier.thirioux | 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 | 2fdbc781 | ploc | | Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> ( |

63 | 40d33d55 | xavier.thirioux | let list = [i; t; e] in |

64 | let neg = List.map (compute_neg_expr cpt_pre) list in |
||

65 | 2fdbc781 | ploc | 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 | 40d33d55 | xavier.thirioux | | 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 | 2fdbc781 | ploc | 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 | 40d33d55 | xavier.thirioux | ) |

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 | 2fdbc781 | ploc | 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 | 40d33d55 | xavier.thirioux | | 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 | bde99c3f | xavier.thirioux | [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] |

95 | 40d33d55 | xavier.thirioux | |

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 | bde99c3f | xavier.thirioux | [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] |

103 | 40d33d55 | xavier.thirioux | | _ -> [] |

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 | bde99c3f | xavier.thirioux | let mcdc_node_stmt stmt = |

149 | match stmt with |
||

150 | | Eq eq -> mcdc_node_eq eq |
||

151 | | Aut aut -> assert false |
||

152 | |||

153 | 40d33d55 | xavier.thirioux | let mcdc_top_decl td = |

154 | match td.top_decl_desc with |
||

155 | bde99c3f | xavier.thirioux | | Node nd -> List.iter mcdc_node_stmt nd.node_stmts |

156 | 40d33d55 | xavier.thirioux | | _ -> () |

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 | (* compile-command:"make -C .." *) |
||

177 | (* End: *) |
||

178 | |||

179 |