open Ast open Util open Ast_util open Formula open Typing open Interpret (* used for constant evaluation ! *) (* Transform SCADE program to logical formula. Convention : to access the last value of a variable, access the variable with the same name prefixed by "L". A pre-processing pass will extract the variables that are referenced in such a way so that they are taken into account when calculating the memory. *) (* node * prefix * equations *) type scope = id * id * eqn ext list type transform_data = { rp : rooted_prog; consts : I.value VarMap.t; (* future : the automata state *) } (* Numerical types / Enumerated types *) type ne_expr = | EE of enum_expr | NE of num_expr * bool (* bool: true -> real, false -> int *) (* f_of_neexpr : transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr *) let rec f_of_neexpr td (node, prefix, clock_scope) where expr = let sub = f_of_neexpr td (node, prefix, clock_scope) in let le = loc_error (snd expr) in match fst expr with (* ident *) | AST_identifier(id, _) -> let qid = node^"/"^id in begin match type_var td.rp node id with | TInt -> where [NE (NIdent qid, false)] | TReal -> where [NE (NIdent qid, true)] | TEnum _ -> where [EE (EIdent qid)] end | AST_idconst(id, _) -> begin let x = VarMap.find ("cst/"^id) td.consts in try where [NE (NIntConst (I.as_int x), false)] with _ -> try where [NE (NRealConst (I.as_real x), true)] with _ -> try where [EE (EItem (if I.as_bool x then bool_true else bool_false))] with _ -> le error "Invalid data for supposedly numerical/boolean constant." end (* numerical *) | AST_int_const(i, _) -> where [NE(NIntConst(int_of_string i), false)] | AST_real_const(r, _) -> where [NE(NRealConst(float_of_string r), true)] | AST_bool_const b -> where [EE(EItem (if b then bool_true else bool_false))] | AST_unary(op, e) -> sub (function | [NE (x, r)] -> where [NE(NUnary(op, x, r), r)] | _ -> le invalid_arity "Unary operator") e | AST_binary(op, a, b) -> sub (function | [NE (x, r1); NE (y, r2)] -> let r = r1 || r2 in where [NE(NBinary(op, x, y, r), r)] | _ -> le invalid_arity "binary operator") (AST_tuple([a; b]), snd expr) | AST_cast(e, ty) -> let is_real = (ty = AST_TREAL) in sub (function | [NE (x, _)] -> where [NE(NUnary(AST_UPLUS, x, is_real), is_real)] | _ -> le invalid_arity "Cast.") e (* temporal *) | AST_pre(expr, id) -> let id = node^"/"^id in let typ = type_expr td.rp node expr in where (List.mapi (fun i t -> let x = "L"^id^"."^(string_of_int i) in match t with | TInt -> NE(NIdent x, false) | TReal -> NE(NIdent x, true) | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> if td.rp.init_scope clock_scope then f_or (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)) (sub where a)) (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false)) (sub where b)) else if not (td.rp.no_time_scope clock_scope) then f_or (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)) (sub where a)) (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)) (sub where b)) else f_or (sub where a) (sub where b) (* other *) | AST_if(c, a, b) -> f_or (f_and (f_of_expr td (node, prefix, clock_scope) c) (sub where a)) (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (sub where b)) | AST_instance ((f, _), args, nid) -> let (n, _) = find_node_decl td.rp.p f in where (List.map (fun (_, id, t) -> let x = node^"/"^nid^"/"^id in match t with | AST_TINT -> NE(NIdent x, false) | AST_TREAL -> NE(NIdent x, true) | _ -> EE(EIdent x)) n.ret) | AST_tuple l -> let rec rl l x = match l with | [] -> where x | p::q -> sub (fun y -> rl q (x@y)) p in rl l [] (* boolean values treated as enumerated types *) | _ when type_expr td.rp node expr = [bool_type] -> f_or (f_and (f_of_expr td (node, prefix, clock_scope) expr) (where [EE (EItem bool_true)])) (f_and (f_of_expr td (node, prefix, clock_scope) (AST_not(expr), snd expr)) (where [EE (EItem bool_false)])) | _ -> le type_error "Expected numerical/enumerated value" (* f_of_expr : transform_data -> (string, string) -> expr -> bool_expr f_of_bexpr : transform_data -> (string, string) -> (bool_expr -> bool_expr) -> expr -> bool_expr *) and f_of_bexpr td (node, prefix, clock_scope) where expr = let sub = f_of_bexpr td (node, prefix, clock_scope) in let sub_id = sub (fun x -> x) in match fst expr with | AST_bool_const b -> where (BConst b) | AST_binary_bool(AST_AND, a, b) -> where (f_and (sub_id a) (sub_id b)) | AST_binary_bool(AST_OR, a, b) -> where (f_or (sub_id a) (sub_id b)) | AST_not(a) -> where (BNot (sub_id a)) | AST_binary_rel(rel, a, b) -> where (f_of_neexpr td (node, prefix, clock_scope) (function | [NE (x, r1); NE (y, r2)] -> BRel(rel, x, y, r1 || r2) | [EE x; EE y] -> let eop = match rel with | AST_EQ -> E_EQ | AST_NE -> E_NE | _ -> type_error "Invalid operator on enumerated values." in f_e_op eop x y | _ -> invalid_arity "Binary operator") (AST_tuple [a; b], snd expr)) (* Temporal *) | AST_arrow(a, b) -> if td.rp.init_scope clock_scope then f_or (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)) (sub where a)) (f_and (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_false)) (sub where b)) else if not (td.rp.no_time_scope clock_scope) then f_or (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)) (sub where a)) (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)) (sub where b)) else f_or (sub where a) (sub where b) (* Enumerations... *) | _ when type_expr td.rp node expr = [bool_type] -> let ff = function | [EE x] -> where (f_e_eq x (EItem bool_true)) | _ -> assert false in f_of_neexpr td (node, prefix, clock_scope) ff expr | _ -> type_error "Expected boolean value." and f_of_expr td (node, prefix, clock_scope) expr = f_of_bexpr td (node, prefix, clock_scope) (fun x -> x) expr (* Translate program into one big formula *) let reset_cond rst_exprs = List.fold_left f_or (BConst false) rst_exprs let no_reset_cond rst_exprs = List.fold_left (fun ff c -> f_and ff (BNot c)) (BConst true) rst_exprs let clock_scope_here (node, prefix, _) = node^"/"^prefix let gen_clock td (node, prefix, _) active rst_exprs = let clock_scope = node^"/"^prefix in let clock_eq = f_or (f_and (reset_cond rst_exprs) (f_and (if not (td.rp.no_time_scope clock_scope) then BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false) else BConst true) (if td.rp.init_scope clock_scope then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_true) else BConst true))) (f_and (no_reset_cond rst_exprs) (if active then f_and (if not (td.rp.no_time_scope clock_scope) then BRel(AST_EQ, NIdent(clock_scope^"time"), NBinary(AST_PLUS, NIntConst 1, NIdent("L"^clock_scope^"time"), false), false) else BConst true) (if td.rp.init_scope clock_scope then f_e_eq (EIdent(clock_scope^"init")) (EItem bool_false) else BConst true) else f_and (if not (td.rp.no_time_scope clock_scope) then BRel(AST_EQ, NIdent(clock_scope^"time"), NIdent("L"^clock_scope^"time"), false) else BConst true) (if td.rp.init_scope clock_scope then f_e_eq (EIdent(clock_scope^"init")) (EIdent ("L"^clock_scope^"init")) else BConst true))) in (clock_scope, rst_exprs), clock_eq let rec f_of_scope active td (node, prefix, eqs) (clock_scope, rst_exprs as cs) assume_guarantees = let expr_eq e = let instance_eq (_, id, eqs, args) = let eq = f_of_scope active td (node^"/"^id, "", eqs) cs assume_guarantees in if active then let arg_eq ((_,argname,ty), expr) = f_of_neexpr td (node, prefix, clock_scope) (function | [NE (v, r)] -> let need_r = (ty = AST_TREAL) in if r <> need_r then error "Invalid type for numerical argument."; BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v, r) | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v | _ -> invalid_arity "in argument") expr in f_and eq (f_and_list (List.map arg_eq args)) else eq in let eq_i = f_and_list (List.map instance_eq (extract_instances td.rp.p e)) in let pre_expr (id, expr) = let id = node^"/"^id in if active then f_of_neexpr td (node, prefix, clock_scope) (fun elist -> list_fold_op f_and (List.mapi (fun i v -> let x = (id^"."^(string_of_int i)) in match v with | NE (v, r) -> BRel(AST_EQ, NIdent x, v, r) | EE v -> f_e_eq (EIdent x) v) elist)) expr else let typ = type_expr td.rp node expr in list_fold_op f_and (List.mapi (fun i t -> let id_x = id ^ "." ^ string_of_int i in match t with | TInt -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), false) | TReal -> BRel(AST_EQ, NIdent(id_x), NIdent ("L"^id_x), true) | TEnum _ -> f_e_eq (EIdent(id_x)) (EIdent ("L"^id_x))) typ) in let eq_p = f_and_list (List.map pre_expr (extract_pre e)) in f_and eq_i eq_p in let do_eq eq = match fst eq with | AST_assign(ids, e) -> let assign_eq = if active then let apply_f vs = let rels = List.map2 (fun (id, _) -> let need_r = (type_var td.rp node id = TReal) in function | NE (v, r) -> if r <> need_r then error "Invalid type in numerical assign"; BRel(AST_EQ, NIdent (node^"/"^id), v, r) | EE v -> f_e_eq (EIdent (node^"/"^id)) v) ids vs in f_and_list rels in f_of_neexpr td (node, prefix, clock_scope) apply_f e else BConst true in f_and (expr_eq e) assign_eq | AST_assume (_, e) -> let assume_eq = if active then f_of_expr td (node, prefix, clock_scope) e else BConst true in f_and (expr_eq e) assume_eq | AST_guarantee ((id, _), e) -> let gn = node^"/g_"^id in let guarantee_eq = if active && assume_guarantees then f_and (f_of_expr td (node, prefix, clock_scope) e) (BEnumCons(E_EQ, gn, EItem bool_true)) else f_or (f_and (f_of_expr td (node, prefix, clock_scope) e) (BEnumCons(E_EQ, gn, EItem bool_true))) (f_and (BNot (f_of_expr td (node, prefix, clock_scope) e)) (BEnumCons(E_EQ, gn, EItem bool_false))) in f_and (expr_eq e) guarantee_eq | AST_activate (b, _) -> let rec cond_eq = function | AST_activate_body b -> BConst true | AST_activate_if(c, a, b) -> f_and (expr_eq c) (f_and (cond_eq a) (cond_eq b)) in let rec do_tree_act = function | AST_activate_body b -> let b_scope = node, b.act_id^".", b.body in let cs2, clock_eq = gen_clock td b_scope true rst_exprs in f_and clock_eq (f_of_scope true td b_scope cs2 assume_guarantees) | AST_activate_if(c, a, b) -> f_or (f_and (f_of_expr td (node, prefix, clock_scope) c) (f_and (do_tree_act a) (do_tree_inact b))) (f_and (BNot(f_of_expr td (node, prefix, clock_scope) c)) (f_and (do_tree_act b) (do_tree_inact a))) and do_tree_inact = function | AST_activate_body b -> let b_scope = node, b.act_id^".", b.body in let cs2, clock_eq = gen_clock td b_scope false rst_exprs in f_and clock_eq (f_of_scope false td b_scope cs2 assume_guarantees) | AST_activate_if(_, a, b) -> f_and (do_tree_inact a) (do_tree_inact b) in f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b) | AST_automaton (aid, states, _) -> let (init_st, _) = List.find (fun (st, _) -> st.initial) states in let lnstv = "L"^node^"/"^aid^".next_state" in let nstv = node^"/"^aid^".next_state" in let stv = node^"/"^aid^".state" in let st_choice_eq = f_or (f_and (reset_cond rst_exprs) (f_e_eq (EIdent stv) (EItem init_st.st_name))) (f_and (no_reset_cond rst_exprs) (f_e_eq (EIdent stv) (EIdent lnstv))) in let st_eq_inact (st, _) = let st_scope = node, aid^"."^st.st_name^".", st.body in let clock_scope, clock_eq = gen_clock td st_scope false rst_exprs in f_and clock_eq (f_and (f_of_scope false td st_scope cs assume_guarantees) (f_and_list (List.map (fun (c, _, _) -> expr_eq c) st.until))) in if active then let st_eq_act (st, l) = let act_eq = let st_scope = node, aid^"."^st.st_name^".", st.body in let cs2, clock_eq = gen_clock td st_scope true rst_exprs in let st_eq = f_and clock_eq (f_of_scope true td st_scope cs2 assume_guarantees) in let rec aux = function | [] -> BEnumCons(E_EQ, nstv, EItem st.st_name) | (c, (target, l), rst)::q -> if rst then loc_error l error "Resetting transitions not supported."; f_or (f_and (f_of_expr td (node, prefix, clock_scope) c) (BEnumCons(E_EQ, nstv, EItem target))) (f_and (BNot (f_of_expr td (node, prefix, clock_scope) c)) (aux q)) in f_and st_eq (aux st.until) in f_or (f_and (BEnumCons(E_EQ, stv, EItem st.st_name)) act_eq) (f_and (BEnumCons(E_NE, stv, EItem st.st_name)) (st_eq_inact (st, l))) in f_and st_choice_eq (f_and_list (List.map st_eq_act states)) else f_and st_choice_eq (f_and_list (List.map st_eq_inact states)) in f_and_list (List.map do_eq eqs) and f_of_prog rp assume_guarantees = let td = { rp = rp; consts = I.consts rp; } in let prog_normal = let clock_scope, clock_eq = gen_clock td rp.root_scope true [] in let scope_f = f_of_scope true td td.rp.root_scope clock_scope assume_guarantees in f_and clock_eq scope_f in let prog_init = let clock_scope, clock_eq = gen_clock td rp.root_scope true [BConst true] in let scope_f = f_of_scope true td td.rp.root_scope clock_scope assume_guarantees in f_and clock_eq scope_f in prog_init, prog_normal (* Get expressions for guarantee violation *) let rec g_of_scope td (node, prefix, eqs) clock_scope cond = let expr_g e = let instance_g (_, id, eqs, args) = g_of_scope td (node^"/"^id, "", eqs) clock_scope cond in List.fold_left (fun x i -> (instance_g i) @ x) [] (extract_instances td.rp.p e) in let do_eq eq = match fst eq with | AST_assign(_, e) | AST_assume(_, e) -> expr_g e | AST_guarantee((id, _), e) -> (id, f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(e), snd e))) :: (expr_g e) | AST_activate (b, _) -> let rec cond_g cond = function | AST_activate_body b -> let bscope = node, b.act_id^".", b.body in g_of_scope td bscope (clock_scope_here bscope) cond | AST_activate_if(c, a, b) -> (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) c)) a) @ (cond_g (f_and cond (f_of_expr td (node, prefix, clock_scope) (AST_not(c), snd c))) b) @ (expr_g c) in cond_g cond b | AST_automaton (aid, states, _) -> let st_g (st, _) = let stscope = (node, aid^"."^st.st_name^".", st.body) in g_of_scope td stscope (clock_scope_here stscope) (f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name))) in List.flatten (List.map st_g states) in List.flatten (List.map do_eq eqs) and guarantees_of_prog rp = let td = { rp = rp; consts = I.consts rp; } in g_of_scope td rp.root_scope (clock_scope_here rp.root_scope) (BConst true) (* 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 | _ -> [] 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] | _ -> [])