Merge pull request #411 from AeneasVerif/son/borrows

Update the join for symbolic values with borrows

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-8a17efc262ef3af377ab172efc865edcf1bb40ea
+df3b7fd4c1277827c92b4a2cb84347f1f54d92a6

src/Errors.ml

@@ -113,8 +113,12 @@ let sanity_check (file : string) (line : int) b span =
 let sanity_check_opt_span (file : string) (line : int) b span =
   cassert_opt_span file line b span "Internal error, please file an issue"
 
-let internal_error (file : string) (line : int) span =
-  craise file line span "Internal error, please file an issue"
+let internal_error_opt_span (file : string) (line : int)
+    (span : Meta.span option) =
+  craise_opt_span file line span "Internal error, please file an issue"
+
+let internal_error (file : string) (line : int) (span : Meta.span) =
+  internal_error_opt_span file line (Some span)
 
 let warn_opt_span (file : string) (line : int) (span : Meta.span option)
     (msg : string) =

src/Logging.ml

@@ -1,86 +1,94 @@
 include Charon.Logging
+open Collections
 
-(** Below, we create subgloggers for various submodules, so that we can precisely
+(** Below, we create loggers for various (sub-)modules, so that we can precisely
     toggle logging on/off, depending on which information we need *)
 
+let loggers : L.logger StringMap.t ref = ref StringMap.empty
+
+let create_logger name =
+  let l = L.get_logger ("MainLogger." ^ name) in
+  loggers := StringMap.add name l !loggers;
+  l
+
 (** Logger for Errors *)
-let errors_log = L.get_logger "MainLogger.Errors"
+let errors_log = create_logger "Errors"
 
 (** Logger for PrePasses *)
-let pre_passes_log = L.get_logger "MainLogger.PrePasses"
+let pre_passes_log = create_logger "PrePasses"
 
 (** Logger for RegionsHierarchy *)
-let regions_hierarchy_log = L.get_logger "MainLogger.RegionsHierarchy"
+let regions_hierarchy_log = create_logger "RegionsHierarchy"
 
 (** Logger for Translate *)
-let translate_log = L.get_logger "MainLogger.Translate"
+let translate_log = create_logger "Translate"
 
 (** Logger for BorrowCheck *)
-let borrow_check_log = L.get_logger "MainLogger.BorrowCheck"
+let borrow_check_log = create_logger "BorrowCheck"
 
 (** Logger for Contexts *)
-let contexts_log = L.get_logger "MainLogger.Contexts"
+let contexts_log = create_logger "Contexts"
 
 (** Logger for PureUtils *)
-let pure_utils_log = L.get_logger "MainLogger.PureUtils"
+let pure_utils_log = create_logger "PureUtils"
 
 (** Logger for SymbolicToPure *)
-let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
+let symbolic_to_pure_log = create_logger "SymbolicToPure"
 
 (** Logger for PureMicroPasses *)
-let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
+let pure_micro_passes_log = create_logger "PureMicroPasses"
 
 (** Logger for PureMicroPasses.simplify_aggregates_unchanged_fields *)
 let simplify_aggregates_unchanged_fields_log =
-  L.get_logger "MainLogger.PureMicroPasses.simplify_aggregates_unchanged_fields"
+  create_logger "PureMicroPasses.simplify_aggregates_unchanged_fields"
 
 (** Logger for ExtractBase *)
-let extract_log = L.get_logger "MainLogger.ExtractBase"
+let extract_log = create_logger "ExtractBase"
 
 (** Logger for ExtractBuiltin *)
-let builtin_log = L.get_logger "MainLogger.Builtin"
+let builtin_log = create_logger "Builtin"
 
 (** Logger for Interpreter *)
-let interpreter_log = L.get_logger "MainLogger.Interpreter"
+let interpreter_log = create_logger "Interpreter"
 
 (** Logger for InterpreterLoopsMatchCtxs *)
-let loops_match_ctxs_log = L.get_logger "MainLogger.Interpreter.LoopsMatchCtxs"
+let loops_match_ctxs_log = create_logger "Interpreter.LoopsMatchCtxs"
 
 (** Logger for InterpreterLoopsJoinCtxs *)
-let loops_join_ctxs_log = L.get_logger "MainLogger.Interpreter.LoopsJoinCtxs"
+let loops_join_ctxs_log = create_logger "Interpreter.LoopsJoinCtxs"
 
 (** Logger for InterpreterLoopsFixedPoint *)
-let loops_fixed_point_log = L.get_logger "MainLogger.Interpreter.FixedPoint"
+let loops_fixed_point_log = create_logger "Interpreter.LoopsFixedPoint"
 
 (** Logger for InterpreterLoops *)
-let loops_log = L.get_logger "MainLogger.Interpreter.Loops"
+let loops_log = create_logger "Interpreter.Loops"
 
 (** Logger for InterpreterStatements *)
-let statements_log = L.get_logger "MainLogger.Interpreter.Statements"
+let statements_log = create_logger "Interpreter.Statements"
 
 (** Logger for InterpreterExpressions *)
-let expressions_log = L.get_logger "MainLogger.Interpreter.Expressions"
+let expressions_log = create_logger "Interpreter.Expressions"
 
 (** Logger for InterpreterPaths *)
-let paths_log = L.get_logger "MainLogger.Interpreter.Paths"
+let paths_log = create_logger "Interpreter.Paths"
 
 (** Logger for InterpreterExpansion *)
-let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion"
+let expansion_log = create_logger "Interpreter.Expansion"
 
 (** Logger for InterpreterProjectors *)
-let projectors_log = L.get_logger "MainLogger.Interpreter.Projectors"
+let projectors_log = create_logger "Interpreter.Projectors"
 
 (** Logger for InterpreterBorrows *)
-let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
+let borrows_log = create_logger "Interpreter.Borrows"
 
 (** Logger for Invariants *)
-let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
+let invariants_log = create_logger "Interpreter.Invariants"
 
 (** Logger for AssociatedTypes *)
-let associated_types_log = L.get_logger "MainLogger.AssociatedTypes"
+let associated_types_log = create_logger "AssociatedTypes"
 
 (** Logger for SCC *)
-let scc_log = L.get_logger "MainLogger.Graph.SCC"
+let scc_log = create_logger "Graph.SCC"
 
 (** Logger for ReorderDecls *)
-let reorder_decls_log = L.get_logger "MainLogger.Graph.ReorderDecls"
+let reorder_decls_log = create_logger "Graph.ReorderDecls"

src/Main.ml

@@ -70,6 +70,18 @@ let matches_name_with_generics (c : crate) (name : Types.name)
   let open ExtractBuiltin in
   Option.is_some (NameMatcherMap.find_with_generics_opt mctx name generics m)
 
+let activated_loggers : (EL.level * string) list ref = ref []
+
+let add_activated_loggers level (name_list : string) =
+  let names = String.split_on_char ',' name_list in
+  activated_loggers := List.map (fun n -> (level, n)) names @ !activated_loggers
+
+let marked_ids : string list ref = ref []
+
+let add_marked_ids (ids : string) =
+  let ids = String.split_on_char ',' ids in
+  marked_ids := ids @ !marked_ids
+
 let () =
   (* Measure start time *)
   let start_time = Unix.gettimeofday () in
@@ -150,6 +162,26 @@ let () =
         Arg.Set print_unknown_externals,
         " Print all the external definitions which are not listed in the \
          builtin functions" );
