path: root/abstract/transform.ml

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_ternary
          (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true))
          (sub where a)
          (sub where b)
    else if not (td.rp.no_time_scope clock_scope)
    then
      f_ternary
          (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false))
          (sub where b)
          (sub where a)
    else begin
      Format.eprintf "WARNING: scope %s needs a clock (init var or time var)!@."
        clock_scope;
      f_or (sub where a) (sub where b)
    end
  (* other *)
  | AST_if(c, a, b) ->
    f_ternary
      (f_of_expr td (node, prefix, clock_scope) c)
      (sub where a)
      (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_ternary
      (f_of_expr td (node, prefix, clock_scope) expr)
      (where [EE (EItem bool_true)])
      (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
  let le = loc_error (snd expr) 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
          | [NE _; EE _] | [EE _; NE _] -> le type_error "Invalid arguments for binary operator."
          | _ -> le invalid_arity "Binary operator")
        (AST_tuple [a; b], snd expr))
  (* Temporal *)
  | AST_arrow(a, b) ->
    if td.rp.init_scope clock_scope
    then
      BTernary(
        (f_e_eq (EIdent (clock_scope^"init")) (EItem bool_true)),
        (sub where a),
        (sub where b))
    else if not (td.rp.no_time_scope clock_scope)
    then
      BTernary(
        (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)),
          (sub where b),
          (sub where a))
    else begin
      Format.eprintf "WARNING: scope %s needs a clock (init var or time var)!@."
        clock_scope;
      f_or (sub where a) (sub where b)
    end
  (* 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
  | _ -> le 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 clock_scope_here (node, prefix, _) =
  node^"/"^prefix

let gen_clock td (node, prefix, _) active rst_exprs =
  let clock_scope = node^"/"^prefix in
  let act_eq =
    if clock_scope = "/"
      then BConst true
      else if active
        then BEnumCons(E_EQ, clock_scope^"act", EItem bool_true)
        else BEnumCons(E_NE, clock_scope^"act", EItem bool_true)
  in
  let clock_eq =
    let rst_code =
        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)
    in
    let last_act_eq =
      (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 BEnumCons (E_NE, clock_scope^"init", EItem bool_true)
          else BConst true))
    in
    let last_inact_eq =
      (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
    let no_rst_code =
      if clock_scope = "/"
        then last_act_eq
        else
          f_ternary
            (BEnumCons(E_EQ, "L"^clock_scope^"act", EItem bool_true))
            last_act_eq last_inact_eq
    in
    if rst_code = BConst true && no_rst_code = BConst true
      then BConst true
      else
        f_ternary
          (reset_cond rst_exprs)
          rst_code
          no_rst_code
  in
  (clock_scope, rst_exprs), f_and act_eq 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_ternary
            (f_of_expr td (node, prefix, clock_scope) e)
            (BEnumCons(E_EQ, gn, EItem bool_true))
            (BEnumCons(E_NE, gn, EItem bool_true))
      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_ternary
            (f_of_expr td (node, prefix, clock_scope) c)
            (f_and (do_tree_act a) (do_tree_inact b))
            (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_ternary
          (reset_cond rst_exprs)
          (f_e_eq (EIdent stv) (EItem init_st.st_name))
          (f_e_eq (EIdent stv) (EIdent lnstv))
      in

      let rst_states = uniq_sorted @@ List.sort compare @@ List.flatten
          (List.map (fun (st, _) ->
              List.map (fun (_, (id, _), _) -> id)
              (List.filter (fun (_, _, rst) -> rst) st.until))
            states)
      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 rst_exprs =
              if List.mem st.st_name rst_states then
                  (f_e_eq (EIdent("L"^node^"/"^aid^"."^st.st_name^".must_reset"))
                    (EItem bool_true))::rst_exprs
              else rst_exprs
            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 cr, cnr = List.partition
              (fun i -> List.exists (fun (_, (v, _), x) -> x && v = i) st.until)
              rst_states in
            let must_reset_c l f =
              f_and_list
                (List.map
                  (fun i -> f_e_eq (EIdent (node^"/"^aid^"."^i^".must_reset"))
                      (EItem (if f i then bool_true else bool_false)))
                  l)
            in
            let rec aux = function
              | [] ->
                f_and
                  (must_reset_c cr (fun _ -> false))
                  (BEnumCons(E_EQ, nstv, EItem st.st_name))
              | (c, (target, l), rst)::q ->
                f_ternary
                  (f_of_expr td (node, prefix, clock_scope) c)
                  (f_and
                    (BEnumCons(E_EQ, nstv, EItem target))
                    (must_reset_c cr (fun i -> rst && i = target)))
                  (aux q)
            in
            let trans_code = must_reset_c cnr (fun _ -> false) in
            let trans_code = f_and trans_code (aux st.until) in
            f_and st_eq trans_code 
          in
          if List.length states = 1 then
            act_eq
          else
            f_ternary
              (BEnumCons(E_EQ, stv, EItem st.st_name))
              act_eq
              (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
            (f_and_list
              (List.map
                (fun s -> let n = node^"/"^aid^"."^s^".must_reset" in
                  f_e_eq (EIdent n) (EIdent ("L"^n)))
                rst_states))
            (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

let f_of_prog_incl_init rp assume_guarantees =
    let td = {
      rp = rp;
      consts = I.consts rp;
    } in

    let init_cond = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in
    let no_next_init_cond = BEnumCons(E_NE, "/must_reset", EItem bool_true) in

    let clock_scope, clock_eq = gen_clock td rp.root_scope true [init_cond] in

    let scope_f = 
      f_of_scope
        true
        td td.rp.root_scope
        clock_scope
        assume_guarantees in
    f_and clock_eq (f_and no_next_init_cond scope_f)

      


(*
    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
  | 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]
    | _ -> [])