file for abstract domain alternative model, fixes

model_with_control_flow/abstract_domain_model.typ

@@ -0,0 +1,448 @@
+// #import "@preview/polylux:0.4.0": *
+#import "@preview/simplebnf:0.1.1": *
+// #import "@preview/zebraw:0.5.0": *
+// #show: zebraw
+#import "@preview/curryst:0.6.0": rule, prooftree, rule-set
+#import "@preview/xarrow:0.4.0": xarrow, xarrowDashed
+
+= Формальная модель используемого языка
+
+*TODO: переработь обычную control flow семантику в формат collecting semantics*
+i
+Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
+
+Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
+- & of | of & -вложенные блоки ?
+- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
+
+Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
+вызов лямбд будет нужен в модели?
+- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
+можно ввести отдельные сигнатуры-определения?
+
+проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
+
+== Синтаксис
+
+#h(10pt)
+
+#let isCorrect = `isCorrect`
+
+#let isRead = `isRead`
+#let isAlwaysWrite = `isAlwaysWrite`
+#let isPossibleWrite = `isPossibleWrite`
+#let isRef = `isRef`
+#let isCopy = `isCopy`
+#let isIn = `isIn`
+#let isOut = `isOut`
+
+#let tag = `tag`
+#let value = `value`
+#let stmt = `stmt`
+#let decl = `decl`
+#let prog = `prog`
+#bnf(
+  Prod(`read`,
+    { Or[Read][read passed value]
+      Or[Not Read][] } ),
+  Prod(`write`,
+    { Or[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant
+      Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?)
+      Or[$not$ Write][] } ), // no write, require n owrites in all flow variants
+  Prod(`copy`,
+    { Or[Ref][pass reference to the value]
+      Or[Value][pass copy of the value] } ),
+  Prod(`in`,
+    { Or[In][parameter value used as input]
+      Or[Not In][] } ),
+  Prod(`out`,
+    { Or[Out][parametr value returned]
+      Or[Not Out][] } ),
+  Prod(
+    `tag`,
+    {
+      Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
+    }
+  ),
+  Prod(
+    `value`,
+    {
+      Or[$0$][cell with some value (always)]
+      Or[$X$][cell with possible value or $bot$]
+      Or[$bot$][spoiled cell (always)]
+    }
+  ),
+  // Prod(
+  //   `arg`,
+  //   {
+  //     Or[$0$][new value, no associated variable]
+  //     Or[$ amp d$][value from some variable]
+  //   }
+  // ),
+  Prod(
+    `stmt`,
+    {
+      Or[`CALL` $f space overline(x)$][call function by id]
+      Or[`WRITE` $x$][write to variable]
+      Or[`READ` $x$][read from variable]
+      Or[`CHOICE` #overline(`stmt`) #overline(`stmt`)][control flow operator, xecution of one of the blocks]
+      // NOTE: var: replaced with arguments (use rvalue as init) (?)
+      // Or[`VAR`][variables inside functions] // NOTE: no modifiers required, because it is in the new memory ?? // TODO: not required ??
+      // NOTE: lambda: compile to call to the funciton with CHOICE between possible lambda bodies <- do this analysis inside synthesizer ?
+    }
+  ),
+  Prod(
+    `decl`,
+    {
+      Or[$overline(stmt)$][function body]
+      Or[$lambda #[`tag` #h(3pt)] a.$ `decl`][argument with argument pass strategy annotation]
+    }
+  ),
+  Prod(
+    `prog`,
+    {
+      Or[`decl`][main function]
+      Or[`decl` `prog`][with supplimentary funcitons]
+    }
+  ),
+)
+== Семантика статического интерпретатора
+
+#h(10pt)
+
+$V := value$ - значения памяти
+
+$L := NN$ - позиции в памяти
+
+$X$ - можество переменных
+
+*TODO: специфицировать доступ*
+
+*TODO: формально описать accessor-ы tag*
+
+$sigma : X -> tag times L$ - #[ позиции памяти, соответстующие переменным контекста,
+                               частично определённая функция ]
+
+$mu : NN -> V$ - память, частично определённая функция
+
+$l in NN$ - длина используемого фрагмента памяти
+
+$DD : NN -> decl$ - определения функций, частично определённая функция
+
+$d in decl, s in stmt, f in NN, x in X, a in NN$
+
+$d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
+
+#let args = `args`
+
+#[
+
+#let ref = `ref`
+#let copy = `copy`
+#let read = `read`
+
+#let cl = $chevron.l$
+#let cr = $chevron.r$
+
+// #align(center, grid(
+//   columns: 3,
+//   gutter: 5%,
+//   align(bottom, prooftree(
+//   ...
+//   )),
+//   align(bottom, prooftree(
+//   ...
+//   )),
+//   align(bottom, prooftree(
+//   ...
+//   )),
+// ))
+
+// TODO: introduce spep env argument ??
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ is correct],
+    $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write
+    $isRead tag -> isIn tag$,
+    $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite sigma(x)$, // NOTE: may tag => should sigma(x)
+    $isRead tag -> mu (sigma(x)) != bot and mu (sigma(x)) != X$, // NOTE: may tag -> ...
+    // TODO: FIXME: != Bot and != X ??? or just != Bot ???
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ spoil init],
+    $mu stretch(=>)^nothing_(cl sigma, mu cr) mu$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ spoil step],
+
+    $mu stretch(=>)^args_sigma gamma$,
+
+    $isPossibleWrite tag$, // NOTE: weak requirement: may write
+    $not isCopy tag$,
+    $not isOut tag$,
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+
+    // mu
+    $gamma stretch(=>)^((tag, x) : args)_sigma gamma[sigma(x) <- bot]$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ fix step],
+
+    $mu stretch(=>)^args_sigma gamma$,
+
+    $isAlwaysWrite tag$, // NOTE: strong requirement: should write
+    $isOut tag$,
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+
+    // mu
+    $gamma stretch(=>)^((tag, x) : args)_sigma gamma[sigma(x) <- 0]$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ skip step],
+
+    $mu stretch(=>)^args_sigma gamma$,
+
+    $not "spoil step"$,
+    $not "fix step"$,
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+
+    // mu
+    $gamma stretch(=>)^((tag, x) : args)_sigma gamma$
+  )
+))
+
+
+#h(10pt)
+
+#align(center, line())
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ $(lambda tag a. d) x, ref + read$],
+
+    $cl sigma, mu, l cr
+     xarrowDashed(d space @ space overline(y))
+     cl sigma, mu', l' cr$,
+
+    $isRead tag$,
+    $not isCopy tag$,
+
+    // NOTE: correctness checked in CALL f
+
+    $cl sigma, mu, l cr
+     xarrowDashed((lambda tag a. d) space @ space  x space overline(y))
+     cl sigma, mu', l' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ $(lambda tag a. d) x, ref - read$],
+
+    $cl sigma, mu [sigma(x) <- bot], l cr
+     xarrowDashed(d space @ space overline(y))
+     cl sigma, mu', l' cr$,
+
+    $not isRead tag$,
+    $not isCopy tag$,
+
+    // NOTE: correctness checked in CALL f
+
+    $cl sigma, mu, l cr
+     xarrowDashed((lambda tag a. d) space @ space  x space overline(y))
+     cl sigma, mu', l' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ $(lambda tag a. d) x, copy + read$],
+
+    $cl sigma [a <- l], mu [l <- 0], l + 1 cr
+     xarrowDashed(d space @ space overline(y))
+     cl sigma', mu', l' cr$,
+
+    $isRead tag$,
+    $isCopy tag$,
+
+    // NOTE: correctness checked in CALL f
+
+    $cl sigma, mu, l cr
+     xarrowDashed((lambda tag a. d) space @ space x space overline(y))
+     cl sigma', mu', l' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ $(lambda tag a. d) x, copy - read$],
+
+    $cl sigma [a <- l], mu [l <- bot], l + 1 cr
+     xarrowDashed(d space @ space overline(y))
+     cl sigma', mu', l' cr$,
+
+    $not isRead tag$,
+    $isCopy tag$,
+
+    // NOTE: correctness checked in CALL f
+
+    $cl sigma, mu, l cr
+     xarrowDashed((lambda tag a. d) space @ space x space overline(y))
+     cl sigma', mu', l' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [decl body],
+
+    $cl sigma, mu, l cr
+     attach(stretch(->)^overline(s), tr: *)
+     cl sigma', mu', l' cr$,
+
+    $d = overline(s)$,
+
+    $cl sigma, mu, l cr
+     xarrowDashed(d space @)
+     cl sigma', mu', l' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, line())
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ CALL $f space overline(x)$],
+
+    $cl [], mu, l cr
+     xarrowDashed(d space @ space overline(x))
+     cl sigma', mu', l' cr$,
+
+    // TODO: FIXME define args in some way
+    $mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
+
+    $DD(f) := d$,
+
+    $cl sigma, mu, l cr
+     xarrow("CALL" f space overline(x))
+     cl sigma, gamma, l cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ READ $x$],
+
+    $mu[sigma(x)] != bot$,
+    $mu[sigma(x)] != X$,
+
+    $cl sigma, mu, l cr
+     xarrow("READ" x)
+     cl sigma, mu, l cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ WRITE $x$],
+
+    $isPossibleWrite sigma(x)$, // TODO: FIXME ?? always or possible ??
+
+    $cl sigma, mu, l cr
+     xarrow("WRITE" x)
+     cl sigma, mu[x <- 0], l union {sigma(x)} cr$,
+  )
+))
+
+#h(10pt)
+
+#let combine = `combine`
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ CHOICE $overline(s)$ $overline(t)$],
+
+    $cl sigma, mu, l cr
+     attach(stretch(->)^overline(s), tr: *)
+     cl sigma_s, mu_s, l_s cr$,
+
+    $cl sigma, mu, l cr
+     attach(stretch(->)^overline(t), tr: *)
+     cl sigma_t, mu_t, l_t cr$,
+
+    $l_t = l_s$,
+    $sigma_s = sigma_t$,
+
+    // TODO changes ?? two ways ??
+    $cl sigma, mu, l cr
+     xarrow("CHOICE" overline(s) space overline(t))
+     cl sigma, combine(mu_s, mu_t), l cr$,
+  )
+))
+
+#h(10pt)
+
+$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $
+$ combine_e (bot, bot) = bot $
+$ combine_e (0, 0) = 0 $
+$ combine_e (\_, \_) = X $
+
+]

