Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / pathConditions.ml @ ef8a361a

History | View | Annotate | Download (6.81 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_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 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
(* compile-command:"make -C .." *)
177
(* End: *)
178

    
179