summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-24 16:51:28 +0100
committerSon Ho2022-01-24 16:51:28 +0100
commite5dce61f35fcc0e716f7aadc32f254c8ba103887 (patch)
tree380df674714ed7133bf660bd9b75c233ced79485
parent3f10869014d639199fc18df661c3faf3b90e6462 (diff)
Start working on name generation for the synthesis
Diffstat (limited to '')
-rw-r--r--TODO.md2
-rw-r--r--src/Collections.ml207
-rw-r--r--src/Identifiers.ml17
-rw-r--r--src/SymbolicToPure.ml91
-rw-r--r--src/main.ml1
5 files changed, 317 insertions, 1 deletions
diff --git a/TODO.md b/TODO.md
index d92e9640..ff7ba7ab 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,6 +2,8 @@
0. update the end borrows internal to abstractions to not introduce a Bottom
+1. reorder the branches of matches
+
1. stateful maps/sets modules (hashtbl?)
1. Check the occurrence of visitors like visit_AEndedMutLoan: the parameters are
diff --git a/src/Collections.ml b/src/Collections.ml
index 54d0acac..ee998546 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -47,6 +47,17 @@ module type OrderedType = sig
val show_t : t -> string
end
+(** Ordered string *)
+module OrderedString : OrderedType with type t = string = struct
+ include String
+
+ let to_string s = s
+
+ let pp_t fmt s = Format.pp_print_string fmt s
+
+ let show_t s = s
+end
+
module type Map = sig
include Map.S
@@ -155,3 +166,199 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
let show s = to_string None s
end
+
+(** A map where the bindings are injective (i.e., if two keys are distinct,
+ their bindings are distinct).
+
+ This is useful for instance when generating mappings from our internal
+ identifiers to names (i.e., strings) when generating code, in order to
+ make sure that we don't have potentially dangerous collisions.
+ *)
+module type MapInj = sig
+ type key
+
+ type elem
+
+ type t
+
+ val empty : t
+
+ val is_empty : t -> bool
+
+ val mem : key -> t -> bool
+
+ val add : key -> elem -> t -> t
+
+ val singleton : key -> elem -> t
+
+ val remove : key -> t -> t
+
+ val compare : (elem -> elem -> int) -> t -> t -> int
+
+ val equal : (elem -> elem -> bool) -> t -> t -> bool
+
+ val iter : (key -> elem -> unit) -> t -> unit
+
+ val fold : (key -> elem -> 'b -> 'b) -> t -> 'b -> 'b
+
+ val for_all : (key -> elem -> bool) -> t -> bool
+
+ val exists : (key -> elem -> bool) -> t -> bool
+
+ val filter : (key -> elem -> bool) -> t -> t
+
+ val partition : (key -> elem -> bool) -> t -> t * t
+
+ val cardinal : t -> int
+
+ val bindings : t -> (key * elem) list
+
+ val min_binding : t -> key * elem
+
+ val min_binding_opt : t -> (key * elem) option
+
+ val max_binding : t -> key * elem
+
+ val max_binding_opt : t -> (key * elem) option
+
+ val choose : t -> key * elem
+
+ val choose_opt : t -> (key * elem) option
+
+ val split : key -> t -> t * elem option * t
+
+ val find : key -> t -> elem
+
+ val find_opt : key -> t -> elem option
+
+ val find_first : (key -> bool) -> t -> key * elem
+
+ val find_first_opt : (key -> bool) -> t -> (key * elem) option
+
+ val find_last : (key -> bool) -> t -> key * elem
+
+ val find_last_opt : (key -> bool) -> t -> (key * elem) option
+
+ val to_seq : t -> (key * elem) Seq.t
+
+ val to_seq_from : key -> t -> (key * elem) Seq.t
+
+ val add_seq : (key * elem) Seq.t -> t -> t
+
+ val of_seq : (key * elem) Seq.t -> t
+end
+
+(** See [MapInj] *)
+module MakeMapInj (Key : OrderedType) (Elem : OrderedType) :
+ MapInj with type key = Key.t with type elem = Elem.t = struct
+ module Map = MakeMap (Key)
+ module Set = MakeSet (Elem)
+
+ type key = Key.t
+
+ type elem = Elem.t
+
+ type t = { map : elem Map.t; elems : Set.t }
+
+ let empty = { map = Map.empty; elems = Set.empty }
+
+ let is_empty m = Map.is_empty m.map
+
+ let mem k m = Map.mem k m.map
+
+ let add k e m =
+ assert (not (Set.mem e m.elems));
+ { map = Map.add k e m.map; elems = Set.add e m.elems }
+
+ let singleton k e = { map = Map.singleton k e; elems = Set.singleton e }
+
+ let remove k m =
+ match Map.find_opt k m.map with
+ | None -> m
+ | Some x -> { map = Map.remove k m.map; elems = Set.remove x m.elems }
+
+ let compare f m1 m2 = Map.compare f m1.map m2.map
+
+ let equal f m1 m2 = Map.equal f m1.map m2.map
+
+ let iter f m = Map.iter f m.map
+
+ let fold f m x = Map.fold f m.map x
+
+ let for_all f m = Map.for_all f m.map
+
+ let exists f m = Map.exists f m.map
+
+ (** Small helper *)
+ let bindings_to_elems_set (bls : (key * elem) list) : Set.t =
+ let elems = List.map snd bls in
+ let elems = List.fold_left (fun s e -> Set.add e s) Set.empty elems in
+ elems
+
+ (** Small helper *)
+ let map_to_elems_set (map : elem Map.t) : Set.t =
+ bindings_to_elems_set (Map.bindings map)
+
+ (** Small helper *)
+ let map_to_t (map : elem Map.t) : t =
+ let elems = map_to_elems_set map in
+ { map; elems }
+
+ let filter f m =
+ let map = Map.filter f m.map in
+ let elems = map_to_elems_set map in
+ { map; elems }
+
+ let partition f m =
+ let map1, map2 = Map.partition f m.map in
+ (map_to_t map1, map_to_t map2)
+
+ let cardinal m = Map.cardinal m.map
+
+ let bindings m = Map.bindings m.map
+
+ let min_binding m = Map.min_binding m.map
+
+ let min_binding_opt m = Map.min_binding_opt m.map
+
+ let max_binding m = Map.max_binding m.map
+
+ let max_binding_opt m = Map.max_binding_opt m.map
+
+ let choose m = Map.choose m.map
+
+ let choose_opt m = Map.choose_opt m.map
+
+ let split k m =
+ let l, data, r = Map.split k m.map in
+ let l = map_to_t l in
+ let r = map_to_t r in
+ (l, data, r)
+
+ let find k m = Map.find k m.map
+
+ let find_opt k m = Map.find_opt k m.map
+
+ let find_first k m = Map.find_first k m.map
+
+ let find_first_opt k m = Map.find_first_opt k m.map
+
+ let find_last k m = Map.find_last k m.map
+
+ let find_last_opt k m = Map.find_last_opt k m.map
+
+ let to_seq m = Map.to_seq m.map
+
+ let to_seq_from k m = Map.to_seq_from k m.map
+
+ let rec add_seq s m =
+ (* Note that it is important to check that we don't add bindings mapping
+ * to the same element *)
+ match s () with
+ | Seq.Nil -> m
+ | Seq.Cons ((k, e), s) ->
+ let m = add k e m in
+ add_seq s m
+
+ let of_seq s = add_seq s empty
+end
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index f2b88fd4..4880a19a 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -147,6 +147,21 @@ module IdGen () : Id = struct
module Map = C.MakeMap (Ord)
end
-type name = string list [@@deriving show]
+type name = string list [@@deriving show, ord]
(** A name such as: `std::collections::vector` (which would be represented as
[["std"; "collections"; "vector"]]) *)
+
+module NameOrderedType : C.OrderedType = struct
+ type t = name
+
+ let compare = compare_name
+
+ let to_string = String.concat "::"
+
+ let pp_t = pp_name
+
+ let show_t = show_name
+end
+
+module NameMap = C.MakeMap (NameOrderedType)
+module NameSet = C.MakeSet (NameOrderedType)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
new file mode 100644
index 00000000..7792db4b
--- /dev/null
+++ b/src/SymbolicToPure.ml
@@ -0,0 +1,91 @@
+open Errors
+module Id = Identifiers
+module T = Types
+module V = Values
+module E = Expressions
+module A = CfimAst
+module S = SymbolicAst
+
+type name =
+ | FunName of A.FunDefId.id * V.BackwardFunctionId.id option
+ | TypeName of T.TypeDefId.id
+[@@deriving show, ord]
+
+let name_to_string (n : name) : string = show_name n
+
+module NameOrderedType = struct
+ type t = name
+
+ let compare = compare_name
+
+ let to_string = name_to_string
+
+ let pp_t = pp_name
+
+ let show_t = show_name
+end
+
+module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType)
+(** Notice that we use the *injective* map to map identifiers to names.
+
+ Of course, even if those names (which are string lists) don't collide,
+ when converting them to strings we can still introduce collisions: we
+ check that later.
+
+ Note that we use injective maps for sanity: though we write the name
+ generation with collision in mind, it is always good to have such checks.
+ *)
+
+let fun_to_name (fdef : A.fun_def) (bid : V.BackwardFunctionId.id option) :
+ Id.name =
+ let sg = fdef.signature in
+ (* General function to generate a suffix for a region group
+ * (i.e., an abstraction)*)
+ let rg_to_string (rg : T.region_var_group) : string =
+ (* We are just a little bit smart:
+ - if there is exactly one region id in the region group and this region
+ has a name, we use this name
+ - otherwise, we use the region number (note that region names shouldn't
+ start with numbers)
+ *)
+ match rg.T.regions with
+ | [ rid ] -> (
+ let rvar = T.RegionVarId.nth sg.region_params rid in
+ match rvar.name with
+ | None -> T.RegionGroupId.to_string rg.T.id
+ | Some name -> name)
+ | _ -> T.RegionGroupId.to_string rg.T.id
+ in
+ (* There are several cases:
+ - this is a forward function: we add "_fwd"
+ - this is a backward function:
+ - this function has one backward function: we add "_back"
+ - this function has several backward function: we add "_back" and an
+ additional suffix to identify the precise backward function
+ *)
+ let suffix =
+ match bid with
+ | None -> "_fwd"
+ | Some bid -> (
+ match sg.regions_hierarchy with
+ | [] ->
+ failwith "Unreachable"
+ (* we can't get there if we ask for a back function *)
+ | [ _ ] ->
+ (* Exactly one backward function *)
+ "_back"
+ | _ ->
+ (* Several backward functions - note that **we use the backward function id
+ * as if it were a region group id** (there is a direct mapping between the
+ * two - TODO: merge them) *)
+ let rg = V.BackwardFunctionId.nth sg.regions_hierarchy bid in
+ "_back" ^ rg_to_string rg)
+ in
+ (* Final name *)
+ let rec add_to_last (n : Id.name) : Id.name =
+ match n with
+ | [] -> failwith "Unreachable"
+ | [ x ] -> [ x ^ suffix ]
+ | x :: n -> x :: add_to_last n
+ in
+ add_to_last fdef.name
diff --git a/src/main.ml b/src/main.ml
index 3772e7ac..67db362e 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -9,6 +9,7 @@ module TA = TypesAnalysis
module P = Pure
open SymbolicAstUtils
open PrintSymbolicAst
+open SymbolicToPure
(* This is necessary to have a backtrace when raising exceptions - for some
* reason, the -g option doesn't work.