diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 61 |
1 files changed, 40 insertions, 21 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 31fe5aa..722dc1a 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -26,6 +26,27 @@ end = struct (* ********************** EDD Domain ********************** *) + + (* + This abstract domain is capable of representing values of a program using enumerated + variables and numerical variables. The representation is a decision graph on + enumerated variables, whose leaves are values for the numerical variables in a given + numerical domain (relationnal or non-relationnal). This domain necessarily does the + disjunction between all the cases that appear for the enumerated variables, and is + not able to do a disjunction with respect to a condition on numerical variables if + that condition is not bound to a boolean variable appearing in the program. + + Possible extensions : + - use groups of variables, so that an EDD does not have to consider all the + numerical and enumerated variables at once + - add the possibility for numeric condition decision nodes (something like ghost + boolean variables that would be bound to a numeric condition) + - ... + + This domain is currently the most promising lead in our research on abstract + interpretation of Scade programs. + *) + type edd = | DBot | DTop @@ -479,10 +500,10 @@ end = struct let ve = v.ve in let leaves, get_leaf = get_leaf_fun () in + let dq = new_node_fun () in - let nc = ref 0 in let memo = Hashtbl.create 12 in - let node_memo = Hashtbl.create 12 in + let rec f l = let kl = List.sort Pervasives.compare (List.map key l) in try Hashtbl.find memo kl @@ -522,16 +543,7 @@ end = struct let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in c, f (ch1@ch2@ch3)) cl in - let _, x0 = List.hd cc in - if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc - then begin - let k = (dv, List.map (fun (a, b) -> a, key b) cc) in - let n = - try Hashtbl.find node_memo k - with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc) - in - DChoice(n, dv, cc) - end else x0 + dq dv cc with | Top -> DTop in Hashtbl.add memo kl r; r in @@ -616,7 +628,7 @@ end = struct (* - edd_join_widen : edd_v -> edd_v -> edd_v + edd_widen : edd_v -> edd_v -> edd_v *) let edd_widen (a:edd_v) (b:edd_v) = let ve = a.ve in @@ -658,7 +670,7 @@ end = struct | _ -> assert false in - { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) } + { leaves; ve; root = time "widen" (fun () -> memo2 f a.root b.root) } (* edd_accumulate : edd_v -> edd_v -> edd_v @@ -703,7 +715,7 @@ end = struct | _ -> assert false in - { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) } + { leaves; ve; root = time "accumulate" (fun () -> memo2 f a.root b.root) } (* edd_star_new : edd_v -> edd_v -> edd_v @@ -775,9 +787,11 @@ end = struct let f = simplify_k (get_root_true f) f in Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f; - (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *) - (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *) - (* WHY THE **** AM I SHOUTING LIKE THAT ? *) + (* + Here we simplify the program formula so that uselessly redundant variables don't + appear anymore. If an enumerated equation x = y appears at the root of the + program, then we chose to remove either x or y. + *) let facts = get_root_true f in let f, rp, repls = List.fold_left (fun (f, (rp : rooted_prog), repls) eq -> @@ -814,6 +828,11 @@ end = struct Format.printf "Complete formula after simpl:@.%a@.@." Formula_printer.print_expr f; + (* + Here we specialize the program formula for the two following cases : + - L/must_reset = tt, this is the first instant of the program (global reset) + - L/must_reset = ff, this is for all the rest of the time + *) let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f in @@ -839,10 +858,8 @@ end = struct let ve = mk_varenv rp f cl in - { rp; opt; ve; init_cl; cl; guarantees; } - let do_prog opt rp = @@ -925,8 +942,10 @@ end = struct let init_acc = edd_star_new (edd_bot e.ve) (pass_cycle e.ve (edd_apply_cl (edd_top e.ve) e.init_cl)) in - (* Dump final state *) + (* Iterate *) let acc = ch_it 0 init_acc in + + (* Dump final state *) edd_dump_graphviz acc "/tmp/graph-final0.dot"; Format.printf "Finishing up...@."; |