Merge branch 'master' into labs

Author: sim642

src/abseval/abseval.ml

@@ -0,0 +1,33 @@
+(** Abstraktne väärtustaja ehk abstraktne interpretaator. *)
+open Ast
+
+(** Abstraktseid väärtustajaid saab luua kasutades erinevaid täisarve abstraheerivaid domeene.
+    Vt. IntDomain. *)
+module Make (ID: IntDomain.S) =
+struct
+  (** Väärtuskeskkonna domeen kasutades antud täisarvude domeeni. *)
+  module ED = EnvDomain.Make (ID)
+
+  (** Väärtustab avaldise keskkonnas.
+      Vihje: ID.of_int.
+      Vihje: ID.of_interval.
+      Vihje: ID.eval_binary. *)
+  let rec eval_expr (env: ED.t) (expr: expr): ID.t =
+    failwith "TODO"
+
+  (** Väärtustab valvuri (avaldis ja selle oodatav tõeväärtus) keskkonnas.
+      Kui valvur on keskkonnaga vastuolus, siis tagastab saavutamatu programmi oleku ED.bot.
+      Kui valvuriga saab keskkonna muutujate väärtusi täpsemaks kitsendada, siis võib keskkonda muuta.
+      Võib jätta keskkonna muutmata, kuid siis ei kasutata valvurist saadavat lisainfot. *)
+  let eval_guard (env: ED.t) (expr: expr) (branch: bool): ED.t =
+    failwith "TODO"
+
+  module EDFP = Fixpoint.MakeDomain (ED)
+
+  (** Väärtustab lause keskkonnas.
+      Vihje: Vea jaoks kasuta failwith funktsiooni.
+      Vihje: eval_guard.
+      Vihje: While jaoks kasuta püsipunkti moodulit EDFP. *)
+  let rec eval_stmt (env: ED.t) (stmt: stmt): ED.t =
+    failwith "TODO"
+end

src/abseval/dune

@@ -0,0 +1,3 @@
+(library
+ (name abseval)
+ (libraries ast domain fixpoint))

src/domain/domain.ml

@@ -0,0 +1,97 @@
+(** Domeenid. *)
+
+(** Poolvõre. *)
+module type Semilattice =
+sig
+  type t [@@deriving eq, ord, show]
+
+  (** Osaline järjestus.
+
+      Relatsioon, mis on:
+      1. refleksiivne,
+      2. antisümmeetriline,
+      3. transitiivne. *)
+  val leq: t -> t -> bool
+
+  (** Ülemraja operatsioon.
+
+      Leiab elemendi, mis on mõlemast antud elemendist suurem (leq järgi)
+      ja on vähim selline element (leq järgi). *)
+  val join: t -> t -> t
+end
+
+(** Tõkestatud poolvõre. *)
+module type BoundedSemilattice =
+sig
+  include Semilattice
+
+  (** Vähim element (leq järgi). *)
+  val bot: t
+end
+
+(** Meie domeen on tõkestatud poolvõre. *)
+module type S = BoundedSemilattice
+
+
+(** Lisab poolvõrele tehisliku vähima elemendi,
+    et saada tõkestatud poolvõre. *)
+module LiftBot (D: Semilattice) =
+struct
+  type t =
+    | Lift of D.t
+    | Bot
+  [@@deriving eq, ord]
+
+  let pp ppf = function
+    | Bot -> Format.pp_print_string ppf "⊥"
+    | Lift x -> Format.fprintf ppf "Lift %a" D.pp x
+
+  let show = Format.asprintf "%a" pp
+
+  let bot = Bot
+  let leq x1 x2 =
+    match x1, x2 with
+    | Bot, _ -> true
+    | Lift _, Bot -> false
+    | Lift d1, Lift d2 -> D.leq d1 d2
+  let join x1 x2 =
+    match x1, x2 with
+    | Bot, x
+    | x, Bot -> x
+    | Lift d1, Lift d2 -> Lift (D.join d1 d2)
+end
+
+(** Moodustab võrreldamatutest elementidest "lameda" võre,
+    lisades tehislikud vähima ja suurima elemendi. *)
+module Flat (E: sig type t [@@deriving eq, ord, show] end) =
+struct
+  type t =
+    | Top
+    | Lift of E.t
+    | Bot
+  [@@deriving eq, ord]
+
+  let pp ppf = function
+    | Bot -> Format.pp_print_string ppf "⊥"
+    | Lift x -> Format.fprintf ppf "Lift %a" E.pp x
+    | Top -> Format.pp_print_string ppf "⊤"
+
+  let show = Format.asprintf "%a" pp
+
+  let bot = Bot
+  let leq x1 x2 =
+    match x1, x2 with
+    | Bot, _ -> true
+    | Lift _, Bot -> false
+    | Lift d1, Lift d2 -> E.equal d1 d2
+    | _, Top -> true
+    | Top, _ -> false
+  let join x1 x2 =
+    match x1, x2 with
+    | Bot, x
+    | x, Bot -> x
+    | Lift d1, Lift d2 when E.equal d1 d2 -> Lift d1
+    | Lift _, Lift _ -> Top
+    | Top, _
+    | _, Top -> Top
+end

