From 860ad2752ef0544bc6874d895875a78f91db9084 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 17 Jun 2014 09:48:22 +0200 Subject: Add AST for logical formula. --- Makefile | 10 +- abstract/formula.ml | 24 +++ abstract/formula_printer.ml | 56 ++++++ frontend/ast_printer.ml | 3 +- interpret/data.ml | 6 - interpret/interpret.ml | 455 ++++++++++++++++++++++++++++++++++++++++++++ interpret/interpret2.ml | 453 ------------------------------------------- main.ml | 71 ++++--- 8 files changed, 576 insertions(+), 502 deletions(-) create mode 100644 abstract/formula.ml create mode 100644 abstract/formula_printer.ml delete mode 100644 interpret/data.ml create mode 100644 interpret/interpret.ml delete mode 100644 interpret/interpret2.ml diff --git a/Makefile b/Makefile index 62245ae..681b651 100644 --- a/Makefile +++ b/Makefile @@ -1,17 +1,18 @@ .PHONY: clean BIN=analyze -SRCDIRS=libs,frontend,interpret +SRCDIRS=libs,frontend,interpret,abstract SRC= main.ml \ frontend/ast.ml \ frontend/parser.mly \ frontend/lexer.mll \ frontend/ast_printer.ml \ - interpret/data.ml \ + abstract/formula.ml \ + abstract/formula_printer.ml \ interpret/bad_interpret.ml \ interpret/interface.ml \ - interpret/interpret2.ml \ + interpret/interpret.ml \ interpret/rename.ml all: $(BIN) @@ -23,4 +24,5 @@ $(BIN): $(SRC) mv main.native $(BIN) clean: - rm -rf _build + rm $(BIN) + ocamlbuild -clean diff --git a/abstract/formula.ml b/abstract/formula.ml new file mode 100644 index 0000000..389000c --- /dev/null +++ b/abstract/formula.ml @@ -0,0 +1,24 @@ +open Ast + +(* AST for logical formulas *) + +type num_expr = + (* constants *) + | NIntConst of int + | NRealConst of float + (* operators *) + | NBinary of binary_op * num_expr * num_expr + | NUnary of unary_op * num_expr + (* identifier *) + | NIdent of id + +type bool_expr = + (* constants *) + | BConst of bool + (* operators from numeric values to boolean values *) + | BRel of binary_rel_op * num_expr * num_expr + (* boolean operators *) + | BAnd of bool_expr * bool_expr + | BOr of bool_expr * bool_expr + | BNot of bool_expr + diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml new file mode 100644 index 0000000..7e626f0 --- /dev/null +++ b/abstract/formula_printer.ml @@ -0,0 +1,56 @@ +open Formula +open Ast_printer + +let ne_prec = function + | NUnary(op, _) -> unary_precedence + | NBinary(op, _, _) -> binary_op_precedence op + | _ -> 100 + +let be_prec = function + | BRel(op, _, _) -> binary_rel_precedence op + | BAnd _ -> binary_bool_precedence AST_AND + | BOr _ -> binary_bool_precedence AST_OR + | BNot _ -> unary_precedence + | _ -> 100 + + +let print_lh fmt pf fa a fe e = + if fa a < fe e + then Format.fprintf fmt "@[<2>(%a)@]" pf a + else Format.fprintf fmt "%a" pf a +let print_rh fmt pf fb b fe e = + if fb b < fe e + then Format.fprintf fmt "@[<2>(%a)@]" pf b + else Format.fprintf fmt "%a" pf b + +let rec print_num_expr fmt e = match e with + | NIntConst i -> Format.fprintf fmt "%d" i + | NRealConst f -> Format.fprintf fmt "%f" f + | NIdent id -> Format.fprintf fmt "%s" id + | NBinary(op, a, b) -> + print_lh fmt print_num_expr ne_prec a ne_prec e; + Format.fprintf fmt "@ %s@ " (string_of_binary_op op); + print_rh fmt print_num_expr ne_prec b ne_prec e + | NUnary(op, a) -> + Format.pp_print_string fmt (string_of_unary_op op); + print_rh fmt print_num_expr ne_prec a ne_prec e + +let rec print_bool_expr fmt e = match e with + | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false") + | BRel(op, a, b) -> + print_lh fmt print_num_expr ne_prec a be_prec e; + Format.fprintf fmt "@ %s@ " (string_of_binary_rel op); + print_rh fmt print_num_expr ne_prec b be_prec e + | BAnd (a, b) -> + print_lh fmt print_bool_expr be_prec a be_prec e; + Format.fprintf fmt "@ /\\@ "; + print_rh fmt print_bool_expr be_prec b be_prec e + | BOr (a, b) -> + print_lh fmt print_bool_expr be_prec a be_prec e; + Format.fprintf fmt "@ \\/@ "; + print_rh fmt print_bool_expr be_prec b be_prec e + | BNot (a) -> + Format.pp_print_string fmt "!"; + print_rh fmt print_bool_expr be_prec a be_prec e + +let print_expr = print_bool_expr diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index 08f4fb4..b6dcdbc 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -44,6 +44,7 @@ let string_of_binary_bool = function | AST_OR -> "or" +let unary_precedence = 99 let binary_op_precedence = function | AST_MUL| AST_DIV| AST_MOD-> 51 | AST_PLUS | AST_MINUS -> 50 @@ -57,7 +58,7 @@ let arrow_precedence = 20 let if_precedence = 10 let expr_precedence = function - | AST_unary (_, _) | AST_pre(_, _) | AST_not(_) -> 99 + | AST_unary (_, _) | AST_pre(_, _) | AST_not(_) -> unary_precedence | AST_binary(op, _, _) -> binary_op_precedence op | AST_binary_rel(r, _, _) -> binary_rel_precedence r | AST_binary_bool(r, _, _) -> binary_bool_precedence r diff --git a/interpret/data.ml b/interpret/data.ml deleted file mode 100644 index 1d91e93..0000000 --- a/interpret/data.ml +++ /dev/null @@ -1,6 +0,0 @@ -(* Data structures for representing the state of a system *) - -open Util -open Ast -open Ast_util - diff --git a/interpret/interpret.ml b/interpret/interpret.ml new file mode 100644 index 0000000..063dad0 --- /dev/null +++ b/interpret/interpret.ml @@ -0,0 +1,455 @@ +open Ast +open Util +open Ast_util +open Interface + +module I : INTERPRET = struct + + (* Values for variables *) + + exception Bad_datatype + + type value = + | VInt of int + | VBool of bool + | VReal of float + | VState of id + | VPrevious of value list + | VBusy (* intermediate value : calculating ! *) + | VCalc of (unit -> unit) + + let int_value i = VInt i + let bool_value b = VBool b + let real_value r = VReal r + + let as_int = function + | VInt i -> i + | _ -> raise Bad_datatype + let as_bool = function + | VBool b -> b + | _ -> raise Bad_datatype + let as_real = function + | VReal r -> r + | _ -> raise Bad_datatype + + let rec str_repr_of_val = 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_repr_of_val v) + "" p + ^ "]" + | VBusy -> "#" + | VCalc _ -> "()" + + (* States of the interpret *) + + (* path to node * subscope prefix in node * equations in scope *) + type scope = id * id * eqn ext list + + type state = { + p : prog; + root_scope : scope; + outputs : id list; + save : value VarMap.t; + } + + let print_state fmt st = + VarMap.iter + (fun id v -> Format.fprintf fmt "%s = %s@." id (str_repr_of_val v)) + st.save + + type io = (id * value) list + + + (* Internal type env : contains the environment for state calculation *) + type env = { + st : state; + vars : (id, value) Hashtbl.t; + } + + + (* + get_var : env -> id -> id -> value + + Gets the value of a variable relative to a node path. + *) + let rec get_var env node id = + let p = node^"/"^id in + try match Hashtbl.find env.vars p with + | VCalc f -> + Hashtbl.replace env.vars p VBusy; + f (); + get_var env node id + | VBusy -> combinatorial_cycle p + | x -> x + with + | Not_found -> no_variable p + + (* + eval_expr : env -> (id * id) -> expr ext -> value list + *) + let rec eval_expr env (node, prefix) exp = + let sub_eval = eval_expr env (node, prefix) in + match fst exp with + | AST_identifier (id, _) -> + [loc_error (snd exp) (get_var env node) id] + | AST_idconst (id, _) -> + begin try [VarMap.find ("cst/"^id) env.st.save] + with Not_found -> loc_error (snd exp) no_variable id end + (* on numerical values *) + | AST_int_const (i, _) -> [VInt (int_of_string i)] + | AST_real_const (r, _) -> [VReal (float_of_string r)] + | AST_unary(AST_UPLUS, e) -> sub_eval e + | AST_unary(AST_UMINUS, e) -> + begin match sub_eval e with + | [VInt x] -> [VInt (-x)] + | [VReal x] -> [VReal(-. x)] + | _ -> type_error "Unary on non-numerical." + end + | AST_binary(op, e1, e2) -> + let iop, fop = match op with + | AST_PLUS -> (+), (+.) + | AST_MINUS -> (-), (-.) + | AST_MUL -> ( * ), ( *. ) + | AST_DIV -> (/), (/.) + | AST_MOD -> (mod), mod_float + in + begin match sub_eval e1, sub_eval e2 with + | [VInt a], [VInt b] -> [VInt (iop a b)] + | [VReal a], [VReal b] -> [VReal(fop a b)] + | _ -> type_error "Invalid arguments for numerical binary." + end + (* on boolean values *) + | AST_bool_const b -> [VBool b] + | AST_binary_rel(op, e1, e2) -> + let r = match op with + | AST_EQ -> (=) | AST_NE -> (<>) + | AST_LT -> (<) | AST_LE -> (<=) + | AST_GT -> (>) | AST_GE -> (>=) + in + begin match sub_eval e1, sub_eval e2 with + | [VInt a], [VInt b] -> [VBool (r a b)] + | [VReal a], [VReal b] -> [VBool (r a b)] + | [VBool a], [VBool b] -> [VBool (r a b)] + | _ -> type_error "Invalid arguments for binary relation." + end + | AST_binary_bool(op, e1, e2) -> + let r = match op with + | AST_AND -> (&&) | AST_OR -> (||) + in + begin match sub_eval e1, sub_eval e2 with + | [VBool a], [VBool b] -> [VBool (r a b)] + | _ -> type_error "Invalid arguments for boolean relation." + end + | AST_not(e) -> + begin match sub_eval e with + | [VBool b] -> [VBool (not b)] + | _ -> type_error "Invalid arguments for boolean negation." + end + (* temporal primitives *) + | AST_pre(exp, n) -> + begin try match VarMap.find (node^"/"^prefix^n) env.st.save with + | VPrevious x -> x + | _ -> assert false + with Not_found -> [] + end + | AST_arrow(before, after) -> + begin try match VarMap.find (node^"/"^prefix^"init") env.st.save with + | VBool true -> sub_eval before + | VBool false -> sub_eval after + | _ -> assert false + with Not_found -> assert false + end + (* other *) + | AST_if(cond, a, b) -> + begin match sub_eval cond with + | [VBool true] -> sub_eval a + | [VBool false] -> sub_eval b + | _ -> type_error "Invalid condition in if." + end + | AST_instance((f, _), args, nid) -> + let (n, _) = find_node_decl env.st.p f in + List.map + (fun (_, (id, _), _) -> get_var env (node^"/"^nid) id) + n.ret + + (* + reset_scope : env -> scope -> unit + + Sets all the init variables to true, and all the state variables + to initial state. Does this recursively. + The state reset done by this on the environment is only applied on the + next iteration, when the state info has been extracted by extract_st. + *) + let rec reset_scope env (node, prefix, eqs) = + Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true); + let do_exp e = + List.iter + (fun (id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs)) + (extract_instances env.st.p e) + in + let do_eq (e, _) = match e with + | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> do_exp e + | AST_automaton (aid, states, _) -> + let (init_state, _) = List.find (fun (st, _) -> st.initial) states in + Hashtbl.replace env.vars (node^"/"^aid^".state") (VState init_state.st_name); + List.iter + (fun (st, _) -> reset_scope env (node, aid^"."^st.st_name^".", st.body)) + states + | AST_activate (x, _) -> + let rec aux = function + | AST_activate_if (_, a, b) -> aux a; aux b + | AST_activate_body b -> + reset_scope env (node, b.act_id^".", b.body) + in aux x + in + List.iter do_eq eqs + + (* + activate_scope : env -> scope -> unit + + Adds functions for calculating the variables in this scope. + For assign : simple ! + For automaton : lazily select+activate automaton state (would enable + implementation of strong transitions) + For activate : lazily select+activate active block + *) + let rec activate_scope env (node, prefix, eqs) = + Hashtbl.replace env.vars (node^"/"^prefix^"act") (VBool true); + let do_expr e = + List.iter + (fun (id, eqs, args) -> + activate_scope env (node^"/"^id, "", eqs); + let do_arg ((_,(name,_),_), expr) = + let apath = node^"/"^id^"/"^name in + let calc () = + match eval_expr env (node, prefix) expr with + | [v] -> Hashtbl.replace env.vars apath v + | _ -> loc_error (snd expr) error "Unsupported arity for argument." + in + Hashtbl.replace env.vars apath (VCalc calc) + in + List.iter do_arg args) + (extract_instances env.st.p e) + in + let do_eq (e, _) = match e with + | AST_assign(vars, e) -> + do_expr e; + let calc () = + let vals = eval_expr env (node, prefix) e in + List.iter2 (fun (id, _) v -> + Hashtbl.replace env.vars (node^"/"^id) v) vars vals + in + List.iter + (fun (id, _) -> + Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc))) + vars + | AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e + | AST_activate(t, vars) -> + let rec do_tree = function + | AST_activate_body _ -> () + | AST_activate_if(c, a, b) -> + do_expr c; do_tree a; do_tree b + in do_tree t; + let rec needed x () = match x with + | AST_activate_body b -> + activate_scope env (node, b.act_id^".", b.body) + | AST_activate_if (c, t, f) -> + begin match eval_expr env (node, prefix) c with + | [VBool true] -> needed t () + | [VBool false] -> needed f () + | _ -> error "Invalid value in activate if condition." + end + in + List.iter (fun id -> + Hashtbl.replace env.vars (node^"/"^id) (VCalc (needed t))) + vars + | AST_automaton(aid, states, vars) -> + let asn = match VarMap.find (node^"/"^aid^".state") env.st.save with + | VState s -> s + | _ -> assert false + in + let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in + activate_scope env (node, aid^"."^st.st_name^".", st.body); + List.iter (fun (c, _, _) -> do_expr c) st.until + in + List.iter do_eq eqs + + (* + is_scope_active : env -> scope -> bool + *) + let is_scope_active env (node, prefix, _) = + try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"act")) + with Not_found -> false + + (* + do_weak_transitions : env -> scope -> unit + *) + let rec do_weak_transitions env (node, prefix, eqs) = + let do_expr e = + List.iter + (fun (id, eqs, args) -> + do_weak_transitions env (node^"/"^id, "", eqs)) + (extract_instances env.st.p e) + in + let do_eq (e, _) = match e with + | AST_assign(_, e) -> do_expr e + | AST_assume (_, e) | AST_guarantee (_, e) -> do_expr e + | AST_activate(t, _) -> + let rec do_tree = function + | AST_activate_body b -> do_weak_transitions env (node, b.act_id^".", b.body) + | AST_activate_if(c, a, b) -> + do_expr c; do_tree a; do_tree b + in do_tree t + | AST_automaton(aid, states, vars) -> + let svn = node^"/"^aid^".state" in + let stv = VarMap.find svn env.st.save in + let new_st = + if is_scope_active env (node, prefix, eqs) then begin + let asn = match stv with + | VState s -> s + | _ -> assert false + in + let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in + try + let (_, (next_st,_), rst) = List.find + (fun (c, _, _) -> eval_expr env (node, aid^"."^st.st_name^".") c = [VBool true]) + st.until + in + if rst then begin + let (st, _) = List.find (fun (st, _) -> st.st_name = next_st) states in + reset_scope env (node, aid^"."^next_st^".", st.body) + end; + VState(next_st) + with + | _ -> stv + end else + stv + in + Hashtbl.replace env.vars svn new_st + in + List.iter do_eq eqs + + (* + extract_st : env -> state + *) + let extract_st env = + let rec aux (node, prefix, eqs) save = + + let init = + try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init")) + with Not_found -> + let pre_init = as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save) + in pre_init && (not (is_scope_active env (node, prefix, eqs))) + in + let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in + + let save_expr save e = + (* Save pre expressions *) + let save = List.fold_left + (fun save (id, expr) -> + let n = node^"/"^prefix^id in + if is_scope_active env (node, prefix, eqs) then + VarMap.add + n + (VPrevious (eval_expr env (node, prefix) expr)) + save + else + try VarMap.add n + (VarMap.find n env.st.save) + save + with Not_found -> save + ) + save (extract_pre e) in + (* Save recursively in sub instances of nodes *) + let save = List.fold_left + (fun save (n, eqs, _) -> + aux (node^"/"^n, "", eqs) save) + save (extract_instances env.st.p e) + in save + in + let save_eq save eq = match fst eq with + | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> + save_expr save e + | AST_automaton(aid, states, _) -> + let svn = node^"/"^aid^".state" in + let st = Hashtbl.find env.vars svn in + let save = VarMap.add (node^"/"^aid^".state") st save in + List.fold_left (fun save (st, _) -> + let save = + List.fold_left (fun save (c, _, _) -> save_expr save c) save st.until in + aux (node, aid^"."^st.st_name^".", st.body) save) + save states + | AST_activate(r, _) -> + let rec do_t save = function + | AST_activate_if(c, t, f) -> + let save = save_expr save c in + let save = do_t save t in + do_t save f + | AST_activate_body b -> + aux (node, b.act_id^".", b.body) save + in + do_t save r + in + List.fold_left save_eq save eqs + + in + let consts = VarMap.filter (fun k _ -> k.[0] <> '/') env.st.save in + { env.st with save = aux env.st.root_scope consts } + + (* + init_state : prog -> id -> state + *) + let init_state p root = + let (n, _) = find_node_decl p root in + let root_scope = ("", "", n.body) in + + let st = { + p = p; + root_scope = root_scope; + save = VarMap.empty; + outputs = (List.map (fun (_,(n,_),_) -> n) n.ret); + } in + + let env = { st = st; vars = Hashtbl.create 42 } in + + (* calculate constants *) + List.iter (function + | AST_const_decl(d, l) -> + let cpath = "cst/" ^ d.c_name in + Hashtbl.replace env.vars cpath (VCalc (fun () -> + match eval_expr env ("cst", "") d.value with + | [v] -> Hashtbl.replace env.vars cpath v + | _ -> loc_error l error "Arity error in constant expression.")) + | _ -> ()) + p; + List.iter (function + | AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name) + | _ -> ()) + p; + + reset_scope env root_scope; + { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty } + + (* + step : state -> io -> (state * io) + *) + let step st i = + let vars = Hashtbl.create 10 in + List.iter (fun (k, v) -> Hashtbl.replace vars ("/"^k) v) i; + let env = { st = st; vars = vars } in + + activate_scope env st.root_scope; + if false then + Hashtbl.iter (fun k v -> Format.printf "%s : %s@." k (str_repr_of_val v)) env.vars; + let out = List.map (fun id -> id, get_var env "" id) st.outputs in + do_weak_transitions env st.root_scope; + extract_st env, out + + +end diff --git a/interpret/interpret2.ml b/interpret/interpret2.ml deleted file mode 100644 index d6f7731..0000000 --- a/interpret/interpret2.ml +++ /dev/null @@ -1,453 +0,0 @@ -open Ast -open Util -open Ast_util -open Interface - -module I : INTERPRET = struct - - (* Values for variables *) - - exception Bad_datatype - - type value = - | VInt of int - | VBool of bool - | VReal of float - | VState of id - | VPrevious of value list - | VBusy (* intermediate value : calculating ! *) - | VCalc of (unit -> unit) - - let int_value i = VInt i - let bool_value b = VBool b - let real_value r = VReal r - - let as_int = function - | VInt i -> i - | _ -> raise Bad_datatype - let as_bool = function - | VBool b -> b - | _ -> raise Bad_datatype - let as_real = function - | VReal r -> r - | _ -> raise Bad_datatype - - let rec str_repr_of_val = 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_repr_of_val v) - "" p - ^ "]" - | VBusy -> "#" - | VCalc _ -> "()" - - (* States of the interpret *) - - (* path to node * subscope prefix in node * equations in scope *) - type scope = id * id * eqn ext list - - type state = { - p : prog; - root_scope : scope; - outputs : id list; - save : value VarMap.t; - } - - let print_state fmt st = - VarMap.iter - (fun id v -> Format.fprintf fmt "%s = %s@." id (str_repr_of_val v)) - st.save - - type io = (id * value) list - - - (* Internal type env : contains the environment for state calculation *) - type env = { - st : state; - vars : (id, value) Hashtbl.t; - } - - - (* - get_var : env -> id -> id -> value - - Gets the value of a variable relative to a node path. - *) - let rec get_var env node id = - let p = node^"/"^id in - try match Hashtbl.find env.vars p with - | VCalc f -> - Hashtbl.replace env.vars p VBusy; - f (); - get_var env node id - | VBusy -> combinatorial_cycle p - | x -> x - with - | Not_found -> no_variable p - - (* - eval_expr : env -> (id * id) -> expr ext -> value list - *) - let rec eval_expr env (node, prefix) exp = - let sub_eval = eval_expr env (node, prefix) in - match fst exp with - | AST_identifier (id, _) -> - [loc_error (snd exp) (get_var env node) id] - | AST_idconst (id, _) -> - begin try [VarMap.find ("cst/"^id) env.st.save] - with Not_found -> loc_error (snd exp) no_variable id end - (* on numerical values *) - | AST_int_const (i, _) -> [VInt (int_of_string i)] - | AST_real_const (r, _) -> [VReal (float_of_string r)] - | AST_unary(AST_UPLUS, e) -> sub_eval e - | AST_unary(AST_UMINUS, e) -> - begin match sub_eval e with - | [VInt x] -> [VInt (-x)] - | [VReal x] -> [VReal(-. x)] - | _ -> type_error "Unary on non-numerical." - end - | AST_binary(op, e1, e2) -> - let iop, fop = match op with - | AST_PLUS -> (+), (+.) - | AST_MINUS -> (-), (-.) - | AST_MUL -> ( * ), ( *. ) - | AST_DIV -> (/), (/.) - | AST_MOD -> (mod), mod_float - in - begin match sub_eval e1, sub_eval e2 with - | [VInt a], [VInt b] -> [VInt (iop a b)] - | [VReal a], [VReal b] -> [VReal(fop a b)] - | _ -> type_error "Invalid arguments for numerical binary." - end - (* on boolean values *) - | AST_bool_const b -> [VBool b] - | AST_binary_rel(op, e1, e2) -> - let r = match op with - | AST_EQ -> (=) | AST_NE -> (<>) - | AST_LT -> (<) | AST_LE -> (<=) - | AST_GT -> (>) | AST_GE -> (>=) - in - begin match sub_eval e1, sub_eval e2 with - | [VInt a], [VInt b] -> [VBool (r a b)] - | [VReal a], [VReal b] -> [VBool (r a b)] - | [VBool a], [VBool b] -> [VBool (r a b)] - | _ -> type_error "Invalid arguments for binary relation." - end - | AST_binary_bool(op, e1, e2) -> - let r = match op with - | AST_AND -> (&&) | AST_OR -> (||) - in - begin match sub_eval e1, sub_eval e2 with - | [VBool a], [VBool b] -> [VBool (r a b)] - | _ -> type_error "Invalid arguments for boolean relation." - end - | AST_not(e) -> - begin match sub_eval e with - | [VBool b] -> [VBool (not b)] - | _ -> type_error "Invalid arguments for boolean negation." - end - (* temporal primitives *) - | AST_pre(exp, n) -> - begin try match VarMap.find (node^"/"^prefix^n) env.st.save with - | VPrevious x -> x - | _ -> assert false - with Not_found -> [] - end - | AST_arrow(before, after) -> - begin try match VarMap.find (node^"/"^prefix^"init") env.st.save with - | VBool true -> sub_eval before - | VBool false -> sub_eval after - | _ -> assert false - with Not_found -> assert false - end - (* other *) - | AST_if(cond, a, b) -> - begin match sub_eval cond with - | [VBool true] -> sub_eval a - | [VBool false] -> sub_eval b - | _ -> type_error "Invalid condition in if." - end - | AST_instance((f, _), args, nid) -> - let (n, _) = find_node_decl env.st.p f in - List.map - (fun (_, (id, _), _) -> get_var env (node^"/"^nid) id) - n.ret - - (* - reset_scope : env -> scope -> unit - - Sets all the init variables to true, and all the state variables - to initial state. Does this recursively. - The state reset done by this on the environment is only applied on the - next iteration, when the state info has been extracted by extract_st. - *) - let rec reset_scope env (node, prefix, eqs) = - Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true); - let do_exp e = - List.iter - (fun (id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs)) - (extract_instances env.st.p e) - in - let do_eq (e, _) = match e with - | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> do_exp e - | AST_automaton (aid, states, _) -> - let (init_state, _) = List.find (fun (st, _) -> st.initial) states in - Hashtbl.replace env.vars (node^"/"^aid^".state") (VState init_state.st_name); - List.iter - (fun (st, _) -> reset_scope env (node, aid^"."^st.st_name^".", st.body)) - states - | AST_activate (x, _) -> - let rec aux = function - | AST_activate_if (_, a, b) -> aux a; aux b - | AST_activate_body b -> - reset_scope env (node, b.act_id^".", b.body) - in aux x - in - List.iter do_eq eqs - - (* - activate_scope : env -> scope -> unit - - Adds functions for calculating the variables in this scope. - For assign : simple ! - For automaton : lazily select+activate automaton state (would enable - implementation of strong transitions) - For activate : lazily select+activate active block - *) - let rec activate_scope env (node, prefix, eqs) = - Hashtbl.replace env.vars (node^"/"^prefix^"act") (VBool true); - let do_expr e = - List.iter - (fun (id, eqs, args) -> - activate_scope env (node^"/"^id, "", eqs); - let do_arg ((_,(name,_),_), expr) = - let apath = node^"/"^id^"/"^name in - let calc () = - match eval_expr env (node, prefix) expr with - | [v] -> Hashtbl.replace env.vars apath v - | _ -> loc_error (snd expr) error "Unsupported arity for argument." - in - Hashtbl.replace env.vars apath (VCalc calc) - in - List.iter do_arg args) - (extract_instances env.st.p e) - in - let do_eq (e, _) = match e with - | AST_assign(vars, e) -> - do_expr e; - let calc () = - let vals = eval_expr env (node, prefix) e in - List.iter2 (fun (id, _) v -> - Hashtbl.replace env.vars (node^"/"^id) v) vars vals - in - List.iter - (fun (id, _) -> - Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc))) - vars - | AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e - | AST_activate(t, vars) -> - let rec do_tree = function - | AST_activate_body _ -> () - | AST_activate_if(c, a, b) -> - do_expr c; do_tree a; do_tree b - in do_tree t; - let rec needed x () = match x with - | AST_activate_body b -> - activate_scope env (node, b.act_id^".", b.body) - | AST_activate_if (c, t, f) -> - begin match eval_expr env (node, prefix) c with - | [VBool true] -> needed t () - | [VBool false] -> needed f () - | _ -> error "Invalid value in activate if condition." - end - in - List.iter (fun id -> - Hashtbl.replace env.vars (node^"/"^id) (VCalc (needed t))) - vars - | AST_automaton(aid, states, vars) -> - let asn = match VarMap.find (node^"/"^aid^".state") env.st.save with - | VState s -> s - | _ -> assert false - in - let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in - activate_scope env (node, aid^"."^st.st_name^".", st.body); - List.iter (fun (c, _, _) -> do_expr c) st.until - in - List.iter do_eq eqs - - (* - is_scope_active : env -> scope -> bool - *) - let is_scope_active env (node, prefix, _) = - try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"act")) - with Not_found -> false - - (* - do_weak_transitions : env -> scope -> unit - *) - let rec do_weak_transitions env (node, prefix, eqs) = - let do_expr e = - List.iter - (fun (id, eqs, args) -> - do_weak_transitions env (node^"/"^id, "", eqs)) - (extract_instances env.st.p e) - in - let do_eq (e, _) = match e with - | AST_assign(_, e) -> do_expr e - | AST_assume (_, e) | AST_guarantee (_, e) -> do_expr e - | AST_activate(t, _) -> - let rec do_tree = function - | AST_activate_body b -> do_weak_transitions env (node, b.act_id^".", b.body) - | AST_activate_if(c, a, b) -> - do_expr c; do_tree a; do_tree b - in do_tree t - | AST_automaton(aid, states, vars) -> - let svn = node^"/"^aid^".state" in - let stv = VarMap.find svn env.st.save in - let new_st = - if is_scope_active env (node, prefix, eqs) then begin - let asn = match stv with - | VState s -> s - | _ -> assert false - in - let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in - try - let (_, (next_st,_), rst) = List.find - (fun (c, _, _) -> eval_expr env (node, aid^"."^st.st_name^".") c = [VBool true]) - st.until - in - if rst then begin - let (st, _) = List.find (fun (st, _) -> st.st_name = next_st) states in - reset_scope env (node, aid^"."^next_st^".", st.body) - end; - VState(next_st) - with - | _ -> stv - end else - stv - in - Hashtbl.replace env.vars svn new_st - in - List.iter do_eq eqs - - (* - extract_st : env -> state - *) - let extract_st env = - let rec aux (node, prefix, eqs) save = - - let init = - try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init")) - with Not_found -> - let pre_init = as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save) - in pre_init && (not (is_scope_active env (node, prefix, eqs))) - in - let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in - - let save_expr save e = - let save = List.fold_left - (fun save (id, expr) -> - let n = node^"/"^prefix^id in - if is_scope_active env (node, prefix, eqs) then - VarMap.add - n - (VPrevious (eval_expr env (node, prefix) expr)) - save - else - try VarMap.add n - (VarMap.find n env.st.save) - save - with Not_found -> save - ) - save (extract_pre e) in - let save = List.fold_left - (fun save (n, eqs, _) -> - aux (node^"/"^n, "", eqs) save) - save (extract_instances env.st.p e) - in save - in - let save_eq save eq = match fst eq with - | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> - save_expr save e - | AST_automaton(aid, states, _) -> - let svn = node^"/"^aid^".state" in - let st = Hashtbl.find env.vars svn in - let save = VarMap.add (node^"/"^aid^".state") st save in - List.fold_left (fun save (st, _) -> - let save = - List.fold_left (fun save (c, _, _) -> save_expr save c) save st.until in - aux (node, aid^"."^st.st_name^".", st.body) save) - save states - | AST_activate(r, _) -> - let rec do_t save = function - | AST_activate_if(c, t, f) -> - let save = save_expr save c in - let save = do_t save t in - do_t save f - | AST_activate_body b -> - aux (node, b.act_id^".", b.body) save - in - do_t save r - in - List.fold_left save_eq save eqs - - in - let consts = VarMap.filter (fun k _ -> k.[0] <> '/') env.st.save in - { env.st with save = aux env.st.root_scope consts } - - (* - init_state : prog -> id -> state - *) - let init_state p root = - let (n, _) = find_node_decl p root in - let root_scope = ("", "", n.body) in - - let st = { - p = p; - root_scope = root_scope; - save = VarMap.empty; - outputs = (List.map (fun (_,(n,_),_) -> n) n.ret); - } in - - let env = { st = st; vars = Hashtbl.create 42 } in - - (* calculate constants *) - List.iter (function - | AST_const_decl(d, l) -> - let cpath = "cst/" ^ d.c_name in - Hashtbl.replace env.vars cpath (VCalc (fun () -> - match eval_expr env ("cst", "") d.value with - | [v] -> Hashtbl.replace env.vars cpath v - | _ -> loc_error l error "Arity error in constant expression.")) - | _ -> ()) - p; - List.iter (function - | AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name) - | _ -> ()) - p; - - reset_scope env root_scope; - { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty } - - (* - step : state -> io -> (state * io) - *) - let step st i = - let vars = Hashtbl.create 10 in - List.iter (fun (k, v) -> Hashtbl.replace vars ("/"^k) v) i; - let env = { st = st; vars = vars } in - - activate_scope env st.root_scope; - if false then - Hashtbl.iter (fun k v -> Format.printf "%s : %s@." k (str_repr_of_val v)) env.vars; - let out = List.map (fun id -> id, get_var env "" id) st.outputs in - do_weak_transitions env st.root_scope; - extract_st env, out - - -end diff --git a/main.ml b/main.ml index bd67cb4..61755e3 100644 --- a/main.ml +++ b/main.ml @@ -1,6 +1,6 @@ open Ast -module Interpret = Interpret2.I +module Interpret = Interpret.I (* command line options *) let dump = ref false @@ -18,6 +18,36 @@ let options = [ "--test", Arg.Set test, "Simple testing."; ] +let do_test_interpret prog verbose = + let s0 = Interpret.init_state prog "test" in + if verbose then begin + Format.printf "Init state:@."; + Interpret.print_state Format.std_formatter s0; + end; + let rec it i st = + let next_st, out = + Interpret.step st + ["i", Interpret.int_value i] + in + if verbose then begin + Format.printf "@.> Step %d:@." i; + Interpret.print_state Format.std_formatter st; + Format.printf "Outputs:@."; + List.iter + (fun (k, v) -> Format.printf "%s = %s@." + k (Interpret.str_repr_of_val v)) + out; + end else begin + Format.printf "%d. %s %s %s@." i + (Interpret.str_repr_of_val (List.assoc "a" out)) + (Interpret.str_repr_of_val (List.assoc "b" out)) + (Interpret.str_repr_of_val (List.assoc "c" out)); + end; + if not (Interpret.as_bool (List.assoc "exit" out)) then + it (i+1) next_st + in + it 0 s0 + let () = Arg.parse options (fun f -> ifile := f) usage; @@ -33,44 +63,9 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !vtest then begin - let s0 = Interpret.init_state prog "test" in - Format.printf "Init state:@."; - Interpret.print_state Format.std_formatter s0; - let rec it i st = - let next_st, out = - Interpret.step st - ["i", Interpret.int_value i] - in - Format.printf "@.> Step %d:@." i; - Interpret.print_state Format.std_formatter st; - Format.printf "Outputs:@."; - List.iter - (fun (k, v) -> Format.printf "%s = %s@." - k (Interpret.str_repr_of_val v)) - out; - if not (Interpret.as_bool (List.assoc "exit" out)) then - it (i+1) next_st - in - it 0 s0 - end; + if !vtest then do_test_interpret prog true + else if !test then do_test_interpret prog false; - if !test then begin - let s0 = Interpret.init_state prog "test" in - let rec it i st = - let next_st, outputs = - Interpret.step st - ["i", Interpret.int_value i] - in - Format.printf "%d. %s %s %s@." i - (Interpret.str_repr_of_val (List.assoc "a" outputs)) - (Interpret.str_repr_of_val (List.assoc "b" outputs)) - (Interpret.str_repr_of_val (List.assoc "c" outputs)); - if not (Interpret.as_bool (List.assoc "exit" outputs)) then - it (i+1) next_st - in - it 0 s0 - end with | Util.NoLocError e -> Format.eprintf "Error: %s@." e | Util.LocError(l, e) -> -- cgit v1.2.3