Add various comments

4 files changed, 54 insertions, 15 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 36977aad..d2bf9181 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -58,6 +58,7 @@ type expression =
   | Switch of operand * switch_targets
   | Loop of expression
 [@@deriving show]
+(* TODO: merge with statement *)
 
 and switch_targets =
   | If of expression * expression  (** Gives the "if" and "else" blocks *)
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d737f79d..57a4e08b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -21,6 +21,8 @@ module L = Logging
    where invariants might be broken, etc.
  *)
 
+(* TODO: test with PLT-redex *)
+
 (** Some utilities *)
 
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
@@ -901,7 +903,10 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer)
 
 (** When we fail reading from or writing to a path, it might be because we
     need to update the environment by ending borrows, expanding symbolic
-    values, etc. The following type is used to convey this information. *)
+    values, etc. The following type is used to convey this information.
+    
+    TODO: compare with borrow_lres?
+*)
 type path_fail_kind =
   | FailSharedLoan of V.BorrowId.Set.t
       (** Failure because we couldn't go inside a shared loan *)
@@ -912,6 +917,7 @@ type path_fail_kind =
           (which should get activated) *)
   | FailSymbolic of (E.projection_elem * V.symbolic_proj_comp)
       (** Failure because we need to enter a symbolic value (and thus need to expand it) *)
+  (* TODO: Remove the parentheses *)
   | FailBottom of (int * E.projection_elem * T.ety)
       (** Failure because we need to enter an any value - we can expand Bottom
           values if they are left values. We return the number of elements which
@@ -1348,7 +1354,9 @@ exception UpdateCtx of C.eval_ctx
 
     This is used when reading, borrowing, writing to a value. We typically
     first call [update_ctx_along_read_place] or [update_ctx_along_write_place]
-    to get access to the value, then call this function to "prepare" the value.
+    to get access to the value, then call this function to "prepare" the value:
+    when moving values, we can't move a value which contains loans and thus need
+    to end them, etc.
  *)
 let rec end_loans_at_place (config : C.config) (access : access_kind)
     (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
@@ -1360,7 +1368,8 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
          In particular, we need to end the proper loans in the value.
          Also, we fail if the value contains any [Bottom].
 
-         We use exceptions to make it handy.
+         We use exceptions to make it handy: whenever we update the
+         context, we raise an exception wrapping the updated context.
       *)
       let rec inspect_update v : unit =
         match v.V.value with
@@ -1400,15 +1409,17 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
       in
       (* Inspect the value and update the context while doing so.
          If the context gets updated: perform a recursive call (many things
-         may have been updated in the context: first we need to retrieve the
-         proper updated value - and this value may actually not be accessible
-         anymore
+         may have been updated in the context: we need to re-read the value
+         at place [p] - and this value may actually not be accessible
+         anymore...)
       *)
       try
         inspect_update v;
         (* No context update required: return the current context *)
         ctx
