Merge pull request #54 from AeneasVerif/son_closures

Add support for function pointers and closures

Makefile

@@ -4,7 +4,7 @@ ifeq (3.81,$(MAKE_VERSION))
 endif
 
 .PHONY: default
-default: build
+default: build-charon-rust
 
 .PHONY: all
 all: build tests nix

charon-ml/name_matcher_parser/Ast.ml

@@ -16,6 +16,7 @@ type literal = LInt of big_int | LBool of bool | LChar of char
 type ref_kind = RMut | RShared [@@deriving show, ord]
 type region = RVar of var option | RStatic [@@deriving show, ord]
 type primitive_adt = TTuple | TArray | TSlice [@@deriving show, ord]
+type mutability = Mut | Not [@@deriving show, ord]
 
 type pattern = pattern_elem list
 and pattern_elem = PIdent of string * generic_args | PImpl of expr
@@ -33,7 +34,9 @@ and expr =
        *)
   | EPrimAdt of primitive_adt * generic_args
   | ERef of region * expr * ref_kind
+  | EArrow of expr list * expr option
   | EVar of var option
+  | ERawPtr of mutability * expr
 
 and generic_arg = GExpr of expr | GValue of literal | GRegion of region
 and generic_args = generic_arg list [@@deriving show, ord]

charon-ml/name_matcher_parser/Lexer.mll

@@ -12,6 +12,8 @@ let whitespace = [' ']+
 rule token = parse
   | "::" { SEP }
   | "mut" { MUT }
