pass_strategy_synthesis/model_with_structures/analyzer.ml

module Functional =
struct

  type data = int
  type memid = int

  (* --- syntax --- *)

  type read_cap = Rd | NRd

  type write_cap = AlwaysWr | MayWr | NeverWr
  type copy_cap = Cp | Rf

  type in_cap = In | NIn
  type out_cap = Out | NOut

  type mode = in_cap * out_cap

  type path = VarP of data | DerefP of path | AccessP of path * data

  type atype = UnitT of read_cap * write_cap
             | RefT of copy_cap * atype
             | TupleT of atype list
             | FunT of (mode * atype) list (* TODO: declaration id for ease of impl / performance instead (?) *)

  type mtype = mode * atype

  type expr = UnitE
            | PathE of path
            (* TODO: extend to include arbitrary path *)
            | RefE of data
            | TupleE of expr list

  type stmt = SkipS
            | CallS of path * expr list
            | WriteS of path
            | ReadS of path
            | SeqS of stmt * stmt
            | ChoiceS of stmt * stmt

  type decl = VarD of (* data * *) atype * expr
            | FunD of (* data * *) (* (data * *) mtype (* )  *) list * stmt

  type prog = decl list * stmt

  (* --- exceptions --- *)

  (* exception Incorrect_memory_access of int *)
  (* exception Ref_rvalue_argument of int *)
  (* exception Incorrect_const_cast of int *)
  (* exception Invalid_argument_tag of int *)
  (* exception Incompatible_states *)
  (* exception Incompatible_path_and_type *)
  (* exception Incompatible_path_and_mem *)
  (* exception Incompatible_path_and_type_for_tag *)
  exception Typing_error of string
  exception Eval_error of string
  exception Cant_fold3_error

  (* value model & memory model *)

  type deepvalue = ZeroDV
                 | SmthDV
                 | BotDV
                 | FunDV of ((* data list * *) stmt) list
                 | RefDV of deepvalue
                 | TupleDV of deepvalue list

  type value = ZeroV
             | SmthV
             | BotV
             | FunV of ((* data list * *) stmt) list
             | RefV of memid
             | TupleV of value list

  type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data

  (* TODO: any additional difference between rvalue and lvalue now ?? *)

  (* --- *)

  type mem = value list * memid (* NOTE: memory and first free elem *)
  type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *)
  type vals = (data * memid) list (* glob *) * (data * memid) list (* glob + loc *)
  type visited = stmt list (* TODO: FIXME: optimize, use ids *)
  type state = mem * types * vals * visited

  (* --- *)

  (* - state utils *)

  let types_assoc (x : data) (types : types) : atype =
    (* try ( List.assoc x (fst types) ) *)
    (* with Not_found -> *)
    List.assoc x (snd types)
  let vals_assoc (x : data) (vals : vals) : memid =
    (* try ( List.assoc x (fst vals) ) *)
    (* with Not_found -> *)
    List.assoc x (snd vals)

  let types_glob_add (types : types) (x : data) (t : atype) =
    ((x, t) :: fst types, (x, t) :: snd types)

  let types_add (types : types) (x : data) (t : atype) =
    (fst types, (x, t) :: snd types)

  let vals_glob_add (vals : vals) (x : data) (id : memid) =
    ((x, id) :: fst vals, (x, id) :: snd vals)

  let vals_add (vals : vals) (x : data) (id : memid) =
    (fst vals, (x, id) :: snd vals)

  (* - utils *)

  let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
   | _ :: xs, 0 -> y :: xs
   | x :: xs, _ -> x :: list_replace xs (id - 1) y
   | [], _ -> raise Not_found

  (* TODO: FIXME: check if this foldl or foldr *)
  let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
    | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs 
    | [], [], [] -> acc
    | _, _, _ -> raise Cant_fold3_error

  (* --- *)

  (* NOTE: old variant with assoc array *)
  (* let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) *)
  (* let mem_add (mem : mem) (v : value) : mem * memid = *)
    (* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
  (* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
    (* ((id, v) :: fst mem, snd mem) *)
  let mem_get (mem : mem) (id : memid) : value = (* FIXME TMP Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); *)
                                                 List.nth (fst mem) (snd mem - id - 1)
  let mem_add (mem : mem) (v : value) : mem * memid =
    ((v :: fst mem, snd mem + 1), snd mem)
  let mem_set (mem : mem) (id : memid) (v : value) : mem =
    (list_replace (fst mem) (snd mem - id - 1) v, snd mem)

  let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
    | ZeroV -> ZeroDV
    | SmthV -> SmthDV
    | BotV -> BotDV
    | FunV s -> FunDV s
    | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id)
    | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs)

  let is_trivial_v (v : value) : bool = 
    v == ZeroV || v == SmthV || v == BotV

  (* --- path accessors --- *)

  let rec pathvar (p : path) : data = match p with
    | VarP x -> x
    | DerefP p -> pathvar p
    | AccessP (p, _) -> pathvar p

  let rec pathrev (p : path) (acc : revpath) : revpath = match p with
    | VarP x -> acc
    | DerefP p -> pathrev p @@ DerefRP acc
    | AccessP (p, i) -> pathrev p @@ AccessRP (acc, i)

  let rec pathtype (types : types) (p : path) : atype = match p with
    | VarP x -> types_assoc x types
    | DerefP p -> (match pathtype types p with
                    | RefT (_, t) -> t
                    | _ -> raise @@ Typing_error "pathtype: deref")
    | AccessP (p, id) -> match pathtype types p with
                           | TupleT ts -> (* FIXME TMP Printf.printf "pathtype access sz=%i id=%i\n" (List.length ts) id; *)
                                          (List.nth ts id)
                           | _ -> raise @@ Typing_error "pathtype: access"

  let rec pathval (mem :  mem) (vals : vals) (p : path) : value = match p with
    | VarP x -> mem_get mem @@ ((* Printf.printf "%i: " x; (* FIXME TMP *)
                                ignore @@ List.map (fun (x, _) -> Printf.printf "%i " x) vals;
                                Printf.printf "mem size: %i, " (List.length (fst mem));
                                Printf.printf "mem size stored: %i " (snd mem);
                                Printf.printf "\n"; *)
                                vals_assoc x vals)
    | DerefP p -> (match pathval mem vals p with
                    | RefV id -> mem_get mem id
                    | _ -> raise @@ Typing_error "pathval: deref")
    | AccessP (p, id) -> match pathval mem vals p with
                           | TupleV vs -> (* FIXME TMP Printf.printf "pathval access sz=%i id=%i\n" (List.length vs) id; *)
                                          (List.nth vs id)
                           | _ -> raise @@ Typing_error "pathval: access"

  (* --- eval rules --- *)

  (* - value construction *)

  let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
    if is_trivial_v v
    then match t with
    | UnitT (Rd, _) -> (mem, v)
    | UnitT (NRd, _) -> (mem, BotV)
    | _ -> raise @@ Typing_error "valcopy: trivial value, wrong type"
    else match t, v with
    (* NOTE: replaced with if | best choice ?? *)
    (* | UnitT (Rd, w), ZeroV -> (mem, v) *)
    (* | UnitT (Rd, w), SmthV -> (mem, v) *)
    (* | UnitT (Rd, w), BotV -> (mem, v) *)
    (* | UnitT (NRd, w), ZeroV -> (mem, BotV) *)
    (* | UnitT (NRd, w), SmthV -> (mem, BotV) *)
    (* | UnitT (NRd, w), BotV -> (mem, BotV) *)
    | FunT _, FunV _ -> (mem, v)
    | RefT (Rf, _), RefV _ -> (mem, v)
    | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
                               let (mem'', id'') = mem_add mem' v' in
                               (mem'', RefV id'') 
    | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
                                                                 (mem', v' :: vs') in 
                              let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
                              (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
    | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"

  (* - value update *)

  let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
    | VarRP, _ -> (mem, b)
    | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
                            (mem_set mem' id v', RefV id)
    | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *)
                                                      valupd mem (List.nth vs id) p b in
                                     (* FIXME TMP Printf.printf "before return\n"; *)
                                     (mem', TupleV (list_replace vs id v'))
    | _, _ -> raise @@ Typing_error "valupd"

  (* - value combination *)

  let rec valcomb (u : value) (v : value) : value =
    if is_trivial_v u && is_trivial_v v
    then (if u == v then u else BotV)
    else match u, v with
      | FunV ustmts, FunV vstmts  -> FunV (ustmts @ vstmts)
      | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
      | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
      | _, _ -> raise @@ Typing_error "valcomb"

  let rec memcomb (m : mem) (n : mem) : mem =
    if snd m != snd n
    then raise @@ Typing_error "memcomb"
    else (List.map2 valcomb (fst m) (fst n), snd m)

  (* - expression evaluation *)

  let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
    | UnitE -> ZeroV
    | PathE p -> pathval mem vals p
    | RefE x -> RefV (vals_assoc x vals)
    | TupleE es -> TupleV (List.map (exprval mem vals) es)

  (* - expression typing *)

  let rec exprtype (types : types) (e : expr) : atype = match e with
    | UnitE -> UnitT (Rd, NeverWr)
    | PathE p -> pathtype types p
    | RefE x -> RefT (Rf, types_assoc x types)
    | TupleE es -> TupleT (List.map (exprtype types) es)

  (* - context initialization *)

  (* let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with *)
  
  (* TODO: check new in vars *)
  let add_decl (state : state) (x : data) (d : decl) : state =
    match state with (mem, types, vals, visited) -> match d with
    | VarD (t, e) -> let v = exprval mem vals e in
                     let (mem', v') = valcopy mem v t in
                     let (mem'', id) = mem_add mem' v' in
                     (mem'', types_glob_add types x t, vals_glob_add vals x id, visited)
    | FunD (ts, s)  -> let (mem', id) = mem_add mem (FunV [s]) in
                       (mem', types_glob_add types x (FunT ts), vals_glob_add vals x id, visited)

  let empty_mem : mem = ([], 0)
  let empty_state : state = (empty_mem, ([], []), ([], []), [])

  (* TODO: better way ??? *)
  let globals_min_id : data = 1000

  let prog_init (prog : prog) : state =
    match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *)
                                    (fun (st, x) d -> (add_decl st x d, x + 1))
                                    (empty_state, globals_min_id)
                                    decls

  (* - call values spoil *)

  (* TODO: check all cases *)
  let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
                      (r' : read_cap) (w' : write_cap) (m : mode)
                      (c : copy_cap) : bool =
    (* FIXME TMP *)
    (* Printf.printf "%b %b %b %b %b\n" *)
      (* (r != Rd || v == ZeroV) *)
      (* (r != Rd || fst m == In) *)
      (* (snd m != Out || w == AlwaysWr) *)
      (* (* TODO: FIXME: why always write ?? *) *)
      (* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *)
      (* (is_trivial_v v); *)
    (r != Rd || v == ZeroV) &&
    (r != Rd || fst m == In) &&
    (snd m != Out || w == AlwaysWr) &&
    (* TODO: FIXME: check *)
    ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
    is_trivial_v v

  let rec valspoil (mem : mem) (v : value) (t : atype)
                   (u : atype) (m : mode) (c : copy_cap)
                   : mem * value = match t, u, v with
    | UnitT (r, w), UnitT (r', w'), _ ->
      if not @@ is_trivial_v v
        then raise @@ Typing_error "valspoil: unit, not trivial"
      else if not @@ is_correct_tags v r w r' w' m c
        then raise @@ Typing_error "valspoil: unit, not correct"
      else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr)
        then (mem, BotV)
      else if snd m == Out && w == AlwaysWr
        then (mem, ZeroV)
      else (mem, v)
    | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
    | RefT (ct, t), RefT (cu, u), RefV id ->
      let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
      (mem_set mem id v', RefV id)
    | TupleT ts, TupleT us, TupleV vs ->
        let folder = fun (mem, vs') t u v ->
          let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
        let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
        (mem', TupleV (List.rev vs'))
    | _, _, _ ->  raise @@ Typing_error "valspoil"

  (* full spoil *)

  let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
    match state with (mem, types, vals, visited) ->
    let x = pathvar p in
    let id = vals_assoc x vals in (* base var address *)
    let b = pathval mem vals p in (* subvalue in var *)
    let t' = pathtype types p in (* type of subvalue *)
    let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
    (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *)
    let pi = pathrev p VarRP in
    let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
    mem_set mem'' id v''

  let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
    match state with (mem, types, vals, visited) -> match e, t with
      | UnitE, UnitT _ -> mem
      | PathE p, t -> argsspoilp state m t p
      | RefE x, t -> argsspoilp state m t (VarP x)
      (* TODO: FIXME: check RefE case ? *)
      | TupleE es, TupleT ts -> List.fold_left2
                                  (fun mem' t' e' -> argsspoile (mem', types, vals, visited) m t' e')
                                  mem ts es
      | _, _ ->  raise @@ Typing_error "valspoile"

  (* - funciton argument addition *)

  let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state =
    match state with (mem, types, vals, visited) ->
    let v = exprval mem oldvals e in
    (* let t' = pathtype types p in *)
    let (mem', v') = valcopy mem v t in
    let (mem'', id) = mem_add mem' v' in
    (mem'', types_add types x t, vals_add vals x id, visited)

  (* - function evaluation *)
  (* NOTE: not needed due to performed optimization in stmt_eval *)
  (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)

  (* - statement evaluation *)

  let rec stmt_eval (state : state) (s : stmt) : state =
    match state with (mem, types, vals, visited) -> match s with
    | SkipS -> state
    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
                               pathval mem vals f in
                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
                               pathtype types f in
                       let types' : types = (fst types, fst types) in
                       let vals' : vals = (fst vals, fst vals) in
                       (match v, t with
                          | FunV (* xs, *) fstmts (* ) *), FunT ts ->
                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *)
                                                       List.fold_left2 (* TODO: FIXME: check x's order *)
                              (fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1))
                              ((mem, types', vals', visited), 0) ts es in
                            (* NOTE: same x's, so can use same args for all the statements *)
                            (match state_with_args with (mem_swa, types_swa, vals_swa, visited_swa) ->
                             let visited_new = (* FIXME TMP Printf.printf "call, before eval\n"; *)
                                               List.fold_left
                                                 (fun visited_old stmt ->
                                                    if List.mem stmt visited_old
                                                    then stmt :: visited_old
                                                    else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
                                                      (_, _, _, visited_after_stmt) -> visited_after_stmt)
                                                 visited_swa
                                                 fstmts in
                             let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
                                               List.fold_left2
                               (fun mem (m, t) e -> argsspoile (mem, types, vals, (* NOTE: not important *) visited_new) m t e)
                               mem ts es in
                             (mem_spoiled, types, vals, visited_new))
                          | FunV _, _ -> raise @@ Eval_error "call: function type"
                          | _, FunT _ -> raise @@ Eval_error "call: function val"
                          | _, _ -> raise @@ Eval_error "call: function type & val")
    | WriteS p -> (match pathtype types p with
                     | UnitT (_, w) ->
                       if w == NeverWr
                       then raise @@ Eval_error "write: write tag"
                       else let x = pathvar p in
                            let id = vals_assoc x vals in
                            let pi = pathrev p VarRP in
                            let (mem', v') = valupd mem (mem_get mem id) pi ZeroV in
                            (mem_set mem' id v', types, vals, visited)
                     | RefT _ -> raise @@ Eval_error "write: ref type"
                     | TupleT _ -> raise @@ Eval_error "write: tuple type"
                     | _ -> raise @@ Eval_error "write: type")
    | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV 
                 then raise @@ Eval_error "read: spoiled value"
                 else if pathval mem vals p != ZeroV 
                 then raise @@ Eval_error "read: nontrivial value"
                 else state
    | SeqS (sl, sr) -> let statel = stmt_eval state sl in
                       stmt_eval statel sr
    | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
                          let stater = stmt_eval state sr in
                          match statel with (meml, typesl, valsl, visitedl) ->
                          match stater with (memr, typesr, valsr, visitedr) ->
                          if typesl != typesr || valsl != valsr
                          then raise @@ Eval_error "choice"
                          (* TODO: FIXME: better list union ??  *)
                          else (memcomb meml memr, typesl, valsl, visitedl @ visitedr)

  (* --- program execution --- *)

  let prog_eval (prog : prog) : state =
    match prog with (decls, s) ->
    let init_state = prog_init prog in
    stmt_eval init_state s

  let prog_eval_noret (prog : prog) : unit =
    ignore @@ prog_eval prog

  (* --- tests --- *)

  (* - shortcuts *)

  let ( #. ) x y = SeqS (x, y)
  let ( |. ) x y = ChoiceS (x, y)

  let v0 = VarP 0
  let v1 = VarP 1
  let v2 = VarP 2
  let v3 = VarP 3
  let v4 = VarP 4
  let v5 = VarP 5
  let v6 = VarP 6
  let v7 = VarP 7
  let v8 = VarP 8
  let vg0 = VarP globals_min_id
  let vg1 = VarP (globals_min_id + 1)
  let vg2 = VarP (globals_min_id + 2)
  let vg3 = VarP (globals_min_id + 3)
  let vg4 = VarP (globals_min_id + 4)
  let vg5 = VarP (globals_min_id + 5)
  let vg6 = VarP (globals_min_id + 6)
  let vg7 = VarP (globals_min_id + 7)
  let vg8 = VarP (globals_min_id + 8)
  let vg9 = VarP (globals_min_id + 9)
  let vg10 = VarP (globals_min_id + 10)

  let rf0E = RefE 0
  let rf1E = RefE 1
  let rf2E = RefE 2
  let rf3E = RefE 3
  let rf4E = RefE 4
  let rf5E = RefE 5
  let rf3E = RefE 3
  let rf4E = RefE 4
  let rf5E = RefE 5
  let rfg0E = RefE globals_min_id
  let rfg1E = RefE (globals_min_id + 1)
  let rfg2E = RefE (globals_min_id + 2)
  let rfg3E = RefE (globals_min_id + 3)
  let rfg4E = RefE (globals_min_id + 4)
  let rfg5E = RefE (globals_min_id + 5)
  let rfg6E = RefE (globals_min_id + 6)
  let rfg7E = RefE (globals_min_id + 7)
  let rfg8E = RefE (globals_min_id + 8)

  let pE p = PathE p

  let drf p = DerefP p
  let access i p = AccessP (p, i)

  let wr x = ReadS x 
  let rd x = WriteS x
  let skp = SkipS

  let uT_r_aw = UnitT (Rd, AlwaysWr)
  let uT_r_mw = UnitT (Rd, MayWr)
  let uT_aw = UnitT (NRd, AlwaysWr)
  let uT_mw = UnitT (NRd, MayWr)
  let uT_r = UnitT (Rd, NeverWr)
  let uT = UnitT (NRd, NeverWr)

  let rfT t = RefT (Rf, t)
  let cpT t = RefT (Cp, t)

  let moded t = ((In, NOut), t)

  let defgu t = VarD (t, UnitE)
  let defg t e = VarD (t, e)

  let wrS p = WriteS p 
  let rdS p = ReadS p 
  let callS f args = CallS (f, args)

  (* - utils tests *)

  let%expect_test "mem add / get / set" =
    let mem = empty_mem in
    let (mem, id1) = mem_add mem ZeroV in 
    let (mem, id2) = mem_add mem SmthV in 
    let (mem, id3) = mem_add mem BotV in 
    Printf.printf "%i %i %i " id1 id2 id3;
    Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
                              (mem_get mem id2 == SmthV)
                              (mem_get mem id3 == BotV);
    let mem = mem_set mem id1 BotV in 
    let mem = mem_set mem id2 ZeroV in 
    let mem = mem_set mem id3 SmthV in 
    Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
                              (mem_get mem id2 == ZeroV)
                              (mem_get mem id3 == SmthV);
    [%expect {| 0 1 2 true true true true true true |}]

  (* - basic var tests *)

  let%expect_test "empty" =
    prog_eval_noret ([], SkipS);
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple var" =
    prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)],
                      ReadS (VarP globals_min_id));
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple var, forbidden read" =
    try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
                         ReadS (VarP globals_min_id));
         [%expect.unreachable]);
    with Eval_error msg -> Printf.printf "%s" msg;
    [%expect {| read: spoiled value |}]

  let%expect_test "simple vars, no read & read" =
    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
                      VarD (UnitT (Rd, MayWr), UnitE)],
                     ReadS (VarP (globals_min_id + 1)));
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple var, write" =
    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
                     WriteS (VarP globals_min_id));
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple var, forbidden write" =
    try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)],
                         WriteS (VarP globals_min_id));
         [%expect.unreachable]);
    with Eval_error msg -> Printf.printf "%s" msg;
    [%expect {| write: write tag |}]

  let%expect_test "simple var, write & read" =
    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
                     SeqS (WriteS (VarP globals_min_id),
                           ReadS (VarP globals_min_id)));
    Printf.printf "done!";
    [%expect {| done! |}]

  (* - basic call tests *)

  (* let%expect_test "simple call with read" = *)
    (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *)
                      (* FunD ([((In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0)))], *)
                     (* CallS (VarP (globals_min_id + 1), *)
                            (* [PathE (VarP globals_min_id)])); *)
    (* Printf.printf "done!"; *)
    (* [%expect {| done! |}] *)

  (* let%expect_test "simple call with write" = *)
    (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
                      (* VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE globals_min_id); *)
                      (* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *)
                     (* CallS (VarP (globals_min_id + 2), *)
                            (* [PathE (VarP (globals_min_id + 1))])); *)
    (* Printf.printf "done!"; *)
    (* [%expect {| done! |}] *)

  let%expect_test "simple call with read, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_mw;
        defg (rfT uT_r_mw) rfg0E;
        FunD (
          [moded @@ cpT @@ uT_r],
          rdS @@ drf @@ v0
        )
      ],
      callS vg2 [pE vg1]
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with write, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_mw;
        defg (rfT uT_r_mw) rfg0E;
        FunD (
          [moded @@ cpT @@ uT_r_mw],
          wrS @@ drf @@ v0
        )
      ],
      callS vg2 [pE vg1]
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with read after write, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_mw;
        defg (rfT uT_r_mw) rfg0E;
        FunD (
          [moded @@ cpT @@ uT_mw],
          (wrS @@ drf @@ v0) #.
          (rdS @@ drf @@ v0)
        )
      ],
      callS vg2 [pE vg1]
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with forbidden write, dsl" =
    try (prog_eval_noret (
      [
        defgu uT_r_mw;
        defg (rfT uT_r_mw) rfg0E;
        FunD (
          [moded @@ cpT @@ uT_r],
          wrS @@ drf @@ v0
        )
      ],
      callS vg2 [pE vg1]
    );
    [%expect.unreachable]);
    with Eval_error msg -> Printf.printf "%s" msg;
    [%expect {| write: write tag |}]

  (* TODO: FIXME: why is condition on always write in parent ?? *)
  let%expect_test "simple call with write to ref, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        FunD (
          [moded @@ rfT @@ uT_aw],
          wrS @@ drf @@ v0
        )
      ],
      callS vg2 [pE vg1]
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with forbidden write to ref, dsl" =
    try (prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        FunD (
          [moded @@ rfT @@ uT_aw],
          wrS @@ drf @@ v0
        )
      ],
      (callS vg2 [pE vg1]) #.
      (rdS @@ drf @@ vg1)
    );
    [%expect.unreachable]);
    with Eval_error msg -> Printf.printf "%s" msg;
    [%expect {| read: spoiled value |}]

  let%expect_test "simple call with write to ref with fix, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        FunD (
          [moded @@ rfT @@ uT_aw],
          wrS @@ drf @@ v0
        )
      ],
      (callS vg2 [pE vg1]) #.
      (wrS @@ drf @@ vg1) #.
      (rdS @@ drf @@ vg1)
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "call inside call, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        FunD (
          [moded @@ rfT @@ uT_aw],
          wrS @@ drf @@ v0
        );
        FunD (
          [moded @@ cpT @@ uT_aw],
          (callS vg2 [pE v0]) #.
          (wrS @@ drf @@ v0)
        )
      ],
      (callS vg3 [pE vg1]) #.
      (rdS @@ drf @@ vg1)
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  (* NOTE: memoization used *)
  let%expect_test "call inside call, recursive, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        FunD (
          [moded @@ cpT @@ uT_aw],
          (callS vg2 [pE v0]) #.
          (wrS @@ drf @@ v0)
        )
      ],
      (callS vg2 [pE vg1]) #.
      (rdS @@ drf @@ vg1)
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "call to fix after call, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        FunD (
          [moded @@ rfT @@ uT_aw],
          wrS @@ drf @@ v0
        );
        FunD (
          [((In, Out), rfT @@ uT_aw)],
          wrS @@ drf @@ v0
        )
      ],
      (callS vg2 [pE vg1]) #.
      (callS vg3 [pE vg1]) #.
      (rdS @@ drf @@ vg1)
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with global variable usage, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        FunD (
          [moded @@ cpT @@ uT_aw],
          (wrS @@ vg0) #.
          (rdS @@ drf @@ vg1)
        )
      ],
      (callS vg2 [pE vg1]) #.
      (rdS @@ drf @@ vg1)
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with read & write (2 args), dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg2E;
        FunD (
          [
            moded @@ rfT @@ uT_r;
            moded @@ rfT @@ uT_aw;
          ],
          (rdS @@ drf @@ v0) #.
          (wrS @@ drf @@ v1)
        )
      ],
      callS vg4 [pE vg1; pE vg3]
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with different arguments modifiers, copy, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg2E;
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg4E;
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg6E;
        FunD (
          [
            ((NIn, NOut), cpT @@ uT_aw);
            ((In, NOut), cpT @@ uT_r_aw);
            ((NIn, Out), cpT @@ uT_aw);
            ((In, Out), cpT @@ uT_r_aw);
          ],
          (rdS @@ drf @@ v1) #.
          (rdS @@ drf @@ v3) #.
          (wrS @@ drf @@ v1) #.
          (wrS @@ drf @@ v2) #.
          (wrS @@ drf @@ v3)
        )
      ],
      (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
      (rdS @@ drf @@ vg1) #.
      (rdS @@ drf @@ vg3) #.
      (rdS @@ drf @@ vg5) #.
      (rdS @@ drf @@ vg7)
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  let%expect_test "simple call with different arguments modifiers, ref, dsl" =
    prog_eval_noret (
      [
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg0E;
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg2E;
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg4E;
        defgu uT_r_aw;
        defg (rfT uT_r_aw) rfg6E;
        FunD (
          [
            ((NIn, NOut), rfT @@ uT);
            ((In, NOut), rfT @@ uT_r);
            ((NIn, Out), rfT @@ uT_aw);
            ((In, Out), rfT @@ uT_r_aw);
          ],
          (rdS @@ drf @@ v1) #.
          (rdS @@ drf @@ v3) #.
          (wrS @@ drf @@ v2) #.
          (wrS @@ drf @@ v3)
        )
      ],
      (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
      (rdS @@ drf @@ vg1) #.
      (rdS @@ drf @@ vg3) #.
      (rdS @@ drf @@ vg5) #.
      (rdS @@ drf @@ vg7)
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  (* - complex tests *)

  (* NOTE: path access isreversed to intuitive function application
           by definition *)
  let%expect_test "complex test: send, dsl" =
    prog_eval_noret (
      (* TODO: set optimal ref mods later *)
      let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in
      let user_infoT =  TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in
      let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in
      let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in
      let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in
      let requestT = TupleT [cpT userT (* 0 user *);
                             cpT versionT (* 1 version *);
                             cpT utilsT (* 2 utils *);
                             cpT uT_r_aw (* 3 data *);
                             uT_r_aw (* 4 operation_date *)] in
      let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in
      let user_infoE =  TupleE [UnitE (* 0 name *); UnitE; UnitE] in
      let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in
      let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in
      let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in
      let requestE = TupleE [rfg2E (* 0 user *);
                             rfg3E (* 1 version *);
                             rfg4E (* 2 utils *);
                             rfg5E (* 3 data *);
                             UnitE (* 4 operation_date *)] in
      let get_version_idID = vg7 in
      let updated_versionID = vg8 in
      let sendID = vg9 in
      let send_allID = vg10 in
      let get_version_idF = FunD ([moded requestT],
        (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
      let updated_versionF = FunD ([moded requestT],
        (rdS @@ access 0 @@ drf @@ access 2 v0) #.
        (* TODO: read all the substructure ?? *)
        (rdS @@ access 0 @@ drf @@ access 1 v0) #.
        (rdS @@ access 1 @@ drf @@ access 1 v0)) in
      let sendF = FunD ([moded requestT],
        ((
           (wrS @@ access 0 @@ drf @@ access 2 v0) #.
           (rdS @@ drf @@ access 3 v0) #.
           (wrS @@ drf @@ access 3 v0) #.
           (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
         ) |. skp) #.
         (wrS @@ access 4 v0) #.
         (* TODO: read all the substructure ?? *)
         (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *)
      let send_allF = FunD ([moded requestT],
        (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *)
        (callS sendID [pE v0]) #.
        (callS get_version_idID [pE v0]) #.
        (callS updated_versionID [pE v0]) #.
        (* TODO: read all the substructure ?? *)
        (wrS @@ access 0 @@ drf @@ access 1 v0) #.
        (wrS @@ access 1 @@ drf @@ access 1 v0) #.
        (* --- *)
        ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |.
         (rdS @@ access 0 @@ drf @@ access 1 v0))) in
      let varID = vg6 in
      [
        defg user_utilsT user_utilsE;
        defg user_infoT user_infoE;
        defg userT userE;
        defg versionT versionE;
        defg utilsT utilsE;
        defgu uT_r_aw;
        defg requestT requestE;
        get_version_idF;
        updated_versionF;
        sendF;
        send_allF
      ],
      callS send_allID [pE varID]
    );
    Printf.printf "done!";
    [%expect {| done! |}]

  (* TODO: version with more optimal modifiers *)
end