CristalCaveGem » LustreC

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

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

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

     let vl, neg = neg_list l in

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

    let vl, neg = neg_list list in

    vl, combine (fun l ->

    let vl = gen_mcdc_cond_guard i in

    let vl', neg = neg_list list in

    vl@vl', combine (fun l ->

     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, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]

  | 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, 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

    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

  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

    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

  | 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

  | _ -> []

  | Types.Tbool ->

     let vl = gen_mcdc_cond_var v expr in

     vl

  | _ -> let vl = mcdc_expr 0 expr in

	 vl

  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

  | Eq eq -> let vl = mcdc_node_eq eq in vl

  | 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

  List.map mcdc_top_decl prog