src/domain/dune

@@ -0,0 +1,5 @@
+(library
+ (name domain)
+ (wrapped false)
+ (libraries ast eval)
+ (preprocess (pps ppx_deriving.std)))

src/domain/envDomain.ml

@@ -0,0 +1,23 @@
+(** Väärtuskeskkonna domeen.
+    Muutujate nimed on sõned ja väärtused mingist domeenist. *)
+module Make (D: Domain.S) =
+struct
+  module M = MapDomain.Make (struct type t = string [@@deriving ord, show] end) (D)
+  (* Lisame tehisliku vähima elemendi (kuigi kujutustel on juba olemas),
+     millega tähistame saavutamatut programmi olekut. *)
+  include Domain.LiftBot (M)
+
+  (* Mõned keskkondade/kujutuste operatsioonid. *)
+
+  let find x d =
+    match d with
+    | Bot -> D.bot
+    | Lift m -> M.find x m
+  let add x v d =
+    match d with
+    | Bot -> Bot
+    | Lift m -> Lift (M.add x v m)
+  let empty = Lift M.empty
+  let singleton x v = Lift (M.singleton x v)
+  let of_list l = Lift (M.of_list l)
+end

src/domain/intDomain.ml

@@ -0,0 +1,95 @@
+(** Täisarvude abstraheerimise domeenid. *)
+
+(** Täisarvude domeeni liides. *)
+module type S =
+sig
+  include Domain.S
+
+  (** Loob konkreetsele täisarvule vastava elemendi. *)
+  val of_int: int -> t
+
+  (** Loob intervallist juhuarvule vastava elemendi. *)
+  val of_interval: int * int -> t
+
+  (** Väärtustab binaarse operaatori. *)
+  val eval_binary: t -> Ast.binary -> t -> t
+
+  (** Välistab konkreetse täisarvu. *)
+  val exclude: int -> t -> t
+end
+
+(** Täisarvude hulkade domeen. *)
+module Set =
+struct
+  include SetDomain.Make (struct type t = int [@@deriving ord, show] end)
+  let of_int i = singleton i
+  let of_interval (l, u) = S.of_list (List.init (u - l + 1) (fun i -> l + i))
+
+  (** Rakendab binaarset operaatorit kõikvõimalikele paaridele. *)
+  let eval_binary s1 b s2 =
+    fold (fun i1 acc ->
+        fold (fun i2 acc ->
+            add (Eval.Concrete.eval_binary i1 b i2) acc
+          ) s2 acc
+      ) s1 empty
+
+  let exclude i s = remove i s
+end
+
+(** Konstantide domeen.
+    "Lame" täisarvude võre, mis võimaldab esitada konkreetseid täisarve,
+    kuid mitte-konstandid on täiesti tundmatud. *)
+module Flat =
+struct
+  include Domain.Flat (struct type t = int [@@deriving eq, ord, show] end)
+  let of_int i = Lift i
+  let of_interval ((l, u): int * int): t =
+    failwith "TODO"
+
+  (** Vihje: Eval.Concrete.eval_binary. *)
+  let eval_binary (i1: t) (b: Ast.binary) (i2: t): t =
+    failwith "TODO"
+
+  let exclude (i: int) (i': t): t =
+    failwith "TODO"
+end
+
+(** Intervallide domeen. *)
+module Interval =
+struct
+  module Interval =
+  struct
+    type t = int * int [@@deriving eq, ord]
+
+    let pp ppf (l, u) = Format.fprintf ppf "[%d, %d]" l u
+    let show = Format.asprintf "%a" pp
+
+    let leq ((l1, u1): t) ((l2, u2): t): bool =
+      failwith "TODO"
+
+    let join ((l1, u1): t) ((l2, u2): t): t =
+      failwith "TODO"
+
+    let eval_binary ((l1, u1): t) (b: Ast.binary) ((l2, u2): t): t =
+      match b with
+
+      | Eq | Ne | Lt | Le | Gt | Ge -> (0, 1) (* Võrdluse tulemus on 0 või 1, mis on korrektne, aga mitte täpne. Ettepoole saab implementeerida täpsemad juhud kui vaja. *)
+
+      | _ -> failwith "TODO" (* Ei pea implementeerima kõiki operaatoreid, vaid ainult testideks vajalikud. *)
+  end
+  (* Lisame tehisliku vähima elemendi,
+     millega tähistame võimatut täisarvulist väärtust. *)
+  include Domain.LiftBot (Interval)
+
+  let of_interval (l, u) = Lift (l, u)
+  let of_int i = of_interval (i, i)
+
+  let eval_binary x1 b x2 =
+    match x1, x2 with
+    | Bot, _
+    | _, Bot -> Bot
+    | Lift i1, Lift i2 -> Lift (Interval.eval_binary i1 b i2)
+
+  let exclude (i: int) (x: t): t =
+    failwith "TODO"
+end

src/domain/mapDomain.ml

@@ -0,0 +1,48 @@
+(** Kujutuste domeen. *)
+module Make (K: sig type t [@@deriving ord, show] end) (D: Domain.S) =
+struct
+  module M =
+  struct
+    include Map.Make (K)
+    let pp pp_v ppf m =
+      let pp_kv ppf (k, v) = Format.fprintf ppf "@[%a:@ %a@]" K.pp k pp_v v in
+      let pp_sep ppf () = Format.fprintf ppf ";@ " in
+      Format.fprintf ppf "@[{%a}@]" (Format.pp_print_list ~pp_sep pp_kv) (bindings m)
+  end
+
+  (** Elementideks on kujutused. *)
+  type t = D.t M.t [@@deriving eq, ord, show]
+
+  (** Leiab väärtuse, mis vaikimisi on vähim element. *)
+  let find k m =
+    match M.find_opt k m with
+    | None -> D.bot
+    | Some d -> d
+
+  (** Vähim element on tühi kujutus. *)
+  let bot = M.empty
+
+  (** Osaline järjestus on punktiviisiline. *)
+  let leq m1 m2 =
+    M.for_all (fun k d1 ->
+        let d2 = find k m2 in
+        D.leq d1 d2
+      ) m1
+
+  (** Ülemraja on punktiviisiline. *)
+  let join m1 m2 =
+    M.merge (fun _ d1 d2 ->
+        match d1, d2 with
+        | None, None -> None
+        | Some d1, None -> Some d1
+        | None, Some d2 -> Some d2
+        | Some d1, Some d2 -> Some (D.join d1 d2)
+      ) m1 m2
+
+  (** Mõned kujutuste operatsioonid. *)
+
+  let add = M.add
+  let empty = M.empty
+  let singleton = M.singleton
+  let of_list l = M.of_seq (List.to_seq l)
+end

src/domain/setDomain.ml

@@ -0,0 +1,34 @@
+(** Alamhulkade domeen. *)
+module Make (E: sig type t [@@deriving ord, show] end) =
+struct
+  module S =
+  struct
+    include Set.Make (E)
+    let pp ppf m =
+      let pp_sep ppf () = Format.fprintf ppf ";@ " in
+      Format.fprintf ppf "@[{%a}@]" (Format.pp_print_list ~pp_sep E.pp) (elements m)
+  end
+
+  (** Elementideks on hulgad. *)
+  type t = S.t [@@deriving eq, ord, show]
+
+  (** Vähim element on tühihulk. *)
+  let bot = S.empty
+
+  (** Osaline järjestus on hulkade sisalduvuse järgi. *)
+  let leq s1 s2 = S.subset s1 s2
+
+  (** Ülemraja on hulkade ühend. *)
+  let join s1 s2 = S.union s1 s2
+
+  (** Mõned hulkade operatsioonid. *)
+
+  let singleton = S.singleton
+  let add = S.add
+  let empty = S.empty
+  let of_list = S.of_list
+  let fold = S.fold
+  let remove = S.remove
+  let union = S.union
+  let inter = S.inter
+end

src/fixpoint/dune

@@ -1,3 +1,4 @@
 (library
  (name fixpoint)
+ (libraries domain)
  (preprocess (pps ppx_deriving.std)))

src/fixpoint/fixpoint.ml

@@ -44,3 +44,17 @@ struct
     in
     helper D.empty initial
 end
+
+(** Püsipunktid üle domeenide. *)
+module MakeDomain (D: Domain.S) =
+struct
+  include Make (D)
+
+  (** Leiab funktsiooni vähima püsipunkti. *)
+  let lfp (f: D.t -> D.t): D.t =
+    fp f D.bot
+
+  (** Leiab funktsiooni sulundi, mis sisaldab antud domeeni elementi. *)
+  let closure (f: D.t -> D.t) (initial: D.t): D.t =
+    lfp (fun x -> D.join initial (f x))
+end