Merge pull request #48 from AeneasVerif/son_closures

Prepare support for function pointers and closures

compiler/AssociatedTypes.ml

@@ -92,7 +92,8 @@ let ctx_add_norm_trait_types_from_preds (ctx : eval_ctx)
 let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool =
   match id with
   | Self | Clause _ -> true
-  | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _ ->
+  | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _
+  | Closure _ ->
       false
   | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
       trait_instance_id_is_local_clause id
@@ -118,13 +119,10 @@ let norm_ctx_to_fmt_env (ctx : norm_ctx) : Print.fmt_env =
     global_decls = ctx.global_decls;
     trait_decls = ctx.trait_decls;
     trait_impls = ctx.trait_impls;
-    generics =
-      {
-        types = ctx.type_vars;
-        const_generics = ctx.const_generic_vars;
-        regions = [];
-        trait_clauses = [];
-      };
+    types = ctx.type_vars;
+    const_generics = ctx.const_generic_vars;
+    regions = [];
+    trait_clauses = [];
     preds = empty_predicates;
     locals = [];
   }
@@ -220,10 +218,13 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
   | TRawPtr (ty, rkind) ->
       let ty = norm_ctx_normalize_ty ctx ty in
       TRawPtr (ty, rkind)
-  | TArrow (inputs, output) ->
+  | TArrow (regions, inputs, output) ->
+      (* TODO: for now it works because we don't support predicates with
+         bound regions. If we do support them, we probably need to do
+         something smarter here. *)
       let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in
       let output = norm_ctx_normalize_ty ctx output in