model_with_control_flow/analyzer.ml

@@ -60,8 +60,9 @@ struct
 
   let state_combine (left : state) (right : state) : state = match left, right with
     (lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) ->
-    if lenv != renv || lmem_len != rmem_len || lvisited != rvisited then raise Incompatible_states
+    if lenv != renv || lmem_len != rmem_len then raise Incompatible_states
-    else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited) (* TODO: union visited lists instead ? *)
+    else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited)
+    (* TODO: union visited lists instead ? *)
 
   (* --- *)
 
@@ -517,6 +518,22 @@ struct
 
   (* --- *)
 
-  (* TODO: combine statement tests *)
+  (* TODO: more Combine statement tests *)
+
+  let%expect_test "simple function call with value arg and choice, rw" =
+    eval_prog ([([wi_value], [Choice ([Write 0; Read 0], [Write 0]); Read 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple function call with ref arg and choice, rw" =
+    try (eval_prog ([([ri_ref], [Choice ([Read 0], [Write 0])])], ([wi_value], [Write 0; Call (0, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_const_cast id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "simple function call with ref arg and choice, rr" =
+    eval_prog ([([ri_ref], [Choice ([Read 0], [Read 0; Read 0])])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
 
 end

model_with_control_flow/model.typ

@@ -94,8 +94,8 @@
   Prod(
     `decl`,
     {
-      Or[ovreline(stmt)][function body]
+      Or[overline(stmt)][function body]
-      Or[$lambda #[`tag` #h(3pt) `argtype`] a.$ `decl`][argument with argument pass strategy annotation]
+      Or[$lambda #[`tag` #h(3pt)] a.$ `decl`][argument with argument pass strategy annotation]
     }
   ),
   Prod(
@@ -167,7 +167,8 @@ $d space @ space overline(x)$ - запись применения функции
     $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write
     $isRead tag -> isIn tag$,
     $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite sigma(x)$, // NOTE: may tag => should sigma(x)
-    $isRead tag -> mu (sigma(x)) != bot$, // NOTE: may tag -> ... 
+    $isRead tag -> mu (sigma(x)) != bot and mu (sigma(x)) != X$, // NOTE: may tag -> ...
+    // TODO: FIXME: != Bot and != X ??? or just != Bot ???
 
     $isCorrect_(cl sigma, mu cr) (tag, x)$,
   )
@@ -406,7 +407,7 @@ $d space @ space overline(x)$ - запись применения функции
 
     $cl sigma, mu, l cr
      xarrow("WRITE" x)
-     cl sigma, mu[x <- 0], l union {sigma(x)} cr$,
+     cl sigma, mu[x <- 0], l cr$,
   )
 ))
 

model_with_control_flow/synthesizer.ml

@@ -190,9 +190,9 @@ struct
   module Stmt = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd
+      type nonrec ('d, 'dl, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl
       [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (Nat.ground, Nat.ground List.ground) t
+      type ground = (Nat.ground, Nat.ground List.ground, ground List.ground) t
     ]
 
     module Test = struct
@@ -260,7 +260,7 @@ struct
   module Value = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec t = Unit | Bot
+      type nonrec t = Unit | Undef | Bot
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = t
     ]
@@ -290,6 +290,51 @@ struct
     end
   end
 
+  (* --- *)
+
+  let rec list_zip_witho f xs ys zs = ocanren {
+    { fresh x, xs', y, ys', z, zs' in
+      xs == x :: xs' &
+      ys == y :: ys' &
+      zs == z :: zs' &
+      f x y z &
+      list_zip_witho f xs' ys' zs' } |
+    { fresh x, xs' in
+      xs == x :: xs' &
+      ys == [] &
+      zs == [] } |
+    { fresh y, ys' in
+      xs == [] &
+      ys == y :: ys' &
+      zs == [] } |
+    { xs == [] & ys == [] & zs == [] }
+  }
+
+  (* --- *)
+
+  let value_combineo left right res = let open Value in ocanren {
+    { left == Unit & right == Unit & res == Unit } |
+    { left == Bot & right == Bot & res == Bot } |
+    { left == Unit & right == Bot & res == Undef } |
+    { left == Bot & right == Unit & res == Undef }
+  }
+
+  let memory_combineo left right res = ocanren {
+    list_zip_witho value_combineo left right res
+  }
+
+  let state_combineo left right res = let open St in ocanren {
+    fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in
+    left == St (lenv, lmem, lmem_len, lvisited) &
+    right == St (renv, rmem, rmem_len, rvisited) &
+    lenv == renv & lmem_len == rmem_len &
+    memory_combineo lmem rmem res_mem  &
+    res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited)
+    (* TODO: union visited lists instead ? *)
+  }
+
+  (* --- *)
+
   let rec list_replaceo xs id value ys = ocanren {
     (* xs == [] & ys == [] | (* NOTE: error *) *)
     { fresh x, xs' in
@@ -582,7 +627,10 @@ struct
       stmt == Write id &
       env_geto state id tag _mem_id &
       is_may_writeo tag &
-      mem_seto state id Unit state' }
+      mem_seto state id Unit state' } |
+    { fresh xs, ys in
+      stmt == Choice (xs, ys) }
+    (* TODO: FIXME: choice actions *)
   }
 
   and eval_body_foldero prog state stmt state' =

simplest_model_with_mods/model.typ

@@ -383,7 +383,7 @@ $d space @ space overline(x)$ - запись применения функции
 
     $cl sigma, mu, l cr
      xarrow("WRITE" x)
-     cl sigma, mu[x <- 0], l union {sigma(x)} cr$,
+     cl sigma, mu[x <- 0], l cr$,
   )
 ))