diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-15 11:35:12 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-15 11:35:12 +0200 |
commit | 4e66de932b91e91e4cadd943ff8859d6f69f57e1 (patch) | |
tree | ced73719216f2f1fd2eb9057001079a39dbad68e /abstract | |
parent | 7205927e18ea355a619e95b1036aac9b94a22667 (diff) | |
download | scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.tar.gz scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.zip |
Clean up & comment a bit.
Diffstat (limited to 'abstract')
-rw-r--r-- | abstract/abs_interp.ml | 13 | ||||
-rw-r--r-- | abstract/abs_interp_dynpart.ml | 9 | ||||
-rw-r--r-- | abstract/abs_interp_edd.ml | 61 | ||||
-rw-r--r-- | abstract/apron_domain.ml | 6 | ||||
-rw-r--r-- | abstract/domain.ml | 3 | ||||
-rw-r--r-- | abstract/enum_domain.ml | 12 | ||||
-rw-r--r-- | abstract/enum_domain_edd.ml | 4 | ||||
-rw-r--r-- | abstract/formula.ml | 165 | ||||
-rw-r--r-- | abstract/formula_printer.ml | 2 | ||||
-rw-r--r-- | abstract/intervals_domain.ml | 7 | ||||
-rw-r--r-- | abstract/nonrelational.ml | 11 | ||||
-rw-r--r-- | abstract/num_domain.ml | 5 | ||||
-rw-r--r-- | abstract/transform.ml | 32 | ||||
-rw-r--r-- | abstract/value_domain.ml | 7 | ||||
-rw-r--r-- | abstract/varenv.ml | 33 |
15 files changed, 242 insertions, 128 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index b5fc684..319f105 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -3,6 +3,7 @@ open Ast_util open Formula open Typing open Cmdline +open Varenv open Util open Num_domain @@ -12,8 +13,6 @@ open Enum_domain module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig - type st - val do_prog : cmdline_opt -> rooted_prog -> unit end = struct @@ -22,6 +21,14 @@ end = struct Disjunction domain ************************** *) + (* + This domain uses a fix set of enumerate-type variables to make disjunctions between + different cases that are analyzed. A case is a list of values for each of these + disjunction variables. The value for that case is the product of a value in a domain + specific for enumerated variables and a domain for numeric variables. See README for + more details. + *) + type case_v = ED.t * ND.t type case = ED.item list @@ -291,7 +298,7 @@ end = struct (* add variables from LASTs *) let last_vars = uniq_sorted - (List.sort compare (Transform.extract_last_vars f)) in + (List.sort compare (extract_last_vars f)) in let last_vars = List.map (fun id -> let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml index 5beffda..23df612 100644 --- a/abstract/abs_interp_dynpart.ml +++ b/abstract/abs_interp_dynpart.ml @@ -19,6 +19,15 @@ end = struct type abs_v = ED.t * ND.t + (* + Abstract analysis based on dynamic partitionning of the state space. + Idea : use somme conditions appearing in the text of the program as + disjunctions. We don't want to consider them all at once in the first + place because it would be way too costly ; instead we try to dynamically + partition tye system. But we haven't got a very good heuristic for that, + so it doesn't work very well. + *) + type location = { id : int; depth : int; 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...@."; diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index 288f961..a929c0b 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -6,6 +6,11 @@ open Num_domain open Apron +(* + Link between our NUMERICAL_ENVIRONMENT_DOMAIN interface and Apron. + Mostly direct translation between the two. +*) + module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* manager *) @@ -18,7 +23,6 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct type t = man Abstract1.t (* direct translation of numerical expressions into Apron tree expressions *) - (* TODO : some variables have type real and not int... *) let rec texpr_of_nexpr = function | NIdent id -> Texpr1.Var (Var.of_string id) | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i)) diff --git a/abstract/domain.ml b/abstract/domain.ml deleted file mode 100644 index 76635d1..0000000 --- a/abstract/domain.ml +++ /dev/null @@ -1,3 +0,0 @@ -open Ast -open Formula - diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index 77d7e3f..68b04f5 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -4,6 +4,18 @@ open Util exception Bot +(* + Interface and implementation of an abstract domain meant to handle + constraints on enumerated variables. + + Constraints are basically of two types : + - var OP value + - var OP var' + with OP either == or != + + (see formula.ml for a definition of the enum_cons type) +*) + module type ENUM_ENVIRONMENT_DOMAIN = sig type t diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml index ae71b09..3e03d59 100644 --- a/abstract/enum_domain_edd.ml +++ b/abstract/enum_domain_edd.ml @@ -3,6 +3,10 @@ open Formula open Util open Enum_domain +(* + Implementation of a more powerfull domain for enumerate constraints, + based on decision graphs (BDD). +*) module EDD : ENUM_ENVIRONMENT_DOMAIN = struct exception Top diff --git a/abstract/formula.ml b/abstract/formula.ml index 650f8f4..4102891 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -4,6 +4,21 @@ open Ast_util (* AST for logical formulas *) +(* + Two representations are used for the formulas : + - Formula tree, representing the boolean formula directly + as would be expected + - "conslist", where all the numerical and enumerate constraints + considered in a tree of ANDs are regrouped in a big list. + The second form is used when applying a formula to an abstract value, + whereas the first form is the one generated by the program transformation + procedure and is the one we prefer to show the user because it is more + easily understandable. +*) + +(* ------------------------------------ *) +(* First representation *) +(* ------------------------------------ *) (* Numerical part *) @@ -27,7 +42,6 @@ type num_cons = num_expr * num_cons_op (* always imply right member = 0 *) (* Logical part *) - (* Enumerated types *) type enum_expr = | EIdent of id @@ -52,6 +66,11 @@ type bool_expr = (* (A and B) or ((not A) and C) *) | BNot of bool_expr +(* + Helper functions to construct formula trees and automatically + simplifying some tautologies/contradictions +*) + let is_false = function | BConst false | BNot(BConst true) -> true | _ -> false @@ -85,7 +104,10 @@ let f_e_op op a b = match a, b with | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v) let f_e_eq = f_e_op E_EQ -(* Write all formula without using the NOT operator *) +(* + Transformation functions so that all the logical formula are written + without using the NOT operator +*) let rec eliminate_not = function | BNot e -> eliminate_not_negate e @@ -117,68 +139,19 @@ and eliminate_not_negate = function BOr(eliminate_not_negate a, eliminate_not_negate b) | BOr(a, b) -> BAnd(eliminate_not_negate a, eliminate_not_negate b) + +(* ------------------------------------ *) +(* Simplification functions on the *) +(* first representation *) +(* ------------------------------------ *) (* - In big ANDs, try to separate levels of /\ and levels of \/ - We also use this step to simplify trues and falses that may be present. -*) - -type conslist = enum_cons list * num_cons list * conslist_bool_expr -and conslist_bool_expr = - | CLTrue - | CLFalse - | CLAnd of conslist_bool_expr * conslist_bool_expr - | CLOr of conslist * conslist - -let rec conslist_of_f = function - | BNot e -> conslist_of_f (eliminate_not_negate e) - | BRel (op, a, b, is_real) -> - let x, y, op = match op with - | AST_EQ -> a, b, CONS_EQ - | AST_NE -> a, b, CONS_NE - | AST_GT -> a, b, CONS_GT - | AST_GE -> a, b, CONS_GE - | AST_LT -> b, a, CONS_GT - | AST_LE -> b, a, CONS_GE - in - let cons = if y = NIntConst 0 || y = NRealConst 0. - then (x, op) - else (NBinary(AST_MINUS, x, y, is_real), op) - in [], [cons], CLTrue - | BConst x -> - [], [], if x then CLTrue else CLFalse - | BEnumCons e -> - [e], [], CLTrue - | BOr(a, b) -> - let eca, ca, ra = conslist_of_f a in - let ecb, cb, rb = conslist_of_f b in - begin match eca, ca, ra, ecb, cb, rb with - | _, _, CLFalse, _, _, _ -> ecb, cb, rb - | _, _, _, _, _, CLFalse -> eca, ca, ra - | [], [], CLTrue, _, _, _ -> [], [], CLTrue - | _, _, _, [], [], CLTrue -> [], [], CLTrue - | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb)) - end - | BAnd(a, b) -> - let eca, ca, ra = conslist_of_f a in - let ecb, cb, rb = conslist_of_f b in - let cons = ca @ cb in - let econs = eca @ ecb in - begin match ra, rb with - | CLFalse, _ | _, CLFalse -> [], [], CLFalse - | CLTrue, _ -> econs, cons, rb - | _, CLTrue -> econs, cons, ra - | _, _ -> econs, cons, CLAnd(ra, rb) - end - | BTernary(c, a, b) -> - conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b))) - - - -(* - Simplify formula considering something is true + Extract enumerated and numeric constants that + are always true in the formula (ie do not appear + under an OR or a ternary). + (not mathematically exact : only a subset is returned) *) let rec get_root_true = function @@ -188,6 +161,13 @@ let rec get_root_true = function | BRel (a, b, c, d) -> [BRel (a, b, c, d)] | _ -> [] +(* + Simplify formula considering something is true + (only does some clearly visible simplifications ; + later simplifications are implicitly done when + abstract-interpreting the formula) +*) + let rec simplify true_eqs e = if List.exists (fun f -> @@ -228,7 +208,6 @@ let rec simplify_k true_eqs e = List.fold_left f_and (simplify true_eqs e) true_eqs - (* Simplify a formula replacing a variable with another *) @@ -266,7 +245,7 @@ let rec formula_replace_evars repls e = (* - extract names of variables referenced in formula + Extract names of enumerated variables referenced in formula *) let rec refd_evars_of_f = function @@ -276,3 +255,65 @@ let rec refd_evars_of_f = function | BEnumCons(_, e, EItem _) -> [e] | BEnumCons(_, e, EIdent f) -> [e; f] | _ -> [] + + + +(* ------------------------------------ *) +(* Second representation *) +(* ------------------------------------ *) + +(* + In big ANDs, try to separate levels of /\ and levels of \/ + We also use this step to simplify trues and falses that may be present. +*) + +type conslist = enum_cons list * num_cons list * conslist_bool_expr +and conslist_bool_expr = + | CLTrue + | CLFalse + | CLAnd of conslist_bool_expr * conslist_bool_expr + | CLOr of conslist * conslist + +let rec conslist_of_f = function + | BNot e -> conslist_of_f (eliminate_not_negate e) + | BRel (op, a, b, is_real) -> + let x, y, op = match op with + | AST_EQ -> a, b, CONS_EQ + | AST_NE -> a, b, CONS_NE + | AST_GT -> a, b, CONS_GT + | AST_GE -> a, b, CONS_GE + | AST_LT -> b, a, CONS_GT + | AST_LE -> b, a, CONS_GE + in + let cons = if y = NIntConst 0 || y = NRealConst 0. + then (x, op) + else (NBinary(AST_MINUS, x, y, is_real), op) + in [], [cons], CLTrue + | BConst x -> + [], [], if x then CLTrue else CLFalse + | BEnumCons e -> + [e], [], CLTrue + | BOr(a, b) -> + let eca, ca, ra = conslist_of_f a in + let ecb, cb, rb = conslist_of_f b in + begin match eca, ca, ra, ecb, cb, rb with + | _, _, CLFalse, _, _, _ -> ecb, cb, rb + | _, _, _, _, _, CLFalse -> eca, ca, ra + | [], [], CLTrue, _, _, _ -> [], [], CLTrue + | _, _, _, [], [], CLTrue -> [], [], CLTrue + | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb)) + end + | BAnd(a, b) -> + let eca, ca, ra = conslist_of_f a in + let ecb, cb, rb = conslist_of_f b in + let cons = ca @ cb in + let econs = eca @ ecb in + begin match ra, rb with + | CLFalse, _ | _, CLFalse -> [], [], CLFalse + | CLTrue, _ -> econs, cons, rb + | _, CLTrue -> econs, cons, ra + | _, _ -> econs, cons, CLAnd(ra, rb) + end + | BTernary(c, a, b) -> + conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b))) + diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index a5359a8..dd902ad 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -3,6 +3,8 @@ open Ast open Formula open Ast_printer +(* Just a pretty-printer, nothing to see here *) + let string_of_binary_rel = function | AST_EQ -> "=" | AST_NE -> "≠" diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 084e397..22ea60b 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -1,5 +1,12 @@ open Value_domain +(* + Value domain for representing one interval, doing operations on + such representations, etc. + + Restricted implementation, only support integers. +*) + module VD : VALUE_DOMAIN = struct type t = itv diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index efa30dd..ed029da 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -5,9 +5,11 @@ open Ast open Value_domain open Num_domain -let debug = false +(* + Implementation of a nonrelationnal domain for numerical values. -(* Restricted domain, only support integers *) + Restricted implementation, only support integers. +*) module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct type env = V.t VarMap.t @@ -160,11 +162,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u | AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v in - if debug then Format.printf - "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i - (Formula_printer.string_of_binary_rel op) - Formula_printer.print_num_expr expr - (V.to_string v1) (V.to_string v2) (V.to_string v1'); Env (VarMap.add i v1' env)) env in diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml index 285b3c4..a91c69f 100644 --- a/abstract/num_domain.ml +++ b/abstract/num_domain.ml @@ -1,6 +1,11 @@ open Ast open Formula +(* + Interface specification for a numerical environment domain + (relationnal with Apron or nonrelationnal with intervals) +*) + module type NUMERICAL_ENVIRONMENT_DOMAIN = sig type t type itv diff --git a/abstract/transform.ml b/abstract/transform.ml index 20512aa..eedec3e 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -7,7 +7,8 @@ open Typing open Interpret (* used for constant evaluation ! *) -(* Transform SCADE program to logical formula. +(* Transform SCADE program to logical formula. + See formula.ml for a description of the formula's AST. Convention : to access the last value of a variable, access the variable with the same name prefixed by "L". @@ -527,8 +528,6 @@ let f_of_prog_incl_init rp assume_guarantees = assume_guarantees in f_and clock_eq (f_and no_next_init_cond scope_f) - - (* Get expressions for guarantee violation @@ -583,30 +582,3 @@ and guarantees_of_prog rp = -(* - Extract variables accessed by a LAST -*) - -let rec extract_last_vars = function - | BRel(_, a, b, _) -> - elv_ne a @ elv_ne b - | BEnumCons c -> - elv_ec c - | BAnd(a, b) | BOr (a, b) -> - extract_last_vars a @ extract_last_vars b - | BNot(e) -> extract_last_vars e - | BTernary(c, a, b) -> extract_last_vars c @ - extract_last_vars a @ extract_last_vars b - | _ -> [] - -and elv_ne = function - | NIdent i when i.[0] = 'L' -> [i] - | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b - | NUnary (_, a, _) -> elv_ne a - | _ -> [] - -and elv_ec (_, v, q) = - (if v.[0] = 'L' then [v] else []) @ - (match q with - | EIdent i when i.[0] = 'L' -> [i] - | _ -> []) diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index 0a421f7..48d87f9 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -1,4 +1,11 @@ +(* + Interface definition for any single-value abstract domain. + Only implementation of interface is intervals. +*) + + + type bound = Int of int | PInf | MInf type itv = Itv of bound * bound | Bot diff --git a/abstract/varenv.ml b/abstract/varenv.ml index 4d6caca..cf29edf 100644 --- a/abstract/varenv.ml +++ b/abstract/varenv.ml @@ -25,6 +25,37 @@ type varenv = { + +(* + Extract variables accessed by a LAST +*) + +let rec extract_last_vars = function + | BRel(_, a, b, _) -> + elv_ne a @ elv_ne b + | BEnumCons c -> + elv_ec c + | BAnd(a, b) | BOr (a, b) -> + extract_last_vars a @ extract_last_vars b + | BNot(e) -> extract_last_vars e + | BTernary(c, a, b) -> extract_last_vars c @ + extract_last_vars a @ extract_last_vars b + | _ -> [] + +and elv_ne = function + | NIdent i when i.[0] = 'L' -> [i] + | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b + | NUnary (_, a, _) -> elv_ne a + | _ -> [] + +and elv_ec (_, v, q) = + (if v.[0] = 'L' then [v] else []) @ + (match q with + | EIdent i when i.[0] = 'L' -> [i] + | _ -> []) + + + (* extract_linked_evars : conslist -> (id * id) list @@ -200,7 +231,7 @@ let force_ordering vars groups = let mk_varenv (rp : rooted_prog) f cl = (* add variables from LASTs *) let last_vars = uniq_sorted - (List.sort compare (Transform.extract_last_vars f)) in + (List.sort compare (extract_last_vars f)) in let last_vars = List.map (fun id -> let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars |