Merge remote-tracking branch 'refs/remotes/origin/main'

1 files changed, 325 insertions, 9 deletions

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 509c19ad..e214e820 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -8,7 +8,9 @@ module C = Contexts
 module Subst = Substitute
 module A = CfimAst
 module L = Logging
+open TypesUtils
 open InterpreterUtils
+open InterpreterBorrowsCore
 
 let debug_invariants : bool ref = ref false
 
@@ -27,6 +29,23 @@ type outer_borrow_info = {
   outer_shared : bool; (* true if the value is borrowed as shared *)
 }
 
+let set_outer_mut (info : outer_borrow_info) : outer_borrow_info =
+  { info with outer_borrow = true }
+
+let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info =
+  { outer_borrow = true; outer_shared = true }
+
+(* TODO: we need to factorize print functions for strings *)
+let ids_reprs_to_string (reprs : V.BorrowId.id V.BorrowId.Map.t) : string =
+  let bindings = V.BorrowId.Map.bindings reprs in
+  let bindings =
+    List.map
+      (fun (id, repr_id) ->
+        V.BorrowId.to_string id ^ " -> " ^ V.BorrowId.to_string repr_id)
+      bindings
+  in
+  String.concat "\n" bindings
+
 let borrows_infos_to_string (infos : borrow_info V.BorrowId.Map.t) : string =
   let bindings = V.BorrowId.Map.bindings infos in
   let bindings = List.map (fun (_, info) -> show_borrow_info info) bindings in
@@ -108,11 +127,11 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     object
       inherit [_] C.iter_eval_ctx as super
 
-      method! visit_Var _inside_abs binder v =
+      method! visit_Var _ binder v =
         let inside_abs = false in
         super#visit_Var inside_abs binder v
 
-      method! visit_Abs _inside_abs abs =
+      method! visit_Abs _ abs =
         let inside_abs = true in
         super#visit_Abs inside_abs abs
 
@@ -120,7 +139,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
         (* Register the loan *)
         let _ =
           match lc with
-          | V.SharedLoan (bids, _tv) -> register_shared_loan inside_abs bids
+          | V.SharedLoan (bids, _) -> register_shared_loan inside_abs bids
           | V.MutLoan bid -> register_mut_loan inside_abs bid
         in
         (* Continue exploring *)
@@ -152,10 +171,23 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
   (* Some utilities to register the borrows *)
   let find_info (bid : V.BorrowId.id) : borrow_info =
     (* Find the representant *)
-    let repr_bid = V.BorrowId.Map.find bid !ids_reprs in
-    (* Lookup the info *)
-    V.BorrowId.Map.find repr_bid !borrows_infos
+    match V.BorrowId.Map.find_opt bid !ids_reprs with
+    | Some repr_bid ->
+        (* Lookup the info *)
+        V.BorrowId.Map.find repr_bid !borrows_infos
+    | None ->
+        let err =
+          "find_info: could not find the representant of borrow "
+          ^ V.BorrowId.to_string bid ^ "\n" ^ "\n- Context:\n"
+          ^ eval_ctx_to_string ctx ^ "\n- representants:\n"
+          ^ ids_reprs_to_string !ids_reprs
+          ^ "\n- info:\n"
+          ^ borrows_infos_to_string !borrows_infos
+        in
+        L.log#serror err;
+        failwith err
   in
+
   let update_info (bid : V.BorrowId.id) (info : borrow_info) : unit =
     (* Find the representant *)
     let repr_bid = V.BorrowId.Map.find bid !ids_reprs in
@@ -233,7 +265,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
         ("\nAbout to check context invariant:\n" ^ eval_ctx_to_string ctx ^ "\n"));
     L.log#ldebug
       (lazy
-        ("Borrows information:\n"
+        ("\nBorrows information:\n"
         ^ borrows_infos_to_string !borrows_infos
         ^ "\n")));
 
@@ -254,9 +286,293 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     - borrows/loans can't contain ⊥ or inactivated mut borrows
     - shared loans can't contain mutable loans
  *)