-      TArrow (inputs, output)
+      TArrow (regions, inputs, output)
   | TTraitType (trait_ref, generics, type_name) -> (
       log#ldebug
         (lazy
@@ -429,6 +430,9 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
       (* TODO: we might want to return the ref to the function pointer,
          in order to later normalize a call to this function pointer *)
       (FnPointer ty, None)
+  | Closure (fid, generics) ->
+      let generics = norm_ctx_normalize_generic_args ctx generics in
+      (Closure (fid, generics), None)
   | UnknownTrait _ ->
       (* This is actually an error case *)
       (id, None)
@@ -562,11 +566,11 @@ let ctx_adt_get_inst_norm_field_etypes (ctx : eval_ctx) (def_id : TypeDeclId.id)
 (** Same as [substitute_signature] but normalizes the types *)
 let ctx_subst_norm_signature (ctx : eval_ctx)
     (asubst : RegionGroupId.id -> AbstractionId.id)
-    (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (r_subst : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
     (cg_subst : ConstGenericVarId.id -> const_generic)
     (tr_subst : TraitClauseId.id -> trait_instance_id)
     (tr_self : trait_instance_id) (sg : fun_sig)
-    (regions_hierarchy : region_groups) : inst_fun_sig =
+    (regions_hierarchy : region_var_groups) : inst_fun_sig =
   let sg =
     Subst.substitute_signature asubst r_subst ty_subst cg_subst tr_subst tr_self
       sg regions_hierarchy

compiler/Assumed.ml

@@ -36,8 +36,8 @@ open LlbcAst
 module Sig = struct
   (** A few utilities *)
 
-  let rvar_id_0 = RegionId.of_int 0
-  let rvar_0 : region = RVar rvar_id_0
+  let rvar_id_0 = RegionVarId.of_int 0
+  let rvar_0 : region = RBVar (0, rvar_id_0)
   let rg_id_0 = RegionGroupId.of_int 0
   let tvar_id_0 = TypeVarId.of_int 0
   let tvar_0 : ty = TVar tvar_id_0
@@ -48,7 +48,7 @@ module Sig = struct
   let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" }
 
   (** Region group: [{ parent={}; regions:{'a of id 0} }] *)
-  let region_group_0 : region_group =
+  let region_group_0 : region_var_group =
     { id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] }
 
   (** Type parameter [T] of id 0 *)
@@ -84,6 +84,8 @@ module Sig = struct
     in
     {
       is_unsafe = false;
+      is_closure = false;
+      closure_info = None;
       generics;
       preds;
       parent_params_info = None;

compiler/Contexts.ml

@@ -190,7 +190,7 @@ type type_context = {
 type fun_context = {
   fun_decls : fun_decl FunDeclId.Map.t;
   fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
-  regions_hierarchies : region_groups FunIdMap.t;
+  regions_hierarchies : region_var_groups FunIdMap.t;
 }
 [@@deriving show]
 
@@ -241,7 +241,11 @@ type eval_ctx = {
   const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
-          if we run in interpreter mode) *)
+          if we run in interpreter mode).
+
+          TODO: this is actually not used in symbolic mode, where we
+          directly introduce fresh symbolic values.
+       *)
   norm_trait_types : ty TraitTypeRefMap.t;
       (** The normalized trait types (a map from trait types to their representatives).
           Note that this doesn't take into account higher-order type constraints

compiler/ExtractBase.ml

@@ -1984,7 +1984,7 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
         let rg = T.RegionGroupId.nth regions_hierarchy rg_id in
         let region_names =
           List.map
-            (fun rid -> (T.RegionId.nth sg.generics.regions rid).name)
+            (fun rid -> (T.RegionVarId.nth sg.generics.regions rid).name)
             rg.regions
         in
         Some { id = rg_id; region_names }

compiler/ExtractName.ml

@@ -3,13 +3,14 @@
 open Charon.NameMatcher
 
 let log = Logging.extract_log
+let match_with_trait_decl_refs = true
 
 module NameMatcherMap = struct
   module NMM = NameMatcherMap
 
   type 'a t = 'a NMM.t
 
-  let config = { map_vars_to_vars = true }
+  let config = { map_vars_to_vars = true; match_with_trait_decl_refs }
 
   let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option =
     NMM.find_opt ctx config name m
@@ -61,7 +62,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
               | TArray -> "Array"
               | TSlice -> "Slice"
             else expr_to_string c ty
-        | ERef _ | EVar _ ->
+        | ERef _ | EVar _ | EArrow _ | ERawPtr _ ->
             (* We simply convert the pattern to a string. This is not very
                satisfying but we should rarely get there. *)
             expr_to_string c ty)
@@ -85,25 +86,29 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
    consistent with the extraction names we derive from the Rust names *)
 let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) :
     string list =
-  let c : to_pat_config = { tgt = TkName } in
+  let c : to_pat_config =
+    { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
   pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n)
 
 (** If the [prefix] is Some, we attempt to remove the common prefix
     between [prefix] and [name] from [name] *)
 let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
     ?(prefix : Types.name option = None) (name : Types.name)
     (p : Types.generic_params) (g : Types.generic_args) : string list =
-  let c : to_pat_config = { tgt = TkName } in
-  let name = name_with_generics_to_pattern ctx c name p g in
+  let c : to_pat_config =
+    { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let name = name_with_generics_to_pattern ctx c p name g in
   let name =
     match prefix with
     | None -> name
     | Some prefix ->
         let prefix =
-          name_with_generics_to_pattern ctx c prefix
-            TypesUtils.empty_generic_params TypesUtils.empty_generic_args
+          name_with_generics_to_pattern ctx c TypesUtils.empty_generic_params
+            prefix TypesUtils.empty_generic_args
         in
-        let _, _, name = pattern_common_prefix prefix name in
+        let _, _, name = pattern_common_prefix { equiv = true } prefix name in
         name
   in
   pattern_to_extract_name is_trait_impl name

compiler/FunsAnalysis.ml

@@ -62,7 +62,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
       {
         type_decls = m.type_decls;
         global_decls = m.global_decls;
+        fun_decls = m.fun_decls;
         trait_decls = m.trait_decls;
+        trait_impls = m.trait_impls;
       }
     in
 
@@ -84,6 +86,16 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
           method may_fail b = can_fail := !can_fail || b
           method maybe_stateful b = stateful := !stateful || b
 
+          method visit_fid id =
+            if FunDeclId.Set.mem id fun_ids then (
+              can_diverge := true;
+              is_rec := true)
+            else
+              let info = FunDeclId.Map.find id !infos in
+              self#may_fail info.can_fail;
+              stateful := !stateful || info.stateful;
+              can_diverge := !can_diverge || info.can_diverge
+
           method! visit_Assert env a =
             self#may_fail true;
             super#visit_Assert env a
@@ -95,25 +107,32 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
             | BinaryOp (bop, _, _) ->
                 can_fail := binop_can_fail bop || !can_fail
 
+          method! visit_Closure env id args =
+            (* Remark: `Closure` is a trait instance id - TODO: rename this variant *)
+            self#visit_fid id;
+            super#visit_Closure env id args
+
+          method! visit_AggregatedClosure env id args =
+            self#visit_fid id;
+            super#visit_AggregatedClosure env id args
+
           method! visit_Call env call =
-            (match call.func.func with
-            | FunId (FRegular id) ->
-                if FunDeclId.Set.mem id fun_ids then (
-                  can_diverge := true;
-                  is_rec := true)
-                else
-                  let info = FunDeclId.Map.find id !infos in
-                  self#may_fail info.can_fail;
-                  stateful := !stateful || info.stateful;
-                  can_diverge := !can_diverge || info.can_diverge
-            | FunId (FAssumed id) ->
-                (* None of the assumed functions can diverge nor are considered stateful *)
-                can_fail := !can_fail || Assumed.assumed_fun_can_fail id
-            | TraitMethod _ ->
-                (* We consider trait functions can fail, but can not diverge and are not stateful.
-                   TODO: this may cause issues if we use use a fuel parameter.
-                *)
-                can_fail := true);
+            (match call.func with
+            | FnOpMove _ ->
+                (* Ignoring this: we lookup the called function upon creating
+                   the closure *)
+                ()
+            | FnOpRegular func -> (
+                match func.func with
+                | FunId (FRegular id) -> self#visit_fid id
+                | FunId (FAssumed id) ->
+                    (* None of the assumed functions can diverge nor are considered stateful *)
+                    can_fail := !can_fail || Assumed.assumed_fun_can_fail id
+                | TraitMethod _ ->
+                    (* We consider trait functions can fail, but can not diverge and are not stateful.
+                       TODO: this may cause issues if we use use a fuel parameter.
+                    *)
+                    can_fail := true));
             super#visit_Call env call
 
           method! visit_Panic env =

compiler/Interpreter.ml

@@ -68,7 +68,7 @@ let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
 let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
-    (regions_hierarchy : region_groups) (kind : fun_kind) :
+    (regions_hierarchy : region_var_groups) (kind : fun_kind) :
     eval_ctx * inst_fun_sig =
   let tr_self =
     match kind with
@@ -192,7 +192,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
   in
   let region_groups =
-    List.map (fun (g : region_group) -> g.id) regions_hierarchy
+    List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
     initialize_eval_context ctx region_groups sg.generics.types

compiler/InterpreterBorrows.ml

@@ -448,8 +448,8 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
   | SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
     ->
       ()
-  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate
-  | ConstGeneric | TraitConst ->
+  | FunCallRet | SynthInput | Global | KindConstGeneric | LoopOutput | LoopJoin
+  | Aggregate | ConstGeneric | TraitConst ->
       raise (Failure "Unreachable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
@@ -1870,15 +1870,15 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
         match bc with
         | VSharedBorrow bid ->
             assert (ty_no_regions ref_ty);
-            let ty = TRef (RVar r_id, ref_ty, kind) in
+            let ty = TRef (RFVar r_id, ref_ty, kind) in
             let value = ABorrow (ASharedBorrow bid) in
             ([ { value; ty } ], v)
         | VMutBorrow (bid, bv) ->
             let r_id = if group then r_id else fresh_region_id () in
             (* We don't support nested borrows for now *)
             assert (not (value_has_borrows ctx bv.value));
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
-            let ty = TRef (RVar r_id, ref_ty, kind) in
+            let ty = TRef (RFVar r_id, ref_ty, kind) in
             let ignored = mk_aignored ref_ty in
             let av = ABorrow (AMutBorrow (bid, ignored)) in
             let av = { value = av; ty } in
@@ -1899,7 +1899,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
             assert (ty_no_regions ty);
-            let ty = mk_ref_ty (RVar r_id) ty RShared in
+            let ty = mk_ref_ty (RFVar r_id) ty RShared in
             let ignored = mk_aignored ty in
             (* Rem.: the shared value might contain loans *)
             let avl, sv = to_avalues false true true r_id sv in
@@ -1917,7 +1917,7 @@ let convert_value_to_abstractions (abs_kind : abs_kind) (can_end : bool)
             (* Push the avalue - note that we use [AIgnore] for the inner avalue *)
             (* For avalues, a loan has the borrow type *)
             assert (ty_no_regions ty);
-            let ty = mk_ref_ty (RVar r_id) ty RMut in
+            let ty = mk_ref_ty (RFVar r_id) ty RMut in
             let ignored = mk_aignored ty in
             let av = ALoan (AMutLoan (bid, ignored)) in
             let av = { value = av; ty } in

compiler/InterpreterExpressions.ml

@@ -300,13 +300,29 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                          e ))))
       | CVar vid -> (
           let ctx0 = ctx in
-          (* Lookup the const generic value *)
-          let cv = ctx_lookup_const_generic_value ctx vid in
-          (* Copy the value *)
-          let allow_adt_copy = false in
-          let ctx, v = copy_value allow_adt_copy config ctx cv in
+          (* In concrete mode: lookup the const generic value.
+             In symbolic mode: introduce a fresh symbolic value.
+
+             We have nothing to do: the value is copyable, so we can freely
+             duplicate it.
+          *)
+          let ctx, cv =
+            let cv = ctx_lookup_const_generic_value ctx vid in
+            match config.mode with
+            | ConcreteMode ->
+                (* Copy the value - this is more of a sanity check *)
+                let allow_adt_copy = false in
+                copy_value allow_adt_copy config ctx cv
+            | SymbolicMode ->
+                (* We use the looked up value only for its type *)
+                let v = mk_fresh_symbolic_typed_value KindConstGeneric cv.ty in
+                (ctx, v)
+          in
           (* Continue *)
-          let e = cf v ctx in
+          let e = cf cv ctx in
+          (* If we are synthesizing a symbolic AST, it means that we are in symbolic
+             mode: the value of the const generic is necessarily symbolic. *)
+          assert (e = None || is_symbolic cv.value);
           (* We have to wrap the generated expression *)
           match e with
           | None -> None
@@ -319,7 +335,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                 (SymbolicAst.IntroSymbolic
                    ( ctx0,
                      None,
-                     value_as_symbolic v.value,
+                     value_as_symbolic cv.value,
                      SymbolicAst.VaCgValue vid,
                      e )))
       | CFnPtr _ -> raise (Failure "TODO"))
@@ -761,6 +777,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
             (* Introduce the symbolic value in the AST *)
             let sv = ValuesUtils.value_as_symbolic saggregated.value in
             Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)))
+    | AggregatedClosure _ -> raise (Failure "Closures are not supported yet")
   in
   (* Compose and apply *)
   comp eval_ops compute cf

compiler/InterpreterLoopsFixedPoint.ml

@@ -164,7 +164,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
     let child_av = mk_aignored child_rty in
 
     (* Create the shared loan *)
-    let loan_rty = TRef (RVar nrid, rty, RShared) in
+    let loan_rty = TRef (RFVar nrid, rty, RShared) in
     let loan_value =
       ALoan (ASharedLoan (BorrowId.Set.singleton nlid, nsv, child_av))
     in