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