-      with UpdateCtx ctx -> end_loans_at_place config access p ctx)
+      with UpdateCtx ctx ->
+        (* The context was updated: do a recursive call to reinspect the value *)
+        end_loans_at_place config access p ctx)
 
 (** Drop (end) all the loans and borrows at a given place, which should be
     seen as an l-value (we will write to it later, but need to drop the borrows
@@ -1878,12 +1889,12 @@ type statement_eval_res = Unit | Break of int | Continue of int | Return
 (** Small utility.
     
     Prepare a place which is to be used as the destination of an assignment:
-    update the environment along the paths, collect the borrows (to end the
-    loans) at the place, then drop the borrows.
+    update the environment along the paths, end the borrows and loans at
+    this place, etc.
 
-    Return the updated value at the end of the place. This value is likely
-    to contain [Bottom] values (as we drop borrows) but should not contain
-    any loan or borrow.
+    Return the updated context and the (updated) value at the end of the
+    place. This value should not contain any loan or borrow (and we check
+    it is the case). Note that it is very likely to contain [Bottom] values.
  *)
 let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) :
     C.eval_ctx * V.typed_value =
@@ -1901,7 +1912,12 @@ let prepare_lplace (config : C.config) (p : E.place) (ctx : C.eval_ctx) :
   (ctx, v)
 
 (** Read the value at a given place.
-    As long as it is a loan, end the loan *)
+    As long as it is a loan, end the loan.
+    This function doesn't perform a recursive exploration:
+    it won't dive into the value to end all the inner
+    loans (contrary to [drop_borrows_loans_at_lplace] for
+    instance).
+ *)
 let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
     (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx =
   let v = read_place_unwrap config access p ctx in
@@ -1914,6 +1930,17 @@ let rec end_loan_exactly_at_place (config : C.config) (access : access_kind)
       end_loan_exactly_at_place config access p ctx
   | _ -> ctx
 
+(** Updates the discriminant of a value at a given place.
+
+    There are two situations:
+    - either the discriminant is already the proper one (in which case we
+      don't do anything)
+    - or it is not the proper one (because the variant is not the proper
+      one, or the value is actually [Bottom] - this happens when
+      initializing ADT values), in which case we replace the value with
+      a variant with all its fields set to [Bottom].
+      For instance, something like: `Cons Bottom Bottom`.
+ *)
 let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place)
     (variant_id : T.VariantId.id) :
     (C.eval_ctx * statement_eval_res) eval_result =
@@ -2466,6 +2493,8 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) :
 
 (** Test a unit function (taking no arguments) by evaluating it in an empty
     environment
+
+    TODO: put in a sub-module
  *)
 let test_unit_function (type_defs : T.type_def list) (fun_defs : A.fun_def list)
     (fid : A.FunDefId.id) : unit eval_result =
diff --git a/src/Types.ml b/src/Types.ml
index 2b57e3f7..fce5c827 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -75,6 +75,7 @@ type 'r ty =
   | Ref of 'r * 'r ty * ref_kind
   | Assumed of assumed_ty * 'r list * 'r ty list
 [@@deriving show]
+(* TODO: group Bool, Char, etc. in Constant *)
 
 type rty = RegionVarId.id region ty [@@deriving show]
 (** Type with *R*egions.
diff --git a/src/Values.ml b/src/Values.ml
index 3e6bc838..57a0aeb0 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -82,9 +82,12 @@ type value =
   | Concrete of constant_value  (** Concrete (non-symbolic) value *)
   | Adt of adt_value  (** Enumerations and structures *)
   | Tuple of typed_value list
-      (** Tuple - note that units are encoded as 0-tuples *)
+      (** Tuple - note that units are encoded as 0-tuples
+          TODO: merge with Adt?
+       *)
   | Bottom  (** No value (uninitialized or moved value) *)
-  | Assumed of assumed_value  (** Assumed types (Box, Vec, Cell...) *)
+  | Assumed of assumed_value
+      (** Value of an abstract type (Box, Vec, Cell...) *)
   | Borrow of borrow_content  (** A borrowed value *)
   | Loan of loan_content  (** A loaned value *)
   | Symbolic of symbolic_proj_comp  (** Unknown value *)
@@ -92,9 +95,12 @@ type value =
 
 and adt_value = {
   def_id : TypeDefId.id;
+  (* TODO: remove *)
   variant_id : VariantId.id option;
   regions : erased_region list;
+  (* TODO: remove *)
   types : ety list;
+  (* TODO: remove *)
   field_values : typed_value list;
 }
 [@@deriving show]
@@ -147,6 +153,7 @@ type avalue =
   | AAssumed of aassumed_value
   | AProj of aproj
 [@@deriving show]
+(*  TODO: merge with value *)
 
 and aadt_value = {
   adef_id : TypeDefId.id;
@@ -156,6 +163,7 @@ and aadt_value = {
   afield_values : typed_avalue list;
 }
 [@@deriving show]
+(* TODO: merge with adt_value *)
 
 and aloan_content =
   | AMutLoan of BorrowId.id * typed_avalue