-let check_borrowed_values_invariant (_ctx : C.eval_ctx) : unit = ()
+let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
+  let visitor =
+    object
+      inherit [_] C.iter_eval_ctx as super
+
+      method! visit_Bottom info =
+        (* No ⊥ inside borrowed values *)
+        assert (not info.outer_borrow)
+
+      method! visit_ABottom _info =
+        (* ⊥ inside an abstraction is not the same as in a regular value *)
+        ()
+
+      method! visit_loan_content info lc =
+        (* Update the info *)
+        let info =
+          match lc with
+          | V.SharedLoan (_, _) -> set_outer_shared info
+          | V.MutLoan _ ->
+              (* No mutable loan inside a shared loan *)
+              assert (not info.outer_shared);
+              set_outer_mut info
+        in
+        (* Continue exploring *)
+        super#visit_loan_content info lc
+
+      method! visit_borrow_content info bc =
+        (* Update the info *)
+        let info =
+          match bc with
+          | V.SharedBorrow _ -> set_outer_shared info
+          | V.InactivatedMutBorrow _ ->
+              assert (not info.outer_borrow);
+              set_outer_shared info
+          | V.MutBorrow (_, _) -> set_outer_mut info
+        in
+        (* Continue exploring *)
+        super#visit_borrow_content info bc
 
