diff options
| -rw-r--r-- | frontend/ast.ml | 13 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 63 | ||||
| -rw-r--r-- | frontend/lexer.mll | 2 | ||||
| -rw-r--r-- | frontend/parser.mly | 19 | ||||
| -rw-r--r-- | interpret/interpret.ml | 171 | ||||
| -rw-r--r-- | libs/util.ml | 5 | ||||
| -rw-r--r-- | tests/limitera.scade | 26 |
7 files changed, 203 insertions, 96 deletions
diff --git a/frontend/ast.ml b/frontend/ast.ml index 50fa3f4..cf04166 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -71,13 +71,24 @@ and state = { body : eqn ext list; until : transition list; } -and transition = (expr ext) * (id ext) +and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *) + +and activate_block = { + id : id; + locals : var_def list; + body : eqn ext list; +} +and activate_if = + | AST_activate_body of activate_block + | AST_activate_if of expr ext * activate_if * activate_if +and activate = activate_if * id list and eqn = | AST_assign of (id ext list) * (expr ext) | AST_guarantee of (id ext) * (expr ext) | AST_assume of (id ext) * (expr ext) | AST_automaton of automaton + | AST_activate of activate type node_decl = { name : id; diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index 857e01d..25b1c11 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -157,11 +157,29 @@ let rec print_expr fmt e = Format.fprintf fmt "%a(%a)" print_id i (print_list print_expr ", ") (List.map fst l) + (* equations *) let indent ind = ind^" " -let rec print_eqn ind fmt = function +let rec print_vars ind fmt = function + | [] -> () + | v -> + Format.fprintf fmt "%svar" ind; + List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) v; + Format.fprintf fmt "@\n"; + +and print_var_decl fmt (pr, (i, _), ty) = + Format.fprintf fmt "%s%s: %s" + (if pr then "probe " else "") + i + (string_of_typ ty) + +and print_body ind fmt body = + Format.fprintf fmt "%slet@\n%a%stel@\n" + ind (print_block ind) body ind + +and print_eqn ind fmt = function | AST_assign (l,(e,_)) -> Format.fprintf fmt "%s%a = %a;@\n" ind (print_list print_id_ext ", ") l print_expr e @@ -172,6 +190,22 @@ let rec print_eqn ind fmt = function Format.fprintf fmt "%sguarantee %s: %a;@\n" ind i print_expr e | AST_automaton a -> print_automaton ind fmt a + | AST_activate a -> print_activate ind fmt a + +and print_activate ind fmt (x, r) = + Format.fprintf fmt "%sactivate@\n" ind; + print_activate_if (indent ind) fmt x; + Format.fprintf fmt "%sreturns %a;@\n" ind (print_list print_id ", ") r + +and print_activate_if ind fmt = function + | AST_activate_if((c, _), t, e) -> + Format.fprintf fmt "%sif %a then@\n" ind print_expr c; + print_activate_if (indent ind) fmt t; + Format.fprintf fmt "%selse@\n" ind; + print_activate_if (indent ind) fmt e + | AST_activate_body(b) -> + print_vars ind fmt b.locals; + print_body ind fmt b.body and print_automaton ind fmt (n, sts, r) = Format.fprintf fmt "%sautomaton %s@\n" ind n; @@ -181,17 +215,12 @@ and print_automaton ind fmt (n, sts, r) = and print_state ind fmt (st, _) = Format.fprintf fmt "%s%sstate %s@\n" ind (if st.initial then "initial " else "") st.name; - if st.locals <> [] then begin - Format.fprintf fmt "%svar" ind; - List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) st.locals; - Format.fprintf fmt "@\n"; - end; - Format.fprintf fmt "%slet@\n%a%stel@\n" - ind (print_block ind) st.body ind; + print_vars ind fmt st.locals; + print_body ind fmt st.body; if st.until <> [] then begin Format.fprintf fmt "%suntil@\n" ind; - List.iter (fun ((e, _),(s, _)) -> - Format.fprintf fmt "%sif %a resume %s;@\n" (indent ind) print_expr e s) + List.iter (fun ((e, _),(s, _), reset) -> + Format.fprintf fmt "%sif %a %s %s;@\n" (indent ind) print_expr e (if reset then "restart" else "resume") s) st.until end @@ -200,24 +229,14 @@ and print_block ind fmt b = (* declarations *) -and print_var_decl fmt (pr, (i, _), ty) = - Format.fprintf fmt "%s%s: %s" - (if pr then "probe " else "") - i - (string_of_typ ty) and print_node_decl fmt (d : node_decl) = Format.fprintf fmt "node %s(%a) returns(%a)@\n" d.name (print_list print_var_decl "; ") d.args (print_list print_var_decl "; ") d.ret; - if d.var <> [] then begin - Format.fprintf fmt "var"; - List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) d.var; - Format.fprintf fmt "@\n" - end; - Format.fprintf fmt "let@\n%atel@\n@\n" - (print_block "") d.body + print_vars "" fmt d.var; + print_body "" fmt d.body let print_const_decl fmt (d : const_decl) = Format.fprintf fmt diff --git a/frontend/lexer.mll b/frontend/lexer.mll index 9dc7da3..8a4ef26 100644 --- a/frontend/lexer.mll +++ b/frontend/lexer.mll @@ -26,12 +26,14 @@ "or", OR; "mod", MOD; + "activate", ACTIVATE; "automaton", AUTOMATON; "state", STATE; "initial", INITIAL; "unless", UNLESS; "until", UNTIL; "resume", RESUME; + "restart", RESTART; "true", TRUE; "false", FALSE; diff --git a/frontend/parser.mly b/frontend/parser.mly index fb00478..ec283c3 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -13,7 +13,8 @@ open Util %token VAR LET TEL %token PRE %token ASSUME GUARANTEE -%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME +%token ACTIVATE +%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME RESTART %token LPAREN RPAREN %token LCURLY RCURLY @@ -128,8 +129,19 @@ trans(TT): | { [] } transition: -| IF e=ext(expr) RESUME s=ext(IDENT) { (e, s) } - +| IF e=ext(expr) RESUME s=ext(IDENT) { (e, s, false) } +| IF e=ext(expr) RESTART s=ext(IDENT) { (e, s, true) } + +activate: +| ACTIVATE a=activate_if RETURNS r=separated_list(COMMA, IDENT) { (a, r) } +activate_if: +| IF c=ext(expr) THEN t=activate_if ELSE e=activate_if { AST_activate_if(c, t, e) } +| lv=option(var_decl) b=body +{ AST_activate_body { + id = "activate"^uid(); + locals = (match lv with Some v -> v | None -> []); + body = b; +} } eqn: | i=separated_list(COMMA, ext(IDENT)) EQUAL e=ext(expr) @@ -137,6 +149,7 @@ eqn: | ASSUME i=ext(IDENT) COLON e=ext(expr) { AST_assume(i, e) } | GUARANTEE i=ext(IDENT) COLON e=ext(expr) { AST_guarantee(i, e) } | a=automaton { AST_automaton(a) } +| a=activate { AST_activate(a) } typ: | INT { AST_TINT } diff --git a/interpret/interpret.ml b/interpret/interpret.ml index d141bc6..373ed5f 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -20,18 +20,63 @@ let find_node_decl p id = | AST_node_decl d -> d | _ -> assert false +(* Utility : build subscopes of equation ; extract pre declarations *) + +(* subscopes : + prog -> expr ext -> (id * eqs * (id * expr ext) list) list +*) +let rec subscopes p e = match fst e with + | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> [] + | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> subscopes p e' + | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2) + | AST_arrow(e1, e2) -> + subscopes p e1 @ subscopes p e2 + | AST_if(e1, e2, e3) -> + subscopes p e1 @ subscopes p e2 @ subscopes p e3 + | AST_instance((f, _), args, id) -> + let more = List.flatten (List.map (subscopes p) args) in + let (node, _) = find_node_decl p f in + let args_x = List.map2 (fun id arg -> id, arg) node.args args in + (id, node.body, args_x)::more + +(* extract_pre : expr ext -> (id * expr ext) list *) +let rec extract_pre e = match fst e with + | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> [] + | AST_unary (_, e') | AST_not e' -> extract_pre e' + | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2) + | AST_arrow(e1, e2) -> + extract_pre e1 @ extract_pre e2 + | AST_if(e1, e2, e3) -> + extract_pre e1 @ extract_pre e2 @ extract_pre e3 + | AST_instance((f, _), args, id) -> + List.flatten (List.map extract_pre args) + | AST_pre(e', n) -> + (n, e')::(extract_pre e') + + (* Expression evaluation *) +type eval_env = { + p: prog; + c: calc_map; + scopes: string list; +} + (* - eval_expr : prog -> calc_map -> state -> string -> expr ext -> (state * value) + eval_expr : eval_env -> string -> expr ext -> (state * value) *) -let rec eval_expr p c scope st exp = - let sub_eval = eval_expr p c scope in +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, _) -> - begin try let st, v = get_var st c (scope^"/"^id) in st, [v] - with No_variable _ -> let st, v = get_var st c ("cst/"^id) in st, [v] - end + let rec aux = function + | [] -> + let st, v = get_var st env.c ("cst/"^id) in st, [v] + | sc::q -> + try let st, v = get_var st env.c (sc^"/"^id) in st, [v] + with No_variable _ -> aux q + in aux env.scopes (* on numerical values *) | AST_int_const (i, _) -> st, [VInt (int_of_string i)] | AST_real_const (r, _) -> st, [VReal (float_of_string r)] @@ -111,16 +156,18 @@ let rec eval_expr p c scope st exp = | _ -> type_error "Invalid condition in if." end | AST_instance((f, _), args, nid) -> - let (n, _) = find_node_decl p f in + let (n, _) = find_node_decl env.p f in List.fold_left - (fun (st, vs) (_, (id,_), _) -> let st, v = get_var st c (scope^"/"^nid^"/"^id) in + (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 = - match eval_expr p c "cst" st d.value with + let env = { p = p; c = c; scopes = ["cst"] } in + match eval_expr env st d.value with | st, [v] -> VarMap.add ("cst/"^d.name) v st | _ -> type_error ("Cannot assign tuple to constant" ^ d.name) @@ -140,46 +187,41 @@ let program_consts p = VarMap.empty cdecl -(* Program execution *) - -(* subscopes : - prog -> expr ext -> (id * eqs * (id * expr ext) list) list -*) -let rec subscopes p e = match fst e with - | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> [] - | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> subscopes p e' - | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2) - | AST_arrow(e1, e2) -> - subscopes p e1 @ subscopes p e2 - | AST_if(e1, e2, e3) -> - subscopes p e1 @ subscopes p e2 @ subscopes p e3 - | AST_instance((f, _), args, id) -> - let more = List.flatten (List.map (subscopes p) args) in - let (node, _) = find_node_decl p f in - let args_x = List.map2 (fun id arg -> id, arg) node.args args in - (id, node.body, args_x)::more +(* 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 (subscopes 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 -(* extract_pre : expr ext -> (id * expr ext) list *) -let rec extract_pre e = match fst e with - | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> [] - | AST_unary (_, e') | AST_not e' -> extract_pre e' - | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2) - | AST_arrow(e1, e2) -> - extract_pre e1 @ extract_pre e2 - | AST_if(e1, e2, e3) -> - extract_pre e1 @ extract_pre e2 @ extract_pre e3 - | AST_instance((f, _), args, id) -> - List.flatten (List.map extract_pre args) - | AST_pre(e', n) -> - (n, e')::(extract_pre e') +(* Program execution *) (* build calc map *) -let rec build_prog_ccmap p scope eqs st = +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 st, vals = eval_expr p c scope st e in + 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 @@ -187,15 +229,13 @@ let rec build_prog_ccmap p scope eqs st = 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 (fun _ a b -> match a, b with - | Some x, None -> Some x - | None, Some y -> Some y - | _ -> assert false) c - (build_prog_ccmap p (scope^"/"^ss_id) ss_eqs st) + 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 st, vals = eval_expr p c scope st eq in + 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" @@ -207,15 +247,18 @@ let rec build_prog_ccmap p scope eqs st = List.fold_left add_subscope c (subscopes 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 p scope eqs st ccmap = +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 scope eqs st nst = + 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) @@ -223,13 +266,13 @@ let extract_next_state active p scope eqs st ccmap = in let add_subscopes active = List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) -> - aux active (scope^"/"^ss_id) ss_eqs st nst) + 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) (subscopes p e) in + let st, nst = add_subscopes active (st, nst) (subscopes env.p e) in List.fold_left (fun (st, nst) (pn, pe) -> - let st, v = if active then eval_expr p ccmap scope st 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 -> [] @@ -238,24 +281,11 @@ let extract_next_state active p scope eqs st ccmap = (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 scope eqs st csts + in aux active env.scopes eqs st csts -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 - List.fold_left (fun st eq -> match fst eq with - | AST_assign(_, e) -> add_subscopes st (subscopes p e) - | AST_assume _ | AST_guarantee _ -> st - | AST_automaton _ -> not_implemented "prog_init_state aux automaton") - st eqs - in - aux (program_consts p) p "" n.body let program_step p st inputs root_node = @@ -263,7 +293,7 @@ let program_step p st inputs root_node = 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 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) @@ -271,7 +301,8 @@ let program_step p st inputs root_node = 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 "" n.body st ccmap 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/libs/util.ml b/libs/util.ml index cfa1619..522c3ec 100644 --- a/libs/util.ml +++ b/libs/util.ml @@ -1,6 +1,11 @@ exception TypeError module VarMap = Mapext.Make(String) +exception Duplicate of string +let disjoint_union k a b = match a, b with + | Some x, None -> Some x + | None, Some y -> Some y + | _ -> raise (Duplicate k) let rec fix equal f s = let fs = f s in diff --git a/tests/limitera.scade b/tests/limitera.scade new file mode 100644 index 0000000..1e4927e --- /dev/null +++ b/tests/limitera.scade @@ -0,0 +1,26 @@ +const bound: int = 128; + +node limiter(x: int; d: int) returns (probe y: int) + var s, r: int; + let + assume in_bounded: x >= -bound and x <= bound; + guarantee out_bounded: y >= -bound and y <= bound; + s = 0 -> pre y; + r = x - s; + activate + if r <= -d then + let y = s - d; tel + else if r >= d then + let y = s + d; tel + else + let y = x; tel + returns y; + tel + +node test(i: int) returns(a, b, c: int; exit: bool) + let + exit = i >= 30; + a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random + b = 16; + c = limiter(a, b); + tel |