Commit 3d79de8f authored by Mickaël Delahaye's avatar Mickaël Delahaye
Browse files

Add GICC, improve GACC & add some doc for GACC

parent 608f5f0d
......@@ -19,7 +19,7 @@ Once Frama-C is installed, compile and install GenLabels:
make
make install
The former command may need to be run as root (or sudo) depending on your
The second command may need to be run as root (or sudo) depending on your
Frama-C installation.
Usage
......@@ -30,7 +30,7 @@ Usage
where CRITERIA is a comma-separated list of criteria. It outputs a new
annotated file named `file_labels.c`, with labels for each selected criterion.
Implemented criteria are CC, MCC, WM, IDP, F and D.
Implemented criteria are CC, MCC, n-CC, WM, IDP, FC, DC, GACC and GICC:
### CC (Conditition Coverage)
......@@ -157,13 +157,48 @@ becomes:
...
}
## GACC (General Active Clause Coverage) [Ammann & Offut, p109]
Weak MCDC, requires two labels by atomic condition in every decision.
The following branch:
if (a && || c) ...
becomes:
pc_label(a && ((! (b || c) && c) || ((b || c) && ! c)),1,"GACC");
pc_label(! a && ((! (b || c) && c) || ((b || c) && ! c)),2,"GACC");
pc_label(b && ((! (a || c) && c) || ((a || c) && ! c)),3,"GACC");
pc_label(! b && ((! (a || c) && c) || ((a || c) && ! c)),4,"GACC");
pc_label(c && ! (a && b),5,"GACC");
pc_label(! c && ! (a && b),6,"GACC");
if (a && || c) ...
Each label includes two parts:
- the atomic condition or its negation;
- the independence condition (inequality of positive and negative
Shannon's cofactors w.r.t. to the atom).
Note that the Boolean inequality of the independence condition `F⁺ ≠ F⁻` is
encoded as `(F⁺&&!F⁻) || (!F⁺&&F⁻)` to allow for more simplifications with
`-lannot-simplify`.
Also supports `-lannot-allbool` in addition to `-lannot-simplify`.
## GICC (General Inactive Clause Coverage) [Ammann & Offut, p112]
Requires four labels by atomic condition.
Authors
-------
Omar Chebaro
Mickaël Delahaye
Nikolai Kosmatov
Sébastien Bardin
- Omar Chebaro
- Mickaël Delahaye
Also many thanks to the rest of LTest's team:
- Nikolai Kosmatov
- Sébastien Bardin
License
-------
......
......@@ -109,10 +109,6 @@ let mk_compute_extras apply name id collect ast =
let register_annotator ann =
Options.debug1 "register %s annotator" ann.name;
Hashtbl.replace annotators ann.name ann
(* (* TO LATE *)
let all = Hashtbl.fold (fun k _v acc -> k :: acc) annotators [] in
Options.Annotators.set_possible_values all
*)
module Register (A : ANNOTATOR) = struct
let self = { name = A.name; help = A.help; apply = mk_apply A.apply A.name }
......
......@@ -37,6 +37,20 @@ module Exp = struct
let binop ?(loc=unk_loc) op left right =
Cil.mkBinOp ~loc op left right
let implies ?(loc=unk_loc) l r =
let n_l = lnot ~loc l in
Cil.mkBinOp ~loc LOr n_l r
let iff ?(loc=unk_loc) l r =
let l_imp_r = implies ~loc l r in
let r_imp_l = implies ~loc r l in
Cil.mkBinOp ~loc LAnd l_imp_r r_imp_l
let niff ?(loc=unk_loc) l r =
let nl_and_r = Cil.mkBinOp ~loc LAnd (lnot ~loc l) r in
let l_and_nr = Cil.mkBinOp ~loc LAnd l (lnot ~loc r) in
Cil.mkBinOp ~loc LOr nl_and_r l_and_nr
let rec replace ~whole ~part ~(repl: exp) : exp=
if part == whole then repl
else
......
......@@ -27,6 +27,15 @@ module Exp : sig
(** Binary operation *)
val binop : ?loc:location -> binop -> exp -> exp -> exp
(** Implies *)
val implies : ?loc:location -> exp -> exp -> exp
(** Iff *)
val iff : ?loc:location -> exp -> exp -> exp
(** Xor, boolean disequality *)
val niff : ?loc:location -> exp -> exp -> exp
(** Replace some subexpression by another (== equality) *)
val replace : whole:exp -> part:exp -> repl:exp -> exp
......
......@@ -73,22 +73,45 @@ let gen_labels_gacc_for mk_label whole part =
let w0 = Exp.replace whole part (Exp.one ()) in
let w1 = Exp.replace whole part (Exp.zero ()) in
(* rather than to test w0 != w1, do (w0 || w1) && !(w0 && w1) *)
let w0_or_w1 = Exp.binop LOr w0 w1 in
let w0_nand_w1 = neg (Exp.binop LAnd w0 w1) in
let indep = Exp.binop LAnd w0_or_w1 w0_nand_w1 in
(* rather than to test w0 != w1, do (w0 && !w1) || (!w0 && w1) *)
let indep = Exp.niff w0 w1 in
let a_indep = Exp.binop LAnd (pos part) (Exp.copy indep) in
let na_indep = Exp.binop LAnd (neg part) (Exp.copy indep) in
Stmt.block [mk_label a_indep loc; mk_label na_indep loc];;
Stmt.block (List.map (fun e -> mk_label e loc) [a_indep; na_indep]);;
(** Generate GACC labels for the given Boolean formula *)
let gen_labels_gacc mk_label bexpr =
let atoms = atomic_conditions bexpr in
Stmt.block (List.map (gen_labels_gacc_for mk_label bexpr) atoms);;
(** Generate GICC labels for the given Boolean formula *)
let gen_labels_gicc_for mk_label whole part =
let loc = whole.eloc in
(* Compute negative and positive Shannon's factors wrt to part *)
let factor0 = Exp.replace whole part (Exp.one ()) in
let factor1 = Exp.replace whole part (Exp.one ()) in
(* Check the inactivity of part *)
let inactive = Exp.iff factor0 factor1 in
let true_inactive = Exp.binop LAnd (pos part) inactive in
let false_inactive = Exp.binop LAnd (neg part) inactive in
let true_inactive_true = Exp.binop LAnd true_inactive (pos whole) in
let true_inactive_false = Exp.binop LAnd true_inactive (neg whole) in
let false_inactive_true = Exp.binop LAnd false_inactive (pos whole) in
let false_inactive_false = Exp.binop LAnd false_inactive (neg whole) in
Stmt.block (List.map (fun e -> mk_label e loc) [
true_inactive_true;
true_inactive_false;
false_inactive_true;
false_inactive_false;
])
(** Generate GICC labels for the given Boolean formula *)
let gen_labels_gicc mk_label bexpr =
let atoms = atomic_conditions bexpr in
Stmt.block (List.map (gen_labels_gicc_for mk_label bexpr) atoms)
(**
* Frama-C in-place visitor that injects labels at each condition/boolean
......@@ -202,3 +225,15 @@ module GACC = Annotators.Register (struct
let apply mk_label file =
apply (gen_labels_gacc mk_label) (Options.AllBoolExps.get ()) file
end)
(**
General Inactive Clause Coverage annotator
*)
module GICC = Annotators.Register (struct
let name = "GICC"
let help = "General Inactive Clause Coverage"
let apply mk_label file =
apply (gen_labels_gicc mk_label) (Options.AllBoolExps.get ()) file
end)
......@@ -33,14 +33,12 @@ let rec string_list l =
| a :: b :: [] -> a^" and "^b
| head :: tail -> head^", "^string_list tail
let annotators = ["MCC"; "CC"; "FC"; "DC"; "WM"; "IDP"]
module Annotators = StringSet (struct
let option_name = "-lannot"
let arg_name = "criteria"
let help = "generate labels for each criterion (comma-separated \
list of criteria, among "^string_list annotators^")"
list of criteria, see -lannot-list)"
end)
let () = Annotators.set_possible_values annotators
let () = Annotators.add_aliases ["-lannotate"]
module Output = EmptyString (struct
......@@ -114,9 +112,9 @@ let () = Parameter_customize.set_group help
let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.do_not_projectify ()
let () = Parameter_customize.do_not_save ()
module AnnotatorsHelp = False (struct
let option_name = "-lannot-criteria-help"
let help = "show criteria help"
module ListAnnotators = False (struct
let option_name = "-lannot-list"
let help = "show list of criteria"
end)
module Simplify = False (struct
......
......@@ -101,7 +101,7 @@ let run () =
| e -> Options.fatal "unexpected exception: %s" (Printexc.to_string e)
let run () =
if Options.AnnotatorsHelp.get () then
if Options.ListAnnotators.get () then
begin
Annotators.print_help Format.std_formatter;
exit 0;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment