## lustrec/src/pathConditions.ml @ 7ecfca04

1 | f29f1bee | ploc | open LustreSpec |
---|---|---|---|

2 | 53bdad2b | ploc | 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 | f29f1bee | ploc | 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 | 53bdad2b | ploc | let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ] |

22 | f29f1bee | ploc | |

23 | 53bdad2b | ploc | 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_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 | 4e66a853 | ploc | if List.length leafs_n_neg_expr > 1 then ( |

98 | List.iter (fun ((vi, nb_pre), expr_neg_vi) -> |
||

99 | f29f1bee | ploc | 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 | 4e66a853 | ploc | ) leafs_n_neg_expr |

102 | ```
)
``` |
||

103 | 53bdad2b | ploc | |

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 | 4e66a853 | ploc | if List.length leafs_n_neg_expr > 1 then ( |

108 | List.iter (fun ((vi, nb_pre), expr_neg_vi) -> |
||

109 | f29f1bee | ploc | 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 | 4e66a853 | ploc | |

112 | ) leafs_n_neg_expr |
||

113 | ```
)
``` |
||

114 | 53bdad2b | ploc | |

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 | 7ecfca04 | ploc | 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 | 53bdad2b | ploc | let mcdc_top_decl td = |

140 | match td.top_decl_desc with |
||

141 | 7ecfca04 | ploc | | Node nd -> List.iter mcdc_node_stmt nd.node_stmts |

142 | 53bdad2b | ploc | | _ -> () |

143 | |||

144 | f29f1bee | ploc | |

145 | 53bdad2b | ploc | let mcdc prog = |

146 | f29f1bee | ploc | ```
(* 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 | 53bdad2b | ploc | List.iter mcdc_top_decl prog |

160 | |||

161 | ```
(* Local Variables: *)
``` |
||

162 | ```
(* compile-command:"make -C .." *)
``` |
||

163 | ```
(* End: *)
``` |
||

164 | |||

165 |