diff options
| -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 | ||||
| -rw-r--r-- | frontend/ast.ml | 11 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 20 | ||||
| -rw-r--r-- | frontend/file_parser.ml | 17 | ||||
| -rw-r--r-- | frontend/rename.ml | 10 | ||||
| -rw-r--r-- | interpret/bad_interpret.ml | 308 | ||||
| -rw-r--r-- | interpret/interpret.ml | 7 | ||||
| -rw-r--r-- | libs/util.ml | 16 | ||||
| -rw-r--r-- | main.ml | 20 |
23 files changed, 305 insertions, 474 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 diff --git a/frontend/ast.ml b/frontend/ast.ml index d55626d..773efa4 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -2,6 +2,15 @@ open Lexing open Util +(* + Abstract Syntax Tree for a subset of the SCADE language. + + This subset includes : + - basic dataflow core (excluding when, merge, and all other clock primitives) + - activate blocks + - automata with weak transitions only +*) + type 'a ext = 'a * extent type id = string @@ -63,7 +72,7 @@ type expr = type var_def = bool * id * typ type automaton = id * state ext list * id list -and state = { +and state = { initial : bool; st_name : id; st_locals : var_def list; diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index 8908687..09f4986 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -3,23 +3,9 @@ open Lexing open Typing open Util - -(* Locations *) - -let string_of_position p = - Printf.sprintf "%s:%i:%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) - -let string_of_extent (p,q) = - if p.pos_fname = q.pos_fname then - if p.pos_lnum = q.pos_lnum then - if p.pos_cnum = q.pos_cnum then - Printf.sprintf "%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) - else - Printf.sprintf "%s:%i.%i-%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (q.pos_cnum - q.pos_bol) - else - Printf.sprintf "%s:%i.%i-%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_lnum (q.pos_cnum - q.pos_bol) - else - Printf.sprintf "%s:%i.%i-%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_fname q.pos_lnum (q.pos_cnum - q.pos_bol) +(* + Just a pretty-printer, nothing to see here. +*) (* Operators *) diff --git a/frontend/file_parser.ml b/frontend/file_parser.ml deleted file mode 100644 index 85eb9cd..0000000 --- a/frontend/file_parser.ml +++ /dev/null @@ -1,17 +0,0 @@ -open Ast -open Ast_printer -open Lexing - -let parse_file (filename : string) : prog = - let f = open_in filename in - let lex = from_channel f in - try - lex.lex_curr_p <- { lex.lex_curr_p with pos_fname = filename; }; - Parser.file Lexer.token lex - with - | Parser.Error -> - Util.error (Printf.sprintf "Parse error (invalid syntax) near %s" - (string_of_position lex.lex_start_p)) - | Failure "lexing: empty token" -> - Util.error (Printf.sprintf "Parse error (invalid token) near %s" - (string_of_position lex.lex_start_p)) diff --git a/frontend/rename.ml b/frontend/rename.ml index 9c4cc31..71ec321 100644 --- a/frontend/rename.ml +++ b/frontend/rename.ml @@ -1,4 +1,12 @@ -(* Scope analyzer *) +(* + Scope analyzer + + Does a tiny bit of renaming, so that in a given node, every + variable declaration is unique. + + Variable name unicity is not assured program-wide. Node paths are + handled only once the program has been "rooted" (see fronted/typing.ml) +*) open Ast open Util diff --git a/interpret/bad_interpret.ml b/interpret/bad_interpret.ml deleted file mode 100644 index 08ccf85..0000000 --- a/interpret/bad_interpret.ml +++ /dev/null @@ -1,308 +0,0 @@ -open Ast -open Data -open Util -open Ast_util - -(* Data structures for the interpret *) - -type scope = string - -type svalue = - | VInt of int - | VBool of bool - | VReal of float - | VState of id - | VPrevious of value - | VBusy (* intermediate value : calculating ! for detection of cycles *) -and value = svalue list - -type state = svalue VarMap.t - -(* functions for recursively getting variables *) - -type calc_fun = - | F of (state -> calc_map -> state) -and calc_map = calc_fun VarMap.t - -let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) = - let st = - if VarMap.mem id st then st - else match VarMap.find id c with - | F f -> - (* Format.printf "%s[ " id; *) - let r = f (VarMap.add id VBusy st) c in - (* Format.printf "]%s " id; *) - r - in - match VarMap.find id st with - | VBusy -> combinatorial_cycle id - | v -> st, v - -(* pretty-printing *) - -let rec str_of_value = function - | VInt i -> string_of_int i - | VReal r -> string_of_float r - | VBool b -> if b then "true" else "false" - | VState s -> "state " ^ s - | VPrevious p -> - "[" ^ - List.fold_left (fun s v -> (if s = "" then "" else s ^ ", ") ^ str_of_value v) "" p - ^ "]" - | VBusy -> "#" -let print_state st = - VarMap.iter (fun id v -> Format.printf "%s = %s@." id (str_of_value v)) st - - - - -(* Expression evaluation *) - -type eval_env = { - p: prog; - c: calc_map; - scopes: string list; -} - -(* - eval_expr : eval_env -> string -> expr ext -> (state * value) -*) -let rec eval_expr env st exp = - let sub_eval = eval_expr env in - let scope = List.hd env.scopes in - match fst exp with - | AST_identifier (id, _) -> - let rec aux = function - | [] -> - no_variable id - | sc::q -> - try let st, v = get_var st env.c (sc^"/"^id) in st, [v] - with Not_found -> aux q - in loc_error (snd exp) aux env.scopes - | AST_idconst (id, _) -> - let st, v = get_var st env.c ("cst/"^id) in st, [v] - (* on numerical values *) - | AST_int_const (i, _) -> st, [VInt (int_of_string i)] - | AST_real_const (r, _) -> st, [VReal (float_of_string r)] - | AST_unary(AST_UPLUS, e) -> sub_eval st e - | AST_unary(AST_UMINUS, e) -> - begin match sub_eval st e with - | st, [VInt x] -> st, [VInt (-x)] - | st, [VReal x] -> st, [VReal(-. x)] - | _ -> type_error "Unary on non-numerical." - end - | AST_binary(op, e1, e2) -> - let st, v1 = sub_eval st e1 in - let st, v2 = sub_eval st e2 in - let iop, fop = match op with - | AST_PLUS -> (+), (+.) - | AST_MINUS -> (-), (-.) - | AST_MUL -> ( * ), ( *. ) - | AST_DIV -> (/), (/.) - | AST_MOD -> (mod), mod_float - in - begin match v1, v2 with - | [VInt a], [VInt b] -> st, [VInt (iop a b)] - | [VReal a], [VReal b] -> st, [VReal(fop a b)] - | _ -> type_error "Invalid arguments for numerical binary." - end - (* on boolean values *) - | AST_bool_const b -> st, [VBool b] - | AST_binary_rel(op, e1, e2) -> - let st, v1 = sub_eval st e1 in - let st, v2 = sub_eval st e2 in - let r = match op with - | AST_EQ -> (=) | AST_NE -> (<>) - | AST_LT -> (<) | AST_LE -> (<=) - | AST_GT -> (>) | AST_GE -> (>=) - in - begin match v1, v2 with - | [VInt a], [VInt b] -> st, [VBool (r a b)] - | [VReal a], [VReal b] -> st, [VBool (r a b)] - | [VBool a], [VBool b] -> st, [VBool (r a b)] - | _ -> type_error "Invalid arguments for binary relation." - end - | AST_binary_bool(op, e1, e2) -> - let st, v1 = sub_eval st e1 in - let st, v2 = sub_eval st e2 in - let r = match op with - | AST_AND -> (&&) | AST_OR -> (||) - in - begin match v1, v2 with - | [VBool a], [VBool b] -> st, [VBool (r a b)] - | _ -> type_error "Invalid arguments for boolean relation." - end - | AST_not(e) -> - begin match sub_eval st e with - | st, [VBool b] -> st, [VBool (not b)] - | _ -> type_error "Invalid arguments for boolean negation." - end - (* temporal primitives *) - | AST_pre(exp, n) -> - begin try match VarMap.find (scope^"/"^n) st with - | VPrevious x -> st, x - | _ -> st, [] - with Not_found -> st, [] - end - | AST_arrow(before, after) -> - begin try match VarMap.find (scope^"/init") st with - | VBool true -> sub_eval st before - | VBool false -> sub_eval st after - | _ -> assert false - with Not_found -> error ("Internal: could not find init for scope " ^ scope) - end - (* other *) - | AST_if(cond, a, b) -> - let st, cv = sub_eval st cond in - begin match cv with - | [VBool true] -> sub_eval st a - | [VBool false] -> sub_eval st b - | _ -> type_error "Invalid condition in if." - end - | AST_instance((f, _), args, nid) -> - let (n, _) = find_node_decl env.p f in - List.fold_left - (fun (st, vs) (_, (id,_), _) -> - let st, v = get_var st env.c (scope^"/"^nid^"/"^id) in - st, vs @ [v]) - (st, []) n.ret - -(* Constant calculation *) - -let rec calc_const p d st c = - let env = { p = p; c = c; scopes = ["cst"] } in - match eval_expr env st d.value with - | st, [v] -> VarMap.add ("cst/"^d.c_name) v st - | _ -> type_error ("Cannot assign tuple to constant" ^ d.c_name) - -let program_consts p = - let cdecl = extract_const_decls p in - let ccmap = List.fold_left - (fun c (d, _) -> VarMap.add ("cst/"^d.c_name) (F (calc_const p d)) c) - VarMap.empty cdecl - in - List.fold_left - (fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.c_name) in st) - VarMap.empty - cdecl - -(* get initial state for program *) -let program_init_state p root_node = - let (n, _) = find_node_decl p root_node in - let rec aux st p scope eqs = - let st = VarMap.add (scope^"/init") (VBool true) st in - let add_subscopes = - List.fold_left (fun st (ss_id, ss_eqs, _) -> aux st p (scope^"/"^ss_id) ss_eqs) - in - let add_eq st eq = match fst eq with - | AST_assign(_, e) -> add_subscopes st (extract_instances p e) - | AST_assume _ | AST_guarantee _ -> st - | AST_automaton (aid, astates, ret) -> - let (initial, _) = List.find (fun (s, _) -> s.initial) astates in - let st = VarMap.add (scope^":"^aid^".state") (VState initial.name) st in - let add_astate st ((astate:Ast.state), _) = - aux st p (scope^":"^aid^"."^astate.name) astate.body - in - List.fold_left add_astate st astates - | AST_activate _ -> not_implemented "program_init_state activate" - in - List.fold_left add_eq st eqs - in - aux (program_consts p) p "" n.body - - -(* Program execution *) - -(* build calc map *) -let rec build_prog_ccmap p scopes eqs st = - let scope = List.hd scopes in - let add_eq c eq = match fst eq with - | AST_assign(vars, e) -> - let calc st c = - let env = { p = p; c = c; scopes = scopes } in - let st, vals = eval_expr env st e in - List.fold_left2 - (fun st (id,_) v -> VarMap.add (scope^"/"^id) v st) - st vars vals - in - let c = List.fold_left (fun c (id, _) -> VarMap.add (scope^"/"^id) (F calc) c) c vars in - - let add_subscope c (ss_id, ss_eqs, ss_args) = - let c = VarMap.merge disjoint_union c - (build_prog_ccmap p [scope^"/"^ss_id] ss_eqs st) - in - let add_v c ((_, (id, _), _), eq) = - let calc st c = - let env = { p = p; c = c; scopes = scopes } in - let st, vals = eval_expr env st eq in - match vals with - | [v] -> VarMap.add (scope^"/"^ss_id^"/"^id) v st - | _ -> type_error "invalid arity" - in - VarMap.add (scope^"/"^ss_id^"/"^id) (F calc) c - in - List.fold_left add_v c ss_args - in - List.fold_left add_subscope c (extract_instances p e) - | AST_assume _ | AST_guarantee _ -> c - | AST_automaton _ -> not_implemented "build_prog_ccmap for automaton" - | AST_activate _ -> not_implemented "build_prog_ccmap for activate" - in - List.fold_left add_eq VarMap.empty eqs - -let extract_next_state active env eqs st = - let csts = VarMap.filter - (fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/") - st - in - let rec aux active scopes eqs st nst = - let scope = List.hd env.scopes in - - let r = VarMap.add (scope^"/init") - (if active then VBool false - else try VarMap.find (scope^"/init") st with Not_found -> assert false) - nst - in - let add_subscopes active = - List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) -> - aux active [scope^"/"^ss_id] ss_eqs st nst) - in - let add_eq (st, nst) eq = match fst eq with - | AST_assign(vars, e) -> - let st, nst = add_subscopes active (st, nst) (extract_instances env.p e) in - List.fold_left (fun (st, nst) (pn, pe) -> - let st, v = if active then eval_expr { env with scopes = scopes } st pe - else st, - try match VarMap.find (scope^"/"^pn) st with VPrevious x -> x | _ -> [] - with Not_found -> [] - in - st, VarMap.add (scope^"/"^pn) (VPrevious v) nst) - (st, nst) (extract_pre e) - | AST_assume _ | AST_guarantee _ -> st, nst - | AST_automaton _ -> not_implemented "extract_next_state automaton" - | AST_activate _ -> not_implemented "extract_next_state activate" - in - List.fold_left add_eq (st, r) eqs - in aux active env.scopes eqs st csts - - - -let program_step p st inputs root_node = - let (n, _) = find_node_decl p root_node in - let st = List.fold_left - (fun st (n, v) -> VarMap.add ("/"^n) v st) st inputs in - - let ccmap = build_prog_ccmap p [""] n.body st in - - let st = List.fold_left - (fun st (_, (id, _), _) -> let st, _ = get_var st ccmap ("/"^id) in st) - st n.ret in - let outputs = List.map - (fun (_, (id, _), _) -> let _, v = get_var st ccmap ("/"^id) in (id, v)) - n.ret in - - let st, next_st = extract_next_state true { p = p; scopes = [""]; c = ccmap } n.body st in - - st, outputs, next_st - - diff --git a/interpret/interpret.ml b/interpret/interpret.ml index 8bdf650..f14d6e2 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -1,3 +1,10 @@ +(* + Interpret for a portion of the concrete semantics of the Scade language. + (basically, interpretation is handled for all the subset of the language + that we can parse). +*) + + open Ast open Util open Ast_util diff --git a/libs/util.ml b/libs/util.ml index 6e8dc59..ffeee82 100644 --- a/libs/util.ml +++ b/libs/util.ml @@ -1,4 +1,5 @@ open Unix +open Lexing (* Small things *) @@ -33,6 +34,21 @@ let position_unknown = Lexing.dummy_pos type extent = position * position let extent_unknown = (position_unknown, position_unknown) +let string_of_position p = + Printf.sprintf "%s:%i:%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) + +let string_of_extent (p,q) = + if p.pos_fname = q.pos_fname then + if p.pos_lnum = q.pos_lnum then + if p.pos_cnum = q.pos_cnum then + Printf.sprintf "%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) + else + Printf.sprintf "%s:%i.%i-%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (q.pos_cnum - q.pos_bol) + else + Printf.sprintf "%s:%i.%i-%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_lnum (q.pos_cnum - q.pos_bol) + else + Printf.sprintf "%s:%i.%i-%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_fname q.pos_lnum (q.pos_cnum - q.pos_bol) + (* Exceptions *) @@ -1,3 +1,5 @@ +open Lexing + open Cmdline open Ast @@ -108,6 +110,20 @@ let options = [ "Scopes for which to introduce a 'init' variable in analysis."; ] +let parse_file (filename : string) : prog = + let f = open_in filename in + let lex = from_channel f in + try + lex.lex_curr_p <- { lex.lex_curr_p with pos_fname = filename; }; + Parser.file Lexer.token lex + with + | Parser.Error -> + Util.error (Printf.sprintf "Parse error (invalid syntax) near %s" + (Util.string_of_position lex.lex_start_p)) + | Failure "lexing: empty token" -> + Util.error (Printf.sprintf "Parse error (invalid token) near %s" + (Util.string_of_position lex.lex_start_p)) + let do_test_interpret prog verbose = let f0 _ = false in let s0 = Interpret.init_state (Typing.root_prog prog "test" f0 f0) in @@ -150,7 +166,7 @@ let () = end; try - let prog = File_parser.parse_file !ifile in + let prog = parse_file !ifile in if !dump then Ast_printer.print_prog Format.std_formatter prog; let prog = Rename.rename_prog prog in @@ -211,6 +227,6 @@ let () = | Util.LocError(l, e) -> Format.eprintf "Error: %s@." e; List.iter - (fun loc -> Format.eprintf "At: %s@." (Ast_printer.string_of_extent loc)) + (fun loc -> Format.eprintf "At: %s@." (Util.string_of_extent loc)) l |