CristalCaveGem » LustreC

open Lustre_types 

open Log

open Format

module IdSet = Set.Make (struct type t = expr * int let compare = compare end)

let inout_vars = ref [] 

   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)" *)

(*   | [] -> 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 = ["="; "!="; "<"; "<="; ">" ; ">=" ]

   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 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) =

match active, modified, orig with

| true::active_tl, e::modified_tl, _::orig_tl -> (List.assoc v e)::(select v active_tl modified_tl orig_tl)

| false::active_tl, _::modified_tl, e::orig_tl -> e::(select v active_tl modified_tl orig_tl)

| [], [], [] -> []

| _ -> assert false

let combine (f: expr list -> expr ) subs orig : ((expr * int) * expr) list  = 

  let elems = List.map (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in

  let all = List.fold_right IdSet.union elems IdSet.empty in

  List.map (fun v ->

    let active_subs = List.map (IdSet.mem v) elems in

    v, f (select v active_subs subs orig)

  ) (IdSet.elements all)

   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 nb_elems expr expr_neg_vi =

  let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in

    if nb_elems > 1 then 

      let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in

      let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in

      let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in

      expr1, expr2

    else

      vi_as_expr, not_vi_as_expr

  in

                                                     true while expr2

                                                     corresponds to atom

                                                     false *)

  (* 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) *)

    List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])

  in

  | Expr_tuple l -> 

     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l

    vl, combine (fun l ->

            | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}

            | _ -> assert false

          ) neg list

    vl@vl', combine (fun l ->

                | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}

                | _ -> assert false

              ) neg list

  | Expr_arrow (e1, e2) -> 

     let vl2, e2' = compute_neg_expr cpt_pre e2 in

     vl1@vl2, combine (fun l -> match l with

                                | _ -> assert false

                ) [e1'; e2'] [e1; e2]

  | Expr_pre e ->

     let vl, e' = compute_neg_expr (cpt_pre+1) e in

     vl, List.map

  | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> 

     let vl, args' = compute_neg_expr cpt_pre args in

     vl, List.map 

           args'

  | _ -> [] (* empty vars *) , [] 

and gen_mcdc_cond_var v expr =

  report ~level:1 (fun fmt ->

        v

        Printers.pp_expr expr);

  if len >= 1 then (

      ) vl leafs_n_neg_expr

    vl

and gen_mcdc_cond_guard expr =

        Printers.pp_expr expr);

  if len >= 1 then (

      ) vl leafs_n_neg_expr)

    vl

let rec mcdc_expr cpt_pre expr = 

  match expr.expr_desc with

     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 = 

     vl

    let vl = mcdc_expr 0 expr in

    vl

	  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

  match stmt with

  match td.top_decl_desc with

     let new_coverage_exprs =

       List.fold_right (

	   vl'@accu_v

     let fresh_cov_defs = List.flatten (List.map (fun ((_, atom), expr_l) -> List.map (fun (atom_valid, case) -> atom, atom_valid, case) expr_l) new_coverage_exprs) in

				     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, None) in

				     let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in

				     cov_var, cov_def, atom, atom_valid

				    ) fresh_cov_defs

       List.fold_right

	 ([], [])

     in

     let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for

			   kind2, and regular ones to keep track of the nature

			   of the annotations. *)

	  let e = expr_of_vdecl v in

	  let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in

	  {annots =  [["PROPERTY"], neg_ee; (* Using negated property to force

                                               model-checker to produce a

                                               suitable covering trace *)

		      let valid_e = let open Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in

		      ["coverage";"mcdc";v.var_id], expr_to_eexpr (Corelang.expr_of_expr_list loc [e; atom; valid_e])

	   annot_loc = v.var_loc})

	 fresh_cov_vars

     Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id;

     {td with top_decl_desc = Node {nd with

				     node_stmts = nd.node_stmts@fresh_eqs;

				     node_annot = nd.node_annot@fresh_annots

				   }}

let mcdc prog =

  (* If main node is provided add silly constraints to show in/out variables in the path condition *)

  if !Options.main_node <> "" then (

    inout_vars := 

      let top = List.find 

	(fun td -> 

	  match td.top_decl_desc with 

	  | Node nd when nd.node_id = !Options.main_node -> true

	  | _ -> false) 

	prog 

      in

      match top.top_decl_desc with

      | Node nd -> nd.node_inputs @ nd.node_outputs

      | _ -> assert false);

(* compile-command:"make -C .." *)

(* End: *)