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

