diff options
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 110 | ||||
| -rw-r--r-- | abstract/enum_domain.ml | 26 | ||||
| -rw-r--r-- | abstract/formula.ml | 2 | ||||
| -rw-r--r-- | main.ml | 26 | ||||
| -rw-r--r-- | tests/source/half.scade | 2 | ||||
| -rw-r--r-- | tests/source/updown2.scade | 2 |
6 files changed, 107 insertions, 61 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index c47fdc7..1adc430 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -62,7 +62,7 @@ end = struct *) let top e = (ED.top e.ve.evars, ND.top e.ve.nvars) let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars) - let is_bot (e, n) = ND.is_bot n + let is_bot (e, n) = ED.is_bot e || ND.is_bot n let print_v fmt (enum, num) = if is_bot (enum, num) then @@ -75,32 +75,34 @@ end = struct widen : abs_v -> abs_v -> abs_v meet : abs_v -> abs_v -> abs_v *) - let join (e1, n1) (e2, n2) = - if is_bot (e1, n1) then (e2, n2) - else if is_bot (e2, n2) then (e1, n1) - else (ED.join e1 e2, ND.join n1 n2) + let join a b = + if is_bot a then b + else if is_bot b then a + else (ED.join (fst a) (fst b), ND.join (snd a) (snd b)) - let widen (e1, n1) (e2, n2) = - if is_bot (e1, n1) then (e2, n2) - else if is_bot (e2, n2) then (e1, n1) - else (ED.join e1 e2, ND.widen n1 n2) + let widen a b = + if is_bot a then b + else if is_bot b then a + else (ED.join (fst a) (fst b), ND.widen (snd a) (snd b)) let meet (e1, n1) (e2, n2) = if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1 else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2 else try (ED.meet e1 e2 , ND.meet n1 n2) - with Bot -> e1, ND.vbottom n1 + with Bot -> ED.vtop e1, ND.vbottom n1 (* eq_v : abs_v -> abs_v -> bool subset_v : abs_v -> abs_v -> bool *) - let eq_v (a, b) (c, d) = (ND.is_bot b && ND.is_bot d) || (ED.eq a c && ND.eq b d) + let eq_v (a, b) (c, d) = + (is_bot (a, b) && is_bot (c, d)) + || (ED.eq a c && ND.eq b d) let subset_v (a, b) (c, d) = - ND.is_bot b || - (not (ND.is_bot d) && ED.subset a c && ND.subset b d) + (is_bot (a, b)) || + (not (is_bot (c, d)) && ED.subset a c && ND.subset b d) (* apply_cl : abs_v -> conslist -> abs_v @@ -109,12 +111,9 @@ end = struct try begin match r with | CLTrue -> - let enum = - fix ED.eq (fun v -> ED.apply_cl v ec) enum - in - (enum, ND.apply_cl num nc) + (ED.apply_cl enum ec, ND.apply_cl num nc) | CLFalse -> - (enum, ND.vbottom num) + (ED.vtop enum, ND.vbottom num) | CLAnd(a, b) -> let enum, num = apply_cl (enum, num) (ec, nc, a) in let enum, num = apply_cl (enum, num) ([], nc, b) in @@ -289,6 +288,23 @@ end = struct meet v tgt (* + print_locs : env -> unit + *) + + let print_locs e = + Hashtbl.iter + (fun id loc -> + Format.printf "@."; + Format.printf "q%d: @[<v 2>[ %a ]@]@." id + (print_list Formula_printer.print_expr " ∧ ") loc.def; + (*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*) + Format.printf " %a@." print_v loc.v; + Format.printf " -> @[<hov>[%a]@]@." + (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t; + ) + e.loc + + (* chaotic_iter : env -> unit Fills the values of loc[*].v, and updates out_t and in_t @@ -309,6 +325,8 @@ end = struct loc.v <- bottom e) e.loc; + print_locs e; + (* Iterate *) let it_counter = ref 0 in while !delta <> [] do @@ -323,7 +341,10 @@ end = struct (*Format.printf "I: %a@." print_v i;*) let i' = set_target_case e i loc.def_cl in (*Format.printf "I': %a@." print_v i';*) - let j = join start (apply_cl (apply_cl (pass_cycle e.ve i') loc.def_cl) loc.cl) in + let j = join start + (apply_cl + (apply_cl (pass_cycle e.ve i') loc.def_cl) + loc.cl) in (*Format.printf "J: %a@." print_v j;*) j in @@ -342,28 +363,30 @@ end = struct in let y = iter 0 start in let z = fix eq_v f y in - (*Format.printf "Fixpoint: %a@." print_v z;*) + let u = pass_cycle e.ve z in + + if e.opt.verbose_ci then + Format.printf "Fixpoint: %a@. mem fp: %a@." print_v z print_v u; loc.v <- z; Hashtbl.iter (fun t loc2 -> - let u = pass_cycle e.ve z in let v = apply_cl u loc2.def_cl in let w = apply_cl v loc2.cl in (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*) - let r_enum, r_num = w in - if not (is_bot (r_enum, r_num)) then begin - (*Format.printf "%d -> %d with:@. %a@." s t print_v (r_enum, r_num);*) + if not (is_bot w) then begin + if e.opt.verbose_ci then + Format.printf "%d -> %d with:@. %a@." s t print_v w; if not (List.mem s loc2.in_t) then loc2.in_t <- s::loc2.in_t; if not (List.mem t loc.out_t) then loc.out_t <- t::loc.out_t; - if not (subset_v (r_enum, r_num) loc2.v) then begin + if not (subset_v w loc2.v) then begin if loc2.in_c < e.opt.widen_delay then - loc2.v <- join (r_enum, r_num) loc2.v + loc2.v <- join w loc2.v else - loc2.v <- widen (r_enum, r_num) loc2.v; + loc2.v <- widen w loc2.v; loc2.in_c <- loc2.in_c + 1; if not (List.mem t !delta) then delta := t::!delta @@ -383,21 +406,11 @@ end = struct useless := i::!useless end) e.loc; - List.iter (Hashtbl.remove e.loc) !useless + List.iter (Hashtbl.remove e.loc) !useless; + + print_locs e - let print_locs e = - Hashtbl.iter - (fun id loc -> - Format.printf "@."; - Format.printf "q%d: @[<v 2>[ %a ]@]@." id - (print_list Formula_printer.print_expr " ∧ ") loc.def; - (*Format.printf " F: (%a)@." Formula_printer.print_expr loc.f;*) - Format.printf " %a@." print_v loc.v; - Format.printf " -> @[<hov>[%a]@]@." - (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t; - ) - e.loc let do_prog opt rp = let e = init_env opt rp in @@ -406,7 +419,6 @@ end = struct Format.printf "@.--------------@.Refinement #%d@." n; chaotic_iter e; - print_locs e; let qc = ref None in @@ -426,8 +438,10 @@ end = struct then BNot cond else cond in - loc.def <- tr::loc.def; - loc.def_cl <- conslist_of_f (f_and_list loc.def); + if not (List.mem tr loc.def) then begin + loc.def <- tr::loc.def; + loc.def_cl <- conslist_of_f (f_and_list loc.def); + end; loc.f <- simplify_k [tr] loc.f; loc.f <- simplify_k (get_root_true loc.f) loc.f; loc.cl <- conslist_of_f loc.f; @@ -445,17 +459,19 @@ end = struct (fun c -> let split_e_case_fold_aux cases c = match c with - | BEnumCons(_, x, EItem _) -> + | BEnumCons(op, x, EItem _) -> + let op = match op with | E_EQ -> (=) | E_NE -> (<>) in (List.map (fun v -> BEnumCons(E_EQ, x, EItem v)) - (List.assoc x e.ve.evars))@cases + (List.filter (op x) (List.assoc x e.ve.evars))) + @cases | _ -> c::cases in let cases_t = List.fold_left split_e_case_fold_aux [] - (split_cases [c]) in + [c] in let cases_f = List.fold_left split_e_case_fold_aux [] - (split_cases [BNot c]) in + [eliminate_not_negate c] in let cases = cases_t @ cases_f in if List.length diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index 4f6aacd..77d7e3f 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -119,11 +119,14 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct if cc op s t then [x] else [] let apply_cl x l = - List.fold_left - (fun k c -> match apply_cons k c with - | [] -> raise Bot - | p::q -> List.fold_left join p q ) - x l + let f x = + List.fold_left + (fun k c -> match apply_cons k c with + | [] -> raise Bot + | p::q -> List.fold_left join p q ) + x l + in + fix eq f x let assign x idl = let v = List.fold_left @@ -242,11 +245,14 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct [] v1 let apply_cl x l = - List.fold_left - (fun k c -> match apply_cons k c with - | [] -> raise Bot - | p::q -> List.fold_left join p q ) - x l + let f x = + List.fold_left + (fun k c -> match apply_cons k c with + | [] -> raise Bot + | p::q -> List.fold_left join p q ) + x l + in + fix eq f x let assign x idl = let v = List.fold_left diff --git a/abstract/formula.ml b/abstract/formula.ml index 5cbe0c9..a124a84 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -277,6 +277,8 @@ let rec split_cases c = match c with | BOr(a, b) -> true, a::(BAnd(BNot a, b))::l + | BTernary(c, a, b) -> + true, (BAnd(c, a))::(BAnd(BNot c, b))::l | x -> u, x::l) (false, []) c in @@ -23,6 +23,10 @@ module AI_S_Itv_DP = Abs_interp_dynpart.I (Enum_domain.MultiValuation)(ItvND) module AI_S_Rel_DP = Abs_interp_dynpart.I (Enum_domain.MultiValuation)(Apron_domain.ND) +module AI_EDD_Itv_DP = Abs_interp_dynpart.I + (Enum_domain_edd.EDD)(ItvND) +module AI_EDD_Rel_DP = Abs_interp_dynpart.I + (Enum_domain_edd.EDD)(Apron_domain.ND) (* command line options *) let times = ref false @@ -36,6 +40,8 @@ let ai_itv_edd = ref false let ai_rel_edd = ref false let ai_s_itv_dp = ref false let ai_s_rel_dp = ref false +let ai_edd_itv_dp = ref false +let ai_edd_rel_dp = ref false let ai_root = ref "test" let ai_widen_delay = ref 5 let ai_no_time_scopes = ref "all" @@ -50,28 +56,41 @@ let usage = "usage: analyzer [options] file.scade" let options = [ "--exec-times", Arg.Set times, "Show time spent in each function of the analyzer, for some functions"; + "--dump", Arg.Set dump, "Dump program source."; "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming."; + "--vtest", Arg.Set vtest, "Verbose testing (direct interpret)."; "--test", Arg.Set test, "Simple testing (direct interpret)."; + "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals."; "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron."; + "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain."; "--ai-rel-edd", Arg.Set ai_rel_edd, "Do abstract analysis using Apron and EDD disjunction domain."; + "--ai-s-itv-dp", Arg.Set ai_s_itv_dp, "Do abstract analysis using dynamic partitionning method, "^ "with intervals and valuation domain for enums."; "--ai-s-rel-dp", Arg.Set ai_s_rel_dp, "Do abstract analysis using dynamic partitionning method, "^ "with Apron and valuation domain for enums."; + "--ai-edd-itv-dp", Arg.Set ai_edd_itv_dp, + "Do abstract analysis using dynamic partitionning method, "^ + "with intervals and EDD domain for enums."; + "--ai-edd-rel-dp", Arg.Set ai_edd_rel_dp, + "Do abstract analysis using dynamic partitionning method, "^ + "with Apron and EDD domain for enums."; + "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)"; "--ai-vvci", Arg.Set ai_vvci, "Very verbose chaotic iterations (show everything all the time)"; - "--wd", Arg.Set_int ai_widen_delay, + "--ai-wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3)."; + "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test)."; "--no-time", Arg.Set_string ai_no_time_scopes, @@ -132,7 +151,8 @@ let () = if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd - || !ai_s_itv_dp || !ai_s_rel_dp then + || !ai_s_itv_dp || !ai_s_rel_dp + || !ai_edd_itv_dp || !ai_edd_rel_dp then begin let comma_split = Str.split (Str.regexp ",") in let select_f x = @@ -168,6 +188,8 @@ let () = if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp; if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp; + if !ai_edd_itv_dp then AI_EDD_Itv_DP.do_prog opt rp; + if !ai_edd_rel_dp then AI_EDD_Rel_DP.do_prog opt rp; end; if !vtest then do_test_interpret prog true diff --git a/tests/source/half.scade b/tests/source/half.scade index 541e81c..7e0df60 100644 --- a/tests/source/half.scade +++ b/tests/source/half.scade @@ -25,5 +25,5 @@ let c = a - b; guarantee c_bounded: c >= 0 and c <= 1; - guarantee link_c_half: (half and c = 1) or ((not half) and c = 0); + guarantee link_c_half: if half then (c = 1) else (c = 0); tel diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade index 29c34ff..72d5bed 100644 --- a/tests/source/updown2.scade +++ b/tests/source/updown2.scade @@ -30,7 +30,7 @@ let guarantee y_bounded: y >= -bound and y <= bound; z = x + y; - guarantee x_y_opp: z = 0 and (true -> pre (z = 0)); + guarantee x_y_opp: z = 0; tel node test(i: int) returns(a, b, c: int; exit: bool) |