Add a CLI option to throw an exception when generating specific ids

src/Main.ml

@@ -90,8 +90,15 @@ let matches_name_with_generics (c : crate) (name : Types.name)
 
 let activated_loggers : string list ref = ref []
 
-let add_activated_logger (name : string) =
-  activated_loggers := name :: !activated_loggers
+let add_activated_loggers (name_list : string) =
+  let names = String.split_on_char ',' name_list in
+  activated_loggers := 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 *)
@@ -174,11 +181,21 @@ let () =
         " Print all the external definitions which are not listed in the \
          builtin functions" );
       ( "-log",
-        Arg.String add_activated_logger,
-        " Activate debugging log for a given logger designated by its name. \
-         The existing loggers are: {"
+        Arg.String add_activated_loggers,
+        " Activate debugging 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)
         ^ "}" );
+      ( "-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
 
@@ -254,6 +271,31 @@ let () =
       | Some logger -> logger#set_level EL.Debug)
     !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/llbc/ContextsBase.ml

@@ -71,15 +71,29 @@ type dummy_var_id = DummyVarId.id [@@deriving show, ord]
   it proved more convenient (and even before updating the code of the
   interpreter to use CPS).
  *)
-
-let symbolic_value_id_counter, fresh_symbolic_value_id =
-  SymbolicValueId.fresh_stateful_generator ()
-
-let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator ()
-let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()
-
-let abstraction_id_counter, fresh_abstraction_id =
-  AbstractionId.fresh_stateful_generator ()
+let ( symbolic_value_id_counter,
+      marked_symbolic_value_ids,
+      marked_symbolic_value_ids_insert_from_int,
+      fresh_symbolic_value_id ) =
+  SymbolicValueId.fresh_marked_stateful_generator ()
+
+let ( borrow_id_counter,
+      marked_borrow_ids,
+      marked_borrow_ids_insert_from_int,
+      fresh_borrow_id ) =
+  BorrowId.fresh_marked_stateful_generator ()
+
+let ( region_id_counter,
+      marked_region_ids,
+      marked_region_ids_insert_from_int,
+      fresh_region_id ) =
+  RegionId.fresh_marked_stateful_generator ()
+
+let ( abstraction_id_counter,
+      marked_abstraction_ids,
+      marked_abstraction_ids_insert_from_int,
+      fresh_abstraction_id ) =
+  AbstractionId.fresh_marked_stateful_generator ()
 
 let loop_id_counter, fresh_loop_id = LoopId.fresh_stateful_generator ()
 

src/symbolic/SymbolicToPure.ml

@@ -2196,8 +2196,20 @@ and aproj_to_consumed_aux (ctx : bs_ctx) (_abs_regions : T.RegionId.Set.t)
   | V.AEndedProjLoans (msv, []) ->
       (* The symbolic value was left unchanged *)
       Some (symbolic_value_to_texpression ctx msv)
-  | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) ->
+  | V.AEndedProjLoans (msv, [ (mnv, child_aproj) ]) ->
       sanity_check __FILE__ __LINE__ (child_aproj = AEmpty) ctx.span;
+      (* TODO: check that the updated symbolic values covers all the cases
+         (part of the symbolic value might have been updated, and the rest
+         left unchanged) - it might happen with nested borrows (see the documentation
+         of [AProjLoans]). For now we check that there are no nested borrows
+         to make sure we have to update this part of the code once we add support
+         for nested borrows.
+      *)
+      sanity_check __FILE__ __LINE__
+        (not
+           (TypesUtils.ty_has_nested_borrows (Some ctx.span)
+              ctx.type_ctx.type_infos msv.sv_ty))
+        ctx.span;
       (* The symbolic value was updated *)
       Some (symbolic_value_to_texpression ctx mnv)
   | V.AEndedProjLoans (_, _) ->