-let check_typing_invariant (_ctx : C.eval_ctx) : unit = ()
+      method! visit_aloan_content info lc =
+        (* Update the info *)
+        let info =
+          match lc with
+          | V.AMutLoan (_, _) -> set_outer_mut info
+          | V.ASharedLoan (_, _, _) -> set_outer_shared info
+          | V.AEndedMutLoan { given_back = _; child = _ } -> set_outer_mut info
+          | V.AEndedSharedLoan (_, _) -> set_outer_shared info
+          | V.AIgnoredMutLoan (_, _) -> set_outer_mut info
+          | V.AEndedIgnoredMutLoan { given_back = _; child = _ } ->
+              set_outer_mut info
+          | V.AIgnoredSharedLoan _ -> set_outer_shared info
+        in
+        (* Continue exploring *)
+        super#visit_aloan_content info lc
+
+      method! visit_aborrow_content info bc =
+        (* Update the info *)
+        let info =
+          match bc with
+          | V.AMutBorrow (_, _) -> set_outer_mut info
+          | V.ASharedBorrow _ -> set_outer_shared info
+          | V.AIgnoredMutBorrow _ -> set_outer_mut info
+          | V.AProjSharedBorrow _ -> set_outer_shared info
+        in
+        (* Continue exploring *)
+        super#visit_aborrow_content info bc
+    end
+  in
+
+  (* Explore *)
+  let info = { outer_borrow = false; outer_shared = false } in
+  visitor#visit_eval_ctx info ctx
+
+let check_constant_value_type (cv : V.constant_value) (ty : T.ety) : unit =
+  match (cv, ty) with
+  | V.Scalar sv, T.Integer int_ty -> assert (sv.int_ty = int_ty)
+  | V.Bool _, T.Bool | V.Char _, T.Char | V.String _, T.Str -> ()
+  | _ -> failwith "Erroneous typing"
+
+let check_typing_invariant (ctx : C.eval_ctx) : unit =
+  (* TODO: the type of aloans doens't make sense: they have a type
+   * of the shape `& (mut) T` where they should have type `T`...
+   * This messes a bit the type invariant checks when checking the
+   * children. In order to isolate the problem (for future modifications)
+   * we introduce function, so that we can easily spot all the involved
+   * places.
+   * *)
+  let aloan_get_expected_child_type (ty : 'r T.ty) : 'r T.ty =
+    let _, ty, _ = ty_get_ref ty in
+    ty
+  in
+
+  let visitor =
+    object
+      inherit [_] C.iter_eval_ctx as super
+
+      method! visit_typed_value info tv =
+        (* Check the current pair (value, type) *)
+        (match (tv.V.value, tv.V.ty) with
+        | V.Concrete cv, ty -> check_constant_value_type cv ty
+        (* ADT case *)
+        | V.Adt av, T.Adt (T.AdtId def_id, regions, tys) ->
+            (* Retrieve the definition to check the variant id, the number of
+             * parameters, etc. *)
+            let def = C.ctx_lookup_type_def ctx def_id in
+            (* Check the number of parameters *)
+            assert (List.length regions = List.length def.region_params);
+            assert (List.length tys = List.length def.type_params);
+            (* Check that the variant id is consistent *)
+            (match (av.V.variant_id, def.T.kind) with
+            | Some variant_id, T.Enum variants ->
+                assert (T.VariantId.to_int variant_id < List.length variants)
+            | None, T.Struct _ -> ()
+            | _ -> failwith "Erroneous typing");
+            (* Check that the field types are correct *)
+            let field_types =
+              Subst.type_def_get_instantiated_field_etypes def av.V.variant_id
+                tys
+            in
+            let fields_with_types =
+              List.combine av.V.field_values field_types
+            in
+            List.iter
+              (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
+              fields_with_types
+        (* Tuple case *)
+        | V.Adt av, T.Adt (T.Tuple, regions, tys) ->
+            assert (regions = []);
+            assert (av.V.variant_id = None);
+            (* Check that the fields have the proper values - and check that there
+             * are as many fields as field types at the same time *)
+            let fields_with_types = List.combine av.V.field_values tys in
+            List.iter
+              (fun ((v, ty) : V.typed_value * T.ety) -> assert (v.V.ty = ty))
+              fields_with_types
+        (* Assumed type case *)
+        | V.Adt av, T.Adt (T.Assumed aty_id, regions, tys) -> (
+            assert (av.V.variant_id = None);
+            match (aty_id, av.V.field_values, regions, tys) with
+            (* Box *)
+            | T.Box, [ boxed_value ], [], [ boxed_ty ] ->
+                assert (boxed_value.V.ty = boxed_ty)
+            | _ -> failwith "Erroneous type")
+        | V.Bottom, _ -> (* Nothing to check *) ()
+        | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
+            match (bc, rkind) with
+            | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut
+              -> (
+                (* Lookup the borrowed value to check it has the proper type *)
+                let _, glc = lookup_loan ek_all bid ctx in
+                match glc with
+                | Concrete (V.SharedLoan (_, sv))
+                | Abstract (V.ASharedLoan (_, sv, _)) ->
+                    assert (sv.V.ty = ref_ty)
+                | _ -> failwith "Inconsistent context")
+            | V.MutBorrow (_, bv), T.Mut ->
+                assert (
+                  (* Check that the borrowed value has the proper type *)
+                  bv.V.ty = ref_ty)
+            | _ -> failwith "Erroneous typing")
+        | V.Loan lc, ty -> (
+            match lc with
+            | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
+            | V.MutLoan bid -> (
+                (* Lookup the borrowed value to check it has the proper type *)
+                let glc = lookup_borrow ek_all bid ctx in
+                match glc with
+                | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
+                | Abstract (V.AMutBorrow (_, sv)) ->
+                    assert (Subst.erase_regions sv.V.ty = ty)
+                | _ -> failwith "Inconsistent context"))
+        | V.Symbolic sv, ty ->
+            let ty' = Subst.erase_regions sv.V.sv_ty in
+            assert (ty' = ty)
+        | _ -> failwith "Erroneous typing");
+        (* Continue exploring to inspect the subterms *)
+        super#visit_typed_value info tv
+
+      method! visit_typed_avalue info atv =
+        (* Check the current pair (value, type) *)
+        (match (atv.V.value, atv.V.ty) with
+        | V.AConcrete cv, ty ->
+            check_constant_value_type cv (Subst.erase_regions ty)
+        (* ADT case *)
+        | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) ->
+            (* Retrieve the definition to check the variant id, the number of
+             * parameters, etc. *)
+            let def = C.ctx_lookup_type_def ctx def_id in
+            (* Check the number of parameters *)
+            assert (List.length regions = List.length def.region_params);
+            assert (List.length tys = List.length def.type_params);
+            (* Check that the variant id is consistent *)
+            (match (av.V.variant_id, def.T.kind) with
+            | Some variant_id, T.Enum variants ->
+                assert (T.VariantId.to_int variant_id < List.length variants)
+            | None, T.Struct _ -> ()
+            | _ -> failwith "Erroneous typing");
+            (* Check that the field types are correct *)
+            let field_types =
+              Subst.type_def_get_instantiated_field_rtypes def av.V.variant_id
+                regions tys
+            in
+            let fields_with_types =
+              List.combine av.V.field_values field_types
+            in
+            List.iter
+              (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
+              fields_with_types
+        (* Tuple case *)
+        | V.AAdt av, T.Adt (T.Tuple, regions, tys) ->
+            assert (regions = []);
+            assert (av.V.variant_id = None);
+            (* Check that the fields have the proper values - and check that there
+             * are as many fields as field types at the same time *)
+            let fields_with_types = List.combine av.V.field_values tys in
+            List.iter
+              (fun ((v, ty) : V.typed_avalue * T.rty) -> assert (v.V.ty = ty))
+              fields_with_types
+        (* Assumed type case *)
+        | V.AAdt av, T.Adt (T.Assumed aty_id, regions, tys) -> (
+            assert (av.V.variant_id = None);
+            match (aty_id, av.V.field_values, regions, tys) with
+            (* Box *)
+            | T.Box, [ boxed_value ], [], [ boxed_ty ] ->
+                assert (boxed_value.V.ty = boxed_ty)
+            | _ -> failwith "Erroneous type")
+        | V.ABottom, _ -> (* Nothing to check *) ()
+        | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
+            match (bc, rkind) with
+            | V.AMutBorrow (_, av), T.Mut ->
+                (* Check that the child value has the proper type *)
+                assert (av.V.ty = ref_ty)
+            | V.ASharedBorrow bid, T.Shared -> (
+                (* Lookup the borrowed value to check it has the proper type *)
+                let _, glc = lookup_loan ek_all bid ctx in
+                match glc with
+                | Concrete (V.SharedLoan (_, sv))
+                | Abstract (V.ASharedLoan (_, sv, _)) ->
+                    assert (sv.V.ty = Subst.erase_regions ref_ty)
+                | _ -> failwith "Inconsistent context")
+            | V.AIgnoredMutBorrow av, T.Mut -> assert (av.V.ty = ref_ty)
+            | V.AProjSharedBorrow _, T.Shared -> ()
+            | _ -> failwith "Inconsistent context")
+        | V.ALoan lc, aty -> (
+            match lc with
+            | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av)
+              -> (
+                let borrowed_aty = aloan_get_expected_child_type aty in
+                assert (child_av.V.ty = borrowed_aty);
+                (* Lookup the borrowed value to check it has the proper type *)
+                let glc = lookup_borrow ek_all bid ctx in
+                match glc with
+                | Concrete (V.MutBorrow (_, bv)) ->
+                    assert (bv.V.ty = Subst.erase_regions borrowed_aty)
+                | Abstract (V.AMutBorrow (_, sv)) ->
+                    assert (
+                      Subst.erase_regions sv.V.ty
+                      = Subst.erase_regions borrowed_aty)
+                | _ -> failwith "Inconsistent context")
+            | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
+              ->
+                let borrowed_aty = aloan_get_expected_child_type aty in
+                assert (sv.V.ty = Subst.erase_regions borrowed_aty);
+                (* TODO: the type of aloans doesn't make sense, see above *)
+                assert (child_av.V.ty = borrowed_aty)
+            | V.AEndedMutLoan { given_back; child }
+            | V.AEndedIgnoredMutLoan { given_back; child } ->
+                let borrowed_aty = aloan_get_expected_child_type aty in
+                assert (given_back.V.ty = borrowed_aty);
+                assert (child.V.ty = borrowed_aty)
+            | V.AIgnoredSharedLoan child_av ->
+                assert (child_av.V.ty = aloan_get_expected_child_type aty))
+        | V.ASymbolic aproj, ty ->
+            let ty1 = Subst.erase_regions ty in
+            let ty2 =
+              match aproj with
+              | V.AProjLoans sv | V.AProjBorrows (sv, _) ->
+                  Subst.erase_regions sv.V.sv_ty
+            in
+            assert (ty1 = ty2)
+        | _ -> failwith "Erroneous typing");
+        (* Continue exploring to inspect the subterms *)
+        super#visit_typed_avalue info atv
+      (** TODO: there is a lot of duplication with [visit_typed_value]... *)
+    end
+  in
+  visitor#visit_eval_ctx () ctx
 
 let check_invariants (ctx : C.eval_ctx) : unit =
   check_loans_borrows_relation_invariant ctx;