+  | "const" { CONST }
+  | "fn" { FN }
   | "'static" { STATIC_REGION }
   | ''' { REGION (index lexbuf) }
   | "true" { TRUE }
@@ -31,7 +33,9 @@ rule token = parse
   | eof { EOF }
   | '<' { LEFT_ANGLE }
   | '>' { RIGHT_ANGLE }
-  | ',' { COMMA } 
+  | ',' { COMMA }
+  | "->" { ARROW }
+  | '*' { STAR }
   | _ { raise (Failure ("Character not allowed in source text: '" ^ Lexing.lexeme lexbuf ^ "'")) }
 
 and index = parse

charon-ml/name_matcher_parser/Parser.mly

@@ -12,7 +12,7 @@ open Ast
 %token LEFT_CURLY RIGHT_CURLY
 %token LEFT_SQUARE RIGHT_SQUARE
 %token LEFT_ANGLE RIGHT_ANGLE
-%token SEMICOL AMPERSAND MUT COMMA EOF
+%token SEMICOL AMPERSAND MUT CONST COMMA EOF FN ARROW STAR
 
 /* Types */
 
@@ -64,6 +64,16 @@ expr:
       ERef (r, ty, RShared) }
   // Variables
   | v=VAR { EVar v }
+  // Arrows
+  | FN; LEFT_BRACKET; inputs=separated_list(COMMA, expr); RIGHT_BRACKET; ARROW; ret=expr {
+    EArrow (inputs, Some ret) }
+  | FN; LEFT_BRACKET; inputs=separated_list(COMMA, expr); RIGHT_BRACKET {
+    EArrow (inputs, None) }
+  // Raw pointers
+  | STAR; MUT; ty=expr {
+    ERawPtr (Mut, ty) }
+  | STAR; CONST; ty=expr {
+    ERawPtr (Not, ty) }
   ;
 
 region:

charon-ml/src/Expressions.ml

@@ -3,7 +3,7 @@ open Types
 open Values
 module VarId = IdGen ()
 module GlobalDeclId = Types.GlobalDeclId
-module FunDeclId = IdGen ()
+module FunDeclId = Types.FunDeclId
 
 type fun_decl_id = FunDeclId.id [@@deriving show, ord]
 
@@ -130,7 +130,6 @@ class ['self] iter_constant_expr_base =
   object (_self : 'self)
     inherit [_] iter_place
     inherit! [_] iter_ty
-    method visit_fun_decl_id : 'env -> fun_decl_id -> unit = fun _ _ -> ()
     method visit_assumed_fun_id : 'env -> assumed_fun_id -> unit = fun _ _ -> ()
   end
 
@@ -139,14 +138,14 @@ class ['self] map_constant_expr_base =
   object (_self : 'self)
     inherit [_] map_place
     inherit! [_] map_ty
-    method visit_fun_decl_id : 'env -> fun_decl_id -> fun_decl_id = fun _ x -> x
 
     method visit_assumed_fun_id : 'env -> assumed_fun_id -> assumed_fun_id =
       fun _ x -> x
   end
 
-(* TODO: FnPtr *)
-type cast_kind = CastInteger of integer_type * integer_type
+type cast_kind =
+  | CastInteger of integer_type * integer_type
+  | CastFnPtr of ty * ty
 
 (* Remark: no `ArrayToSlice` variant: it gets eliminated in a micro-pass. *)
 and unop =
@@ -238,6 +237,7 @@ type operand = Copy of place | Move of place | Constant of constant_expr
 and aggregate_kind =
   | AggregatedAdt of type_id * variant_id option * generic_args
   | AggregatedArray of ty * const_generic
+  | AggregatedClosure of fun_decl_id * generic_args
 
 (* TODO: move the aggregate kind to operands *)
 (* TODO: we should prefix the type variants with "T", this would avoid collisions *)

charon-ml/src/GAst.ml

@@ -44,8 +44,9 @@ class ['self] map_ast_base =
 (* Below: the types need not be mutually recursive, but it makes it easier
    to derive the visitors *)
 type assertion = { cond : operand; expected : bool }
+and fn_operand = FnOpRegular of fn_ptr | FnOpMove of place
 
-and call = { func : fn_ptr; args : operand list; dest : place }
+and call = { func : fn_operand; args : operand list; dest : place }
 [@@deriving
   show,
     visitors
@@ -88,9 +89,14 @@ type params_info = {
 }
 [@@deriving show]
 
+type closure_kind = Fn | FnMut | FnOnce [@@deriving show]
+type closure_info = { kind : closure_kind; state : ty list } [@@deriving show]
+
 (** A function signature for function declarations *)
 type fun_sig = {
   is_unsafe : bool;
+  is_closure : bool;
+  closure_info : closure_info option;
   generics : generic_params;
   preds : predicates;
   parent_params_info : params_info option;

charon-ml/src/GAstOfJson.ml

@@ -130,7 +130,7 @@ let region_var_of_json (js : json) : (region_var, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("index", index); ("name", name) ] ->
-        let* index = RegionId.id_of_json index in
+        let* index = RegionVarId.id_of_json index in
         let* name = string_option_of_json name in
         Ok { index; name }
     | _ -> Error "")
@@ -140,9 +140,10 @@ let region_of_json (js : json) : (region, string) result =
     (match js with
     | `String "Static" -> Ok RStatic
     | `String "Erased" -> Ok RErased
-    | `Assoc [ ("Var", rid) ] ->
-        let* rid = RegionId.id_of_json rid in
-        Ok (RVar rid : region)
+    | `Assoc [ ("BVar", `List [ dbid; rid ]) ] ->
+        let* dbid = int_of_json dbid in
+        let* rid = RegionVarId.id_of_json rid in
+        Ok (RBVar (dbid, rid) : region)
     | _ -> Error "")
 
 let integer_type_of_json (js : json) : (integer_type, string) result =
@@ -330,10 +331,11 @@ let rec ty_of_json (js : json) : (ty, string) result =
         let* generics = generic_args_of_json generics in
         let* item_name = string_of_json item_name in
         Ok (TTraitType (trait_ref, generics, item_name))
-    | `Assoc [ ("Arrow", `List [ inputs; output ]) ] ->
+    | `Assoc [ ("Arrow", `List [ regions; inputs; output ]) ] ->
+        let* regions = list_of_json region_var_of_json regions in
         let* inputs = list_of_json ty_of_json inputs in
         let* output = ty_of_json output in
-        Ok (TArrow (inputs, output))
+        Ok (TArrow (regions, inputs, output))
     | _ -> Error "")
 
 and trait_ref_of_json (js : json) : (trait_ref, string) result =
@@ -407,6 +409,10 @@ and trait_instance_id_of_json (js : json) : (trait_instance_id, string) result =
     | `Assoc [ ("FnPointer", ty) ] ->
         let* ty = ty_of_json ty in
         Ok (FnPointer ty)
+    | `Assoc [ ("Closure", `List [ fid; generics ]) ] ->
+        let* fid = FunDeclId.id_of_json fid in
+        let* generics = generic_args_of_json generics in
+        Ok (Closure (fid, generics))
     | _ -> Error "")
 
 let field_of_json (id_to_file : id_to_file_map) (js : json) :
@@ -444,17 +450,17 @@ let type_decl_kind_of_json (id_to_file : id_to_file_map) (js : json) :
     | `String "Opaque" -> Ok Opaque
     | _ -> Error "")
 
-let region_var_group_of_json (js : json) : (region_group, string) result =
+let region_var_group_of_json (js : json) : (region_var_group, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] ->
         let* id = RegionGroupId.id_of_json id in
-        let* regions = list_of_json RegionId.id_of_json regions in
+        let* regions = list_of_json RegionVarId.id_of_json regions in
         let* parents = list_of_json RegionGroupId.id_of_json parents in
         Ok { id; regions; parents }
     | _ -> Error "")
 
-let region_var_groups_of_json (js : json) : (region_groups, string) result =
+let region_var_groups_of_json (js : json) : (region_var_groups, string) result =
   combine_error_msgs js __FUNCTION__ (list_of_json region_var_group_of_json js)
 
 let trait_clause_of_json (id_to_file : id_to_file_map) (js : json) :
@@ -674,6 +680,10 @@ let cast_kind_of_json (js : json) : (cast_kind, string) result =
         let* src_ty = integer_type_of_json src_ty in
         let* tgt_ty = integer_type_of_json tgt_ty in
         Ok (CastInteger (src_ty, tgt_ty))
+    | `Assoc [ ("FnPtr", `List [ src_ty; tgt_ty ]) ] ->
+        let* src_ty = ty_of_json src_ty in
+        let* tgt_ty = ty_of_json tgt_ty in
+        Ok (CastFnPtr (src_ty, tgt_ty))
     | _ -> Error "")
 
 let unop_of_json (js : json) : (unop, string) result =
@@ -775,6 +785,17 @@ let fn_ptr_of_json (js : json) : (fn_ptr, string) result =
         Ok { func; generics; trait_and_method_generic_args }
     | _ -> Error "")
 
+let fn_operand_of_json (js : json) : (fn_operand, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("Regular", func) ] ->
+        let* func = fn_ptr_of_json func in
+        Ok (FnOpRegular func)
+    | `Assoc [ ("Move", p) ] ->
+        let* p = place_of_json p in
+        Ok (FnOpMove p)
+    | _ -> Error "")
+
 let rec constant_expr_of_json (js : json) : (constant_expr, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -831,6 +852,10 @@ let aggregate_kind_of_json (js : json) : (aggregate_kind, string) result =
         let* ty = ty_of_json ty in
         let* cg = const_generic_of_json cg in
         Ok (AggregatedArray (ty, cg))
+    | `Assoc [ ("Closure", `List [ fid; generics ]) ] ->
+        let* fid = FunDeclId.id_of_json fid in
+        let* generics = generic_args_of_json generics in
+        Ok (AggregatedClosure (fid, generics))
     | _ -> Error "")
 
 let rvalue_of_json (js : json) : (rvalue, string) result =
@@ -898,35 +923,67 @@ let params_info_of_json (js : json) : (params_info, string) result =
           }
     | _ -> Error "")
 
+let closure_kind_of_json (js : json) : (closure_kind, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `String "Fn" -> Ok Fn
+    | `String "FnMut" -> Ok FnMut
+    | `String "FnOnce" -> Ok FnOnce
+    | _ -> Error "")
+
+let closure_info_of_json (js : json) : (closure_info, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("kind", kind); ("state", state) ] ->
+        let* kind = closure_kind_of_json kind in
+        let* state = list_of_json ty_of_json state in
+        Ok { kind; state }
+    | _ -> Error "")
+
 let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) :
     (fun_sig, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
         [
           ("is_unsafe", is_unsafe);
+          ("is_closure", is_closure);
+          ("closure_info", closure_info);
           ("generics", generics);
           ("preds", preds);
           ("parent_params_info", parent_params_info);
           ("inputs", inputs);
           ("output", output);
         ] ->
         let* is_unsafe = bool_of_json is_unsafe in
+        let* is_closure = bool_of_json is_closure in
+        let* closure_info = option_of_json closure_info_of_json closure_info in
+
         let* generics = generic_params_of_json id_to_file generics in
         let* preds = predicates_of_json preds in
         let* parent_params_info =
           option_of_json params_info_of_json parent_params_info
         in
         let* inputs = list_of_json ty_of_json inputs in
         let* output = ty_of_json output in
-        Ok { is_unsafe; generics; preds; parent_params_info; inputs; output }
+        Ok
+          {
+            is_unsafe;
+            is_closure;
+            closure_info;
+            generics;
+            preds;
+            parent_params_info;
+            inputs;
+            output;
+          }
     | _ -> Error "")
 
 let call_of_json (js : json) : (call, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("func", func); ("args", args); ("dest", dest) ] ->
-        let* func = fn_ptr_of_json func in
+        let* func = fn_operand_of_json func in
         let* args = list_of_json operand_of_json args in
         let* dest = place_of_json dest in
         Ok { func; args; dest }

charon-ml/src/GAstUtils.ml

@@ -6,7 +6,7 @@ open GAst
 
     This list *doesn't* include the current region.
  *)
-let rec list_ancestor_region_groups (regions_hierarchy : region_groups)
+let rec list_ancestor_region_groups (regions_hierarchy : region_var_groups)
     (gid : RegionGroupId.id) : RegionGroupId.Set.t =
   let rg = RegionGroupId.nth regions_hierarchy gid in
   let parents =
@@ -23,15 +23,15 @@ let rec list_ancestor_region_groups (regions_hierarchy : region_groups)
   parents
 
 (** Small utility: same as {!list_ancestor_region_groups}, but returns an ordered list.  *)
-let list_ordered_ancestor_region_groups (regions_hierarchy : region_groups)
+let list_ordered_ancestor_region_groups (regions_hierarchy : region_var_groups)
     (gid : RegionGroupId.id) : RegionGroupId.id list =
   let pset = list_ancestor_region_groups regions_hierarchy gid in
   let parents =
     List.filter
-      (fun (rg : region_group) -> RegionGroupId.Set.mem rg.id pset)
+      (fun (rg : region_var_group) -> RegionGroupId.Set.mem rg.id pset)
       regions_hierarchy
   in
-  let parents = List.map (fun (rg : region_group) -> rg.id) parents in
+  let parents = List.map (fun (rg : region_var_group) -> rg.id) parents in
   parents
 
 let gexpr_body_get_input_vars (fbody : 'body gexpr_body) : var list =

charon-ml/src/LlbcOfJson.ml

@@ -139,6 +139,8 @@ let global_decl_of_json (id_to_file : id_to_file_map) (js : json)
        {
          (* Not sure about `is_unsafe` actually *)
          is_unsafe = false;
+         is_closure = false;
+         closure_info = None;
          generics = TypesUtils.empty_generic_params;
          preds = TypesUtils.empty_predicates;
          parent_params_info = None;

charon-ml/src/Logging.ml

@@ -151,3 +151,8 @@ let main_logger_handler =
   match handlers with
   | [ handler ] -> handler
   | _ -> raise (Failure "Unexpected")
+
+(*
+ * Subloggers
+ *)
+let name_matcher_logger = L.get_logger "NameMatcher"