diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 8 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 500 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 9 | ||||
| -rw-r--r-- | libs/util.ml | 35 | ||||
| -rw-r--r-- | main.ml | 9 |
6 files changed, 536 insertions, 26 deletions
@@ -24,6 +24,7 @@ SRC= main.ml \ abstract/transform.ml \ \ abstract/abs_interp.ml \ + abstract/abs_interp_edd.ml \ interpret/interpret.ml \ all: $(BIN) diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index f526095..bed2f2c 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -233,7 +233,7 @@ end = struct *) let init_state opt rp = Format.printf "Vars: @[<hov>%a@]@.@." - (Ast_printer.print_list Ast_printer.print_typed_var ", ") + (print_list Ast_printer.print_typed_var ", ") rp.all_vars; let enum_vars = List.fold_left @@ -390,7 +390,7 @@ end = struct incr n_ch_iter; Format.printf "Chaotic iteration %d: @[<hov>[%a]@]@." !n_ch_iter - (Ast_printer.print_list Formula_printer.print_id ", ") case; + (print_list Formula_printer.print_id ", ") case; let start = try Hashtbl.find st.env case with Not_found -> assert false in let start_dd = dd_singleton st.d_vars start in @@ -465,11 +465,11 @@ end = struct Format.printf "%a" ND.print_itv (ND.project num id) | TEnum _ -> Format.printf "@[<hov>{ %a }@]" - (Ast_printer.print_list Formula_printer.print_id ", ") + (print_list Formula_printer.print_id ", ") (ED.project enum id) end; Format.printf " when @[<hov>[%a]@]@ " - (Ast_printer.print_list Formula_printer.print_id ", ") case) + (print_list Formula_printer.print_id ", ") case) final.data; Format.printf "@]@ " end) diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml new file mode 100644 index 0000000..a9ecc07 --- /dev/null +++ b/abstract/abs_interp_edd.ml @@ -0,0 +1,500 @@ +open Ast +open Ast_util +open Formula +open Typing + +open Util +open Num_domain +open Abs_interp + +module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig + + val do_prog : cmdline_opt -> rooted_prog -> unit + + val test : unit -> unit + +end = struct + + + (* ********************** + EDD Domain + ********************** *) + + type item = string + + type evar = id * item list + type nvar = id * bool + + type varenv = { + evars : evar list; + nvars : nvar list; + ev_order : (id, int) Hashtbl.t; + } + + type edd = + | DBot + | DVal of int + | DChoice of id * (item * edd) list + + type edd_v = { + ve : varenv; + root : edd; + leaves : (int, ND.t) Hashtbl.t; + (* add here eventual annotations *) + } + + + + (* + edd_print : Format.formatter -> edd_v -> unit + *) + let edd_print fmt v = + let ids = Hashtbl.create 12 in + let n = ref 0 in + let rec mkid = function + | DChoice(_, l) as x -> + if not (Hashtbl.mem ids x) then begin + incr n; Hashtbl.add ids x !n; + List.iter (fun (_, x) -> mkid x) l + end + | _ -> () + in mkid v.root; + let print_n fmt = function + | DBot -> Format.fprintf fmt "⊥"; + | DVal i -> Format.fprintf fmt "v%d" i; + | DChoice _ as x -> Format.fprintf fmt "n%d" (Hashtbl.find ids x) + in + Format.fprintf fmt "Root: %a@." print_n v.root; + Hashtbl.iter + (fun x id -> match x with + | DChoice (var, l) -> + let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in + Format.fprintf fmt "n%d: %s ? @[<hov>%a@]@." id var + (print_list p ", ") l + | _ -> assert false) + ids; + Hashtbl.iter + (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v) + v.leaves + + + + (* + edd_bot : varenv -> edd_v + *) + let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 } + + (* + edd_top : evar list -> nvar list -> edd_v + *) + let edd_top ve = + let leaves = Hashtbl.create 1 in + Hashtbl.add leaves 0 (ND.top ve.nvars); + { ve; root = DVal 0; leaves } + + (* + edd_of_cons : varenv -> enum_cons -> edd_v + *) + let edd_of_cons ve (op, vid, r) = + let op = match op with | E_EQ -> (=) | E_NE -> (<>) in + + let leaves = Hashtbl.create 1 in + Hashtbl.add leaves 0 (ND.top ve.nvars); + + let root = match r with + | EItem x -> + DChoice(vid, + List.map (fun v -> if op v x then v, DVal 0 else v, DBot) + (List.assoc vid ve.evars)) + | EIdent vid2 -> + let a, b = + if Hashtbl.find ve.ev_order vid < Hashtbl.find ve.ev_order vid2 + then vid, vid2 + else vid2, vid + in + let nb x = + DChoice(b, + List.map (fun v -> if op v x then v, DVal 0 else v, DBot) + (List.assoc b ve.evars)) + in + DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars)) + in + { ve; root; leaves } + + (* + edd_join : edd_v -> edd_v -> edd_v + *) + let edd_join a b = + let ve = a.ve in + + let leaves = Hashtbl.copy a.leaves in + let n = ref 0 in + Hashtbl.iter (fun i _ -> if i > !n then n := i) leaves; + + let get_leaf x = + let id = ref None in + Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves; + begin match !id with + | Some i -> DVal i + | None -> + incr n; + Hashtbl.add leaves !n x; + DVal (!n) + end + in + + let memo_bcopy = Hashtbl.create 12 in + let rec bcopy nb = + try Hashtbl.find memo_bcopy nb + with Not_found -> let r = + match nb with + | DBot -> DBot + | DVal i -> get_leaf (Hashtbl.find b.leaves i) + | DChoice (v, x) -> + DChoice(v, List.map (fun (c, n) -> c, bcopy n) x) + in Hashtbl.add memo_bcopy nb r; r + in + + let memo = Hashtbl.create 12 in + let rec f (na, nb) = + try Hashtbl.find memo (na, nb) + with Not_found -> let r = + let dq v l = + let _, x0 = List.hd l in + if List.exists (fun (_, x) -> x <> x0) l + then DChoice(v, l) + else x0 + in + match na, nb with + | DBot, x -> bcopy x + | x, DBot -> x + + | DChoice(va, la), DChoice(vb, lb) when va = vb -> + let kl = List.map2 + (fun (ta, ba) (tb, bb) -> assert (ta = tb); + ta, f (ba, bb)) + la lb + in + dq va kl + | DChoice(va, la), DChoice(vb, lb) -> + let v, kl = + if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then + va, List.map (fun (k, ca) -> k, f (ca, nb)) la + else + vb, List.map (fun (k, cb) -> k, f (na, cb)) lb + in + dq v kl + + | DChoice(va, la), _ -> + let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in + dq va kl + | _, DChoice(vb, lb) -> + let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in + dq vb kl + + | DVal u, DVal v -> + let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + in Hashtbl.add memo (na, nb) r; r + in + { leaves; ve; root = f (a.root, b.root) } + + (* + edd_meet : edd_v -> edd_v -> edd_v + *) + let edd_meet a b = + let ve = a.ve in + + let n = ref 0 in + let leaves = Hashtbl.create 12 in + + let get_leaf x = + if ND.is_bot x then DBot else begin + let id = ref None in + Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves; + match !id with + | Some i -> DVal i + | None -> + incr n; + Hashtbl.add leaves !n x; + DVal (!n) + end + in + + let memo = Hashtbl.create 12 in + let rec f (na, nb) = + try Hashtbl.find memo (na, nb) + with Not_found -> let r = + let dq v l = + let _, x0 = List.hd l in + if List.exists (fun (_, x) -> x <> x0) l + then DChoice(v, l) + else x0 + in + match na, nb with + | DBot, _ | _, DBot -> DBot + | DChoice(va, la), DChoice(vb, lb) when va = vb -> + let kl = List.map2 + (fun (ta, ba) (tb, bb) -> assert (ta = tb); + ta, f (ba, bb)) + la lb + in + dq va kl + | DChoice(va, la), DChoice(vb, lb) -> + let v, kl = + if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then + va, List.map (fun (k, ca) -> k, f (ca, nb)) la + else + vb, List.map (fun (k, cb) -> k, f (na, cb)) lb + in + dq v kl + | DChoice(va, la), _ -> + let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in + dq va kl + | _, DChoice(vb, lb) -> + let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in + dq vb kl + | DVal u, DVal v -> + let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in + get_leaf x + in Hashtbl.add memo (na, nb) r; r + in + { leaves; ve; root = f (a.root, b.root) } + + (* + edd_of_conslist : varenv -> enum_cons list -> edd_v + + Does this by dichotomy so that the EDD meets are done mostly on + small sized EDDs. + *) + let rec edd_of_conslist ve = function + | [] -> edd_top ve + | [a] -> edd_of_cons ve a + | l -> + let rec split = function + | [] -> [], [] + | [a] -> [a], [] + | a::b::q -> let u, v = split q in a::u, b::v + in + let u, v = split l in + edd_meet (edd_of_conslist ve u) (edd_of_conslist ve v) + + + let test () = + let ve = { + evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]]; + nvars = []; + ev_order = Hashtbl.create 2 } in + Hashtbl.add ve.ev_order "x" 0; + Hashtbl.add ve.ev_order "y" 1; + Hashtbl.add ve.ev_order "z" 2; + let u = edd_of_cons ve (E_EQ, "x", EIdent "y") in + Format.printf "x = y : @[%a@]@." edd_print u; + let v = edd_of_cons ve (E_NE, "y", EIdent "z") in + Format.printf "y != z : @[%a@]@." edd_print v; + let w = edd_meet u v in + Format.printf "x = y && y != z : @[%a@]@." edd_print w; + let t = edd_join u v in + Format.printf "x = y || y != z : @[%a@]@." edd_print t + + + (* ****************************** + Abstract interpret + ******************************* *) + + type env = { + rp : rooted_prog; + opt : cmdline_opt; + + ve : varenv; + + (* program expressions *) + f : bool_expr; + cl : conslist; + f_g : bool_expr; + cl_g : conslist; + guarantees : (id * bool_expr) list; + + (* abstract interpretation *) + cycle : (id * id * typ) list; (* s'(x) = s(y) *) + forget : (id * typ) list; (* s'(x) not specified *) + } + + (* + extract_linked_evars : conslist -> (id * id) list + + Extract all pairs of enum-type variable (x, y) appearing in an + equation like x = y or x != y + + A couple may appear several times in the result. + *) + let rec extract_linked_evars (ecl, _, r) = + let v_ecl = List.fold_left + (fun c (_, x, v) -> match v with + | EIdent y -> (x, y)::c + | _ -> c) + [] ecl + in + let v_ecl2 = + let q = List.fold_left + (fun c (_, x, v) -> match v with + | EItem _ -> x::c | _ -> c) + [] ecl + in + match q with + | [x; y] -> [x, y] + | _ -> [] + in + let rec aux = function + | CLTrue | CLFalse -> [] + | CLAnd(a, b) -> aux a @ aux b + | CLOr(a, b) -> extract_linked_evars a @ extract_linked_evars b + in + v_ecl @ v_ecl2 @ aux r + + (* + scope_constrict : id list -> (id * id) list -> id list + + Orders the variable in the first argument such as to minimize the + sum of the distance between the position of two variables appearing in + a couple of the second list. (minimisation is approximate, this is + an heuristic so that the EDD will not explode in size when expressing + equations such as x = y && u = v && a != b) + *) + let scope_constrict vars cp_id = + let var_i = Array.of_list vars in + let n = Array.length var_i in + + let i_var = Hashtbl.create n in + Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i; + + let cp_i = List.map + (fun (x, y) -> Hashtbl.find i_var x, Hashtbl.find i_var y) + cp_id in + + let eval i = + let r = Array.make n (-1) in + Array.iteri (fun pos var -> r.(var) <- pos) i; + Array.iteri (fun _ x -> assert (x <> (-1))) r; + List.fold_left + (fun s (x, y) -> s + abs (r.(x) - r.(y))) + 0 cp_i + in + + let best = Array.make n 0 in + for i = 0 to n-1 do best.(i) <- i done; + + let usefull = ref true in + Format.printf "SCA"; + while !usefull do + Format.printf ".@?"; + + usefull := false; + let try_s x = + if eval x < eval best then begin + Array.blit x 0 best 0 n; + usefull := true + end + in + + for i = 0 to n-1 do + let tt = Array.copy best in + (* move item i at beginning *) + let temp = tt.(i) in + for j = i downto 1 do tt.(j) <- tt.(j-1) done; + tt.(0) <- temp; + (* try all positions *) + try_s tt; + for j = 1 to n-1 do + let temp = tt.(j-1) in + tt.(j-1) <- tt.(j); + tt.(j) <- temp; + try_s tt + done + done + done; + Format.printf "@."; + + Array.to_list (Array.map (Array.get var_i) best) + + (* + init_env : cmdline_opt -> rooted_prog -> env + *) + let init_env opt rp = + Format.printf "Vars: @[<hov>%a@]@.@." + (print_list Ast_printer.print_typed_var ", ") + rp.all_vars; + + let enum_vars = List.fold_left + (fun v (_, id, t) -> match t with + | TEnum ch -> (id, ch)::v | _ -> v) + [] rp.all_vars in + let num_vars = List.fold_left + (fun v (_, id, t) -> match t with + | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v) + [] rp.all_vars in + + let init_f = Transform.init_f_of_prog rp in + Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; + let init_cl = conslist_of_f init_f in + + let guarantees = Transform.guarantees_of_prog rp in + Format.printf "Guarantees:@."; + List.iter (fun (id, f) -> + Format.printf " %s: %a@." id Formula_printer.print_expr f) + guarantees; + Format.printf "@."; + + let f = Formula.eliminate_not (Transform.f_of_prog rp false) in + let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in + Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; + + let cl = Formula.conslist_of_f f in + let cl_g = Formula.conslist_of_f f_g in + + (* calculate order for enumerated variables *) + let evars = List.map fst enum_vars in + + let lv0 = List.map (fun x -> x, "N"^x) + (List.filter (fun x -> List.exists (fun y -> y = "N"^x) evars) evars) in + let lv = lv0 @ extract_linked_evars init_cl @ extract_linked_evars cl_g in + let lv = uniq_sorted + (List.sort Pervasives.compare (List.map ord_couple lv)) in + let evars_ord = scope_constrict evars (lv0 @ lv) in + + let ev_order = Hashtbl.create (List.length evars) in + List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord; + let ve = { evars = enum_vars; nvars = num_vars; ev_order } in + + Format.printf "Order for variables: @[<hov>[%a]@]@." + (print_list Formula_printer.print_id ", ") evars_ord; + + (* calculate cycle variables and forget variables *) + let cycle = List.fold_left + (fun q (_, id, ty) -> + if id.[0] = 'N' then + (String.sub id 1 (String.length id - 1), id, ty)::q + else q) + [] rp.all_vars + in + let forget = List.map (fun (_, id, ty) -> (id, ty)) + (List.filter + (fun (_, id, _) -> + not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars)) + rp.all_vars) + in + + { rp; opt; ve; + f; cl; f_g; cl_g; guarantees; + cycle; forget } + + + + + let do_prog opt rp = + let e = init_env opt rp in + () + +end + + diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index b6c06fb..9a4d62d 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -1,6 +1,7 @@ open Ast open Lexing open Typing +open Util (* Locations *) @@ -69,14 +70,6 @@ let expr_precedence = function (* utility *) -let print_list f sep fmt l = - let rec aux = function - | [] -> () - | [a] -> f fmt a - | a::b -> f fmt a; Format.fprintf fmt "%s@," sep; aux b - in - aux l - let print_id_ext fmt (i, _) = Format.pp_print_string fmt i diff --git a/libs/util.ml b/libs/util.ml index 01b0c5c..443fb1e 100644 --- a/libs/util.ml +++ b/libs/util.ml @@ -1,3 +1,21 @@ +(* Small things *) + +let ord_couple (a, b) = if a < b then a, b else b, a + +(* uniq_sorted : 'a list -> 'a list *) +let rec uniq_sorted = function + | [] -> [] + | [a] -> [a] + | a::b::q when a = b -> uniq_sorted (b::q) + | a::r -> a::(uniq_sorted r) + +(* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *) +let rec list_fold_op op = function + | [] -> invalid_arg "list_fold_opt on empty list" + | [a] -> a + | x::q -> op x (list_fold_op op q) + + (* Either type *) type ('a, 'b) either = @@ -47,24 +65,15 @@ let rec fix equal f s = let (@@) f x = f x -let print_list x l = - Format.printf "%s: " x; +let print_list f sep fmt l = let rec aux = function | [] -> () - | [a] -> Format.printf "%s" a - | p::q -> Format.printf "%s, " p; aux q + | [a] -> f fmt a + | a::b -> f fmt a; Format.fprintf fmt "%s@," sep; aux b in - Format.printf "["; aux l; Format.printf "]@." + aux l let uid = let c = ref 0 in fun () -> c := !c + 1; string_of_int !c -(* On lists *) - -(* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *) -let rec list_fold_op op = function - | [] -> invalid_arg "list_fold_opt on empty list" - | [a] -> a - | x::q -> op x (list_fold_op op q) - @@ -12,6 +12,8 @@ module ItvND = Nonrelational.ND(Intervals_domain.VD) module AI_Itv = Abs_interp.I(Enum_domain.Valuation)(ItvND) module AI_Rel = Abs_interp.I(Enum_domain.Valuation)(Apron_domain.ND) +module AI_Itv_EDD = Abs_interp_edd.I(ItvND) + (* command line options *) let dump = ref false let dumprn = ref false @@ -19,6 +21,7 @@ let test = ref false let vtest = ref false let ai_itv = ref false let ai_rel = ref false +let ai_itv_edd = ref false let ai_root = ref "test" let ai_widen_delay = ref 3 let ai_no_time_scopes = ref "" @@ -36,6 +39,7 @@ let options = [ "--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-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)"; "--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)."; @@ -78,6 +82,8 @@ let do_test_interpret prog verbose = let () = Arg.parse options (fun f -> ifile := f) usage; + AI_Itv_EDD.test (); + if !ifile = "" then begin Format.eprintf "No input file...@."; exit 1 @@ -90,7 +96,7 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv || !ai_rel then begin + if !ai_itv || !ai_rel || !ai_itv_edd then begin let comma_split = Str.split (Str.regexp ",") in let select_f x = if x = "all" @@ -111,6 +117,7 @@ let () = if !ai_itv then AI_Itv.do_prog opt rp; if !ai_rel then AI_Rel.do_prog opt rp; + if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp; end; if !vtest then do_test_interpret prog true |