From 3e1d20e05c22094981f9dc271b015ffa498c97ed Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Wed, 15 Nov 2017 00:12:57 -0800
Subject: [PATCH] [MCDC] Solved some issues and transformed the code from
iterators to fold
---
src/corelang.ml | 67 ++++-----
src/corelang.mli | 2 +-
src/main_lustre_testgen.ml | 12 +-
src/pathConditions.ml | 278 ++++++++++++++++++++++++++-----------
4 files changed, 241 insertions(+), 118 deletions(-)
diff --git a/src/corelang.ml b/src/corelang.ml
index 694ba1b5..3f335713 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -894,45 +894,46 @@ let rec substitute_expr vars_to_replace defs e =
ed
}
-(* FAUT IL RETIRER ?
let rec expr_to_eexpr expr =
{ eexpr_tag = expr.expr_tag;
- eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
+ eexpr_qfexpr = expr;
+ eexpr_quantifiers = [];
eexpr_type = expr.expr_type;
eexpr_clock = expr.expr_clock;
- eexpr_loc = expr.expr_loc
+ eexpr_loc = expr.expr_loc;
+ eexpr_normalized = None
}
- and expr_desc_to_eexpr_desc expr_desc =
- let conv = expr_to_eexpr in
- match expr_desc with
- | Expr_const c -> EExpr_const (match c with
- | Const_int x -> EConst_int x
- | Const_real x -> EConst_real x
- | Const_float x -> EConst_float x
- | Const_tag x -> EConst_tag x
- | _ -> assert false
-
- )
- | Expr_ident i -> EExpr_ident i
- | Expr_tuple el -> EExpr_tuple (List.map conv el)
-
- | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)
- | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
- | Expr_pre e' -> EExpr_pre (conv e')
- | Expr_appl (i, e', i') ->
- EExpr_appl
- (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
-
- | Expr_when _
- | Expr_merge _ -> assert false
- | Expr_array _
- | Expr_access _
- | Expr_power _ -> assert false
- | Expr_ite (c, t, e) -> assert false
- | _ -> assert false
-
- *)
+ (* and expr_desc_to_eexpr_desc expr_desc = *)
+ (* let conv = expr_to_eexpr in *)
+ (* match expr_desc with *)
+ (* | Expr_const c -> EExpr_const (match c with *)
+ (* | Const_int x -> EConst_int x *)
+ (* | Const_real x -> EConst_real x *)
+ (* | Const_float x -> EConst_float x *)
+ (* | Const_tag x -> EConst_tag x *)
+ (* | _ -> assert false *)
+
+ (* ) *)
+ (* | Expr_ident i -> EExpr_ident i *)
+ (* | Expr_tuple el -> EExpr_tuple (List.map conv el) *)
+
+ (* | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) *)
+ (* | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *)
+ (* | Expr_pre e' -> EExpr_pre (conv e') *)
+ (* | Expr_appl (i, e', i') -> *)
+ (* EExpr_appl *)
+ (* (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *)
+
+ (* | Expr_when _ *)
+ (* | Expr_merge _ -> assert false *)
+ (* | Expr_array _ *)
+ (* | Expr_access _ *)
+ (* | Expr_power _ -> assert false *)
+ (* | Expr_ite (c, t, e) -> assert false *)
+ (* | _ -> assert false *)
+
+
let rec get_expr_calls nodes e =
let get_calls = get_expr_calls nodes in
match e.expr_desc with
diff --git a/src/corelang.mli b/src/corelang.mli
index 20bb6786..ea020ab9 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -98,7 +98,7 @@ val call_of_expr: expr -> (ident * expr list * expr option)
val expr_of_dimension: Dimension.dim_expr -> expr
val dimension_of_expr: expr -> Dimension.dim_expr
val dimension_of_const: Location.t -> constant -> Dimension.dim_expr
-
+val expr_to_eexpr: expr -> eexpr
(* REMOVED, pushed in utils.ml val new_tag : unit -> tag *)
val add_internal_funs: unit -> unit
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index 85b4feac..e9d39e1b 100644
--- a/src/main_lustre_testgen.ml
+++ b/src/main_lustre_testgen.ml
@@ -54,7 +54,17 @@ let testgen_source dirname basename extension =
*)
if !Options.gen_mcdc then (
- PathConditions.mcdc prog;
+ let prog_mcdc = PathConditions.mcdc prog in
+ let _, type_env, _ = import_dependencies prog_mcdc in
+
+ let _ = type_decls type_env prog_mcdc in
+
+ let destname = !Options.dest_dir ^ "/" ^ basename in
+ let source_file = destname ^ ".mcdc.lus" in (* Could be changed *)
+ let source_out = open_out source_file in
+ let fmt = formatter_of_out_channel source_out in
+ Printers.pp_prog fmt prog_mcdc;
+ Format.fprintf fmt "@.@?";
exit 0
) ;
diff --git a/src/pathConditions.ml b/src/pathConditions.ml
index b97a0608..49882401 100644
--- a/src/pathConditions.ml
+++ b/src/pathConditions.ml
@@ -7,35 +7,45 @@ module IdSet = Set.Make (struct type t = expr * int let compare = compare end)
let inout_vars = ref []
-let print_tautology_var fmt v =
- match (Types.repr v.var_type).Types.tdesc with
- | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id
- | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
- | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id
- | _ -> Format.fprintf fmt "(true)"
+(* This was used to add inout variables in the final signature. May have to be
+ reactivated later *)
+
+(* let print_tautology_var fmt v = *)
+(* match (Types.repr v.var_type).Types.tdesc with *)
+(* | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *)
+(* | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
+(* | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
+(* | _ -> Format.fprintf fmt "(true)" *)
-let print_path arg = match !inout_vars with
- | [] -> Format.printf "%t@." arg
- | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun fmt elem -> print_tautology_var fmt elem)) l
+(* let print_path arg = match !inout_vars with *)
+(* | [] -> Format.printf "%t@." arg *)
+(* | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun fmt elem -> print_tautology_var fmt elem)) l *)
let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ]
-let rec print_pre fmt nb_pre =
- if nb_pre <= 0 then ()
- else (
- Format.fprintf fmt "pre ";
- print_pre fmt (nb_pre-1)
- )
+(* Used when we were printing the expression directly. Now we are constructing
+ them as regular expressions.
+
+ let rec print_pre fmt nb_pre = if nb_pre <= 0 then () else ( Format.fprintf
+ fmt "pre "; print_pre fmt (nb_pre-1) )
+*)
+
+let rec mk_pre n e =
+ if n <= 0 then
+ e
+ else
+ mkexpr e.expr_loc (Expr_pre e)
+
(*
-let combine2 f sub1 sub2 =
- let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in
- let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in
- let common = IdSet.inter elem_e1 elem_e2 in
- let sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
- let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2 in
- (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @
- (List.map (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @
- (List.map (fun v -> (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common)) )
+ let combine2 f sub1 sub2 =
+ let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in
+ let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in
+ let common = IdSet.inter elem_e1 elem_e2 in
+ let sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
+ let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2 in
+ (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @
+ (List.map (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @
+ (List.map (fun v -> (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common)) )
*)
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =
@@ -53,107 +63,209 @@ let combine (f: expr list -> expr ) subs orig : ((expr * int) * expr) list =
v, f (select v active_subs subs orig)
) (IdSet.elements all)
-let rec compute_neg_expr cpt_pre expr =
+
+(* In a previous version, the printer was introducing fake description, ie
+ tautologies, over inout variables to make sure they were not suppresed by
+ some other algorithms *)
+
+(* Takes the variable on which these coverage criteria will apply, as well as
+ the expression and its negated version. Returns the expr and the variable
+ expression, as well as the two new boolean expressions descibing the two
+ associated modes. *)
+let mcdc_var vi_as_expr expr expr_neg_vi =
+ let loc = expr.expr_loc in
+ let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in
+ let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in
+ let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in
+ let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in
+ ((expr,vi_as_expr),[expr1;expr2])
+
+ (* Format.printf "%a@." Printers.pp_expr expr1; *)
+ (* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
+ (* Printers.pp_expr vi_as_expr *)
+ (* Printers.pp_expr expr (\*v*\) *)
+ (* Printers.pp_expr expr_neg_vi); *)
+ (* Format.printf "%a@." Printers.pp_expr expr2; *)
+ (* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
+ (* Printers.pp_expr vi_as_expr *)
+ (* Printers.pp_expr expr (\*v*\) *)
+ (* Printers.pp_expr expr_neg_vi) *)
+
+let rec compute_neg_expr cpt_pre (expr: LustreSpec.expr) =
+ let neg_list l =
+ List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])
+ in
match expr.expr_desc with
| Expr_tuple l ->
- let neg = List.map (compute_neg_expr cpt_pre) l in
- combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
-
+ let vl, neg = neg_list l in
+ vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
+
| Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> (
let list = [i; t; e] in
- let neg = List.map (compute_neg_expr cpt_pre) list in
- combine (fun l ->
+ let vl, neg = neg_list list in
+ vl, combine (fun l ->
match l with
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
| _ -> assert false
) neg list
)
| Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
- gen_mcdc_cond_guard i;
+ let vl = gen_mcdc_cond_guard i in
let list = [i; t; e] in
- let neg = List.map (compute_neg_expr cpt_pre) list in
- combine (fun l ->
+ let vl', neg = neg_list list in
+ vl@vl', combine (fun l ->
match l with
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
| _ -> assert false
) neg list
)
| Expr_arrow (e1, e2) ->
- let e1' = compute_neg_expr cpt_pre e1 in
- let e2' = compute_neg_expr cpt_pre e2 in
- combine (fun l -> match l with
- | [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
- | _ -> assert false
- ) [e1'; e2'] [e1; e2]
- | Expr_pre e ->
- List.map
- (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } ))
- (compute_neg_expr (cpt_pre+1) e)
+ let vl1, e1' = compute_neg_expr cpt_pre e1 in
+ let vl2, e2' = compute_neg_expr cpt_pre e2 in
+ vl1@vl2, combine (fun l -> match l with
+ | [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
+ | _ -> assert false
+ ) [e1'; e2'] [e1; e2]
+
+ | Expr_pre e ->
+ let vl, e' = compute_neg_expr (cpt_pre+1) e in
+ vl, List.map
+ (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
| Expr_appl (op_name, args, r) when List.mem op_name rel_op ->
- [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
+ [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
- | Expr_appl (op_name, args, r) ->
- List.map
- (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
- (compute_neg_expr cpt_pre args)
+ | Expr_appl (op_name, args, r) ->
+ let vl, args' = compute_neg_expr cpt_pre args in
+ vl, List.map
+ (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
+ args'
| Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool ->
- [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
- | _ -> []
-
-and
- gen_mcdc_cond_var v expr =
- report ~level:1 (fun fmt -> Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." v Printers.pp_expr expr);
- let leafs_n_neg_expr = compute_neg_expr 0 expr in
+ [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
+ | _ -> [] (* empty vars *) , []
+and gen_mcdc_cond_var v expr =
+ report ~level:1 (fun fmt ->
+ Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@."
+ v
+ Printers.pp_expr expr);
+ let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
if List.length leafs_n_neg_expr > 1 then (
- List.iter (fun ((vi, nb_pre), expr_neg_vi) ->
- 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);
- 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)
- ) leafs_n_neg_expr
+ List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
+ (mcdc_var (mk_pre nb_pre vi) expr expr_neg_vi)::accu
+ ) vl leafs_n_neg_expr
)
+ else vl
and gen_mcdc_cond_guard expr =
- report ~level:1 (fun fmt -> Format.fprintf fmt".. Generating MC/DC cond for guard %a@." Printers.pp_expr expr);
- let leafs_n_neg_expr = compute_neg_expr 0 expr in
+ report ~level:1 (fun fmt ->
+ Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
+ Printers.pp_expr expr);
+ let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
if List.length leafs_n_neg_expr > 1 then (
- List.iter (fun ((vi, nb_pre), expr_neg_vi) ->
- 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);
- 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)
-
- ) leafs_n_neg_expr
- )
+ List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
+ (mcdc_var (mk_pre nb_pre vi) expr expr_neg_vi)::accu
+ ) vl leafs_n_neg_expr)
+ else
+ vl
let rec mcdc_expr cpt_pre expr =
match expr.expr_desc with
- | Expr_tuple l -> List.iter (mcdc_expr cpt_pre) l
- | Expr_ite (i,t,e) -> (gen_mcdc_cond_guard i; List.iter (mcdc_expr cpt_pre) [t; e])
- | Expr_arrow (e1, e2) -> List.iter (mcdc_expr cpt_pre) [e1; e2]
- | Expr_pre e -> mcdc_expr (cpt_pre+1) e
- | Expr_appl (_, args, _) -> mcdc_expr cpt_pre args
- | _ -> ()
+ | Expr_tuple l ->
+ let vl =
+ List.fold_right (fun e accu_v ->
+ let vl = mcdc_expr cpt_pre e in
+ (vl@accu_v))
+ l
+ []
+ in
+ vl
+ | Expr_ite (i,t,e) ->
+ let vl_i = gen_mcdc_cond_guard i in
+ let vl_t = mcdc_expr cpt_pre t in
+ let vl_e = mcdc_expr cpt_pre e in
+ vl_i@vl_t@vl_e
+ | Expr_arrow (e1, e2) ->
+ let vl1 = mcdc_expr cpt_pre e1 in
+ let vl2 = mcdc_expr cpt_pre e2 in
+ vl1@vl2
+ | Expr_pre e ->
+ let vl = mcdc_expr (cpt_pre+1) e in
+ vl
+ | Expr_appl (f, args, r) ->
+ let vl = mcdc_expr cpt_pre args in
+ vl
+ | _ -> []
let mcdc_var_def v expr =
match (Types.repr expr.expr_type).Types.tdesc with
- | Types.Tbool -> gen_mcdc_cond_var v expr
- | _ -> mcdc_expr 0 expr
+ | Types.Tbool ->
+ let vl = gen_mcdc_cond_var v expr in
+ vl
+ | _ -> let vl = mcdc_expr 0 expr in
+ vl
let mcdc_node_eq eq =
- match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
- | [lhs], Types.Tbool, _ -> gen_mcdc_cond_var lhs eq.eq_rhs
- | _::_, Types.Ttuple tl, Expr_tuple rhs -> List.iter2 mcdc_var_def eq.eq_lhs rhs
- | _ -> mcdc_expr 0 eq.eq_rhs
+ let vl =
+ match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
+ | [lhs], Types.Tbool, _ -> gen_mcdc_cond_var lhs eq.eq_rhs
+ | _::_, Types.Ttuple tl, Expr_tuple rhs ->
+ (* We iterate trough pairs, but accumulate variables aside. The resulting
+ expression shall remain a tuple defintion *)
+ let vl = List.fold_right2 (fun lhs rhs accu ->
+ let v = mcdc_var_def lhs rhs in
+ (* we don't care about the expression it. We focus on the coverage
+ expressions in v *)
+ v@accu
+ ) eq.eq_lhs rhs []
+ in
+ vl
+ | _ -> mcdc_expr 0 eq.eq_rhs
+ in
+ vl
let mcdc_node_stmt stmt =
match stmt with
- | Eq eq -> mcdc_node_eq eq
+ | Eq eq -> let vl = mcdc_node_eq eq in vl
| Aut aut -> assert false
let mcdc_top_decl td =
match td.top_decl_desc with
- | Node nd -> List.iter mcdc_node_stmt nd.node_stmts
- | _ -> ()
+ | Node nd ->
+ let new_coverage_exprs =
+ List.fold_right (
+ fun s accu_v ->
+ let vl' = mcdc_node_stmt s in
+ vl'@accu_v
+ ) nd.node_stmts []
+ in
+ (* We add coverage vars as boolean internal flows. TODO *)
+ let fresh_cov_defs = List.flatten (List.map snd new_coverage_exprs) in
+ let nb_total = List.length fresh_cov_defs in
+ let fresh_cov_vars = List.mapi (fun i cov_expr ->
+ let loc = cov_expr.expr_loc in
+ Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
+ let cov_id = Format.flush_str_formatter () in
+ let cov_var = mkvar_decl loc
+ (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None) in
+ let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
+ cov_var, cov_def
+ ) fresh_cov_defs
+ in
+ let fresh_vars, fresh_eqs = List.split fresh_cov_vars in
+ let fresh_annots =
+ List.map
+ (fun v -> {annots = [["PROPERTY"], expr_to_eexpr (expr_of_vdecl v)]; annot_loc = td.top_decl_loc})
+ fresh_vars in
+ Format.printf "We have %i coverage criteria for node %s@." nb_total nd.node_id;
+ (* And add them as annotations --%PROPERTY: var TODO *)
+ {td with top_decl_desc = Node {nd with
+ node_locals = nd.node_locals@fresh_vars;
+ node_stmts = nd.node_stmts@fresh_eqs;
+ node_annot = nd.node_annot@fresh_annots
+ }}
+ | _ -> td
let mcdc prog =
@@ -170,7 +282,7 @@ let mcdc prog =
match top.top_decl_desc with
| Node nd -> nd.node_inputs @ nd.node_outputs
| _ -> assert false);
- List.iter mcdc_top_decl prog
+ List.map mcdc_top_decl prog
(* Local Variables: *)
(* compile-command:"make -C .." *)
--
GitLab