+      ( "-log",
+        Arg.String (add_activated_loggers EL.Trace),
+        " Activate trace log for a given logger designated by its name. It is \
+         possible to specifiy a list of names if they are separated by commas \
+         without spaces; for instance: '-log Interpreter,SymbolicToPure'. The \
+         existing loggers are: {"
+        ^ String.concat ", " (Collections.StringMap.keys !loggers)
+        ^ "}" );
+      ( "-log-debug",
+        Arg.String (add_activated_loggers EL.Debug),
+        " Same as '-log' but sets the level to the more verbose 'debug' rather \
+         than 'trace'" );
+      ( "-mark-ids",
+        Arg.String add_marked_ids,
+        " For developers: mark some identifiers to throw an exception if we \
+         generate them; this is useful to insert breakpoints when debugging by \
+         using the log. For example, one can mark the symbolic value ids 1 and \
+         2 with '-mark-ids s1,s2', or '-mark-ids s@1, s@2. The supported \
+         prefixes are: 's' (symbolic value id), 'b' (borrow id), 'a' \
+         (abstraction id), 'r' (region id)." );
     ]
   in
 
@@ -211,6 +243,58 @@ let () =
     if cond then fail_with_error msg
   in
 
+  (* Activate the loggers *)
+  let activated_loggers_set = ref Collections.StringSet.empty in
+  List.iter
+    (fun (level, name) ->
+      match Collections.StringMap.find_opt name !loggers with
+      | None ->
+          log#serror
+            ("The logger '" ^ name
+           ^ "' does not exist. The existing loggers are: {"
+            ^ String.concat ", " (Collections.StringMap.keys !loggers)
+            ^ "}");
+          fail false
+      | Some logger ->
+          (* Check that we haven't activated the logger twice *)
+          if Collections.StringSet.mem name !activated_loggers_set then begin
+            log#serror
+              ("The logger '" ^ name
+             ^ "' is used twice in the '-log' and/or '-log-debug' option(s)");
+            fail false
+          end
+          else begin
+            activated_loggers_set :=
+              Collections.StringSet.add name !activated_loggers_set;
+            logger#set_level level
+          end)
+    !activated_loggers;
+
+  (* Properly register the marked ids *)
+  List.iter
+    (fun id ->
+      let i = if String.length id >= 2 && String.get id 1 = '@' then 2 else 1 in
+      let sub = String.sub id i (String.length id - i) in
+      match int_of_string_opt sub with
+      | None ->
+          log#serror
+            ("Invalid identifier provided to option `-mark-ids`: '" ^ id
+           ^ "': '" ^ sub ^ "' can't be parsed as an int");
+          fail false
+      | Some i -> (
+          let open ContextsBase in
+          match String.get id 0 with
+          | 's' -> marked_symbolic_value_ids_insert_from_int i
+          | 'b' -> marked_borrow_ids_insert_from_int i
+          | 'a' -> marked_abstraction_ids_insert_from_int i
+          | 'r' -> marked_region_ids_insert_from_int i
+          | _ ->
+              log#serror
+                ("Invalid identifier provided to option: '" ^ id
+               ^ "': the first character should be in {'s', 'b', 'a', 'r'}");
+              fail false))
+    !marked_ids;
+
   (* Sanity check (now that the arguments are parsed!) *)
   check_arg_implies
     (not !extract_template_decreases_clauses)

src/dune

@@ -60,6 +60,7 @@
   PrePasses
   Print
   PrintPure
+  PrintSymbolicAst
   PureMicroPasses
   Pure
   PureTypeCheck

src/extract/Extract.ml

@@ -433,7 +433,7 @@ and extract_App (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
 and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (fid : fun_or_op_id)
     (generics : generic_args) (args : texpression list) : unit =
-  log#ldebug
+  log#ltrace
     (lazy
       ("extract_function_call: "
       ^ fun_or_op_id_to_string ctx fid
@@ -2864,7 +2864,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
 (** Extract a trait implementation *)
 let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (impl : trait_impl) : unit =
-  log#ldebug
+  log#ltrace
     (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.item_meta.name));
   (* Retrieve the impl name *)
   let impl_name = ctx_get_trait_impl impl.item_meta.span impl.def_id ctx in

src/extract/ExtractBuiltin.ml

@@ -588,7 +588,7 @@ let mk_builtin_funs_map () =
          (fun (name, filter, info) -> (name, (filter, info)))
          (builtin_funs ()))
   in
-  log#ldebug
+  log#ltrace
     (lazy ("builtin_funs_map:\n" ^ NameMatcherMap.to_string (fun _ -> "...") m));
   m
 
@@ -872,7 +872,7 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list =
 
 let mk_builtin_trait_impls_map () =
   let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in
-  log#ldebug
+  log#ltrace
     (lazy
       ("builtin_trait_impls_map:\n"
       ^ NameMatcherMap.to_string (fun _ -> "...") m));

src/interp/Cps.ml

@@ -17,21 +17,35 @@ type statement_eval_res =
   | Panic
   | LoopReturn of loop_id
       (** We reached a return statement *while inside a loop* *)
-  | EndEnterLoop of loop_id * typed_value SymbolicValueId.Map.t
+  | EndEnterLoop of
+      loop_id
+      * typed_value SymbolicValueId.Map.t
+      * symbolic_value_id SymbolicValueId.Map.t
       (** When we enter a loop, we delegate the end of the function is
           synthesized with a call to the loop translation. We use this
           evaluation result to transmit the fact that we end evaluation
           because we entered a loop.
 
           We provide the list of values for the translated loop function call
           (or to be more precise the input values instantiation).
+
+          We also provide the map from the input symbolic values to refresh symbolic
+          values (we need those to introduce intermediate let-bindings in the translation).
+          TODO: not clean; we will get rid of those once we generalize.
        *)
-  | EndContinue of loop_id * typed_value SymbolicValueId.Map.t
+  | EndContinue of
+      loop_id
+      * typed_value SymbolicValueId.Map.t
+      * symbolic_value_id SymbolicValueId.Map.t
       (** For loop translations: we end with a continue (i.e., a recursive call
           to the translation for the loop body).
 
           We provide the list of values for the translated loop function call
           (or to be more precise the input values instantiation).
+
+          We also provide the map from the input symbolic values to refresh symbolic
+          values (we need those to introduce intermediate let-bindings in the translation).
+          TODO: not clean; we will get rid of those once we generalize.
        *)
 [@@deriving show]