Merge pull request #44 from AeneasVerif/son_traits_types

Add support for traits

1 files changed, 119 insertions, 76 deletions

diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 8b2070c6..245f3b77 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -7,6 +7,7 @@ module E = Expressions
 open Utils
 module C = Contexts
 module Subst = Substitute
+module Assoc = AssociatedTypes
 module L = Logging
 open TypesUtils
 open ValuesUtils
@@ -141,11 +142,19 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
   | V.Adt av ->
       (* Sanity check *)
       (match v.V.ty with
-      | T.Adt (T.Assumed (T.Box | Vec), _, _, _) ->
+      | T.Adt (T.Assumed T.Box, _) ->
           raise (Failure "Can't copy an assumed value other than Option")
-      | T.Adt (T.AdtId _, _, _, _) -> assert allow_adt_copy
-      | T.Adt ((T.Assumed Option | T.Tuple), _, _, _) -> () (* Ok *)
-      | T.Adt (T.Assumed (Slice | T.Array), [], [ ty ], []) ->
+      | T.Adt (T.AdtId _, _) as ty ->
+          assert (allow_adt_copy || ty_is_primitively_copyable ty)
+      | T.Adt (T.Tuple, _) -> () (* Ok *)
+      | T.Adt
+          ( T.Assumed (Slice | T.Array),
+            {
+              regions = [];
+              types = [ ty ];
+              const_generics = [];
+              trait_refs = [];
+            } ) ->
           assert (ty_is_primitively_copyable ty)
       | _ -> raise (Failure "Unreachable"));
       let ctx, fields =
@@ -230,17 +239,16 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
   let prepare : cm_fun =
    fun cf ctx ->
     match op with
-    | Expressions.Constant (ty, cv) ->
+    | E.Constant _ ->
         (* No need to reorganize the context *)
-        literal_to_typed_value (TypesUtils.ty_as_literal ty) cv |> ignore;
         cf ctx
-    | Expressions.Copy p ->
+    | E.Copy p ->
         (* Access the value *)
         let access = Read in
         (* Expand the symbolic values, if necessary *)
         let expand_prim_copy = true in
         access_rplace_reorganize config expand_prim_copy access p cf ctx
-    | Expressions.Move p ->
+    | E.Move p ->
         (* Access the value *)
         let access = Move in
         let expand_prim_copy = false in
@@ -260,9 +268,71 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
      ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
-  | Expressions.Constant (ty, cv) ->
-      cf (literal_to_typed_value (TypesUtils.ty_as_literal ty) cv) ctx
-  | Expressions.Copy p ->
+  | E.Constant cv -> (
+      match cv.value with
+      | E.CLiteral lit ->
+          cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx
+      | E.CTraitConst (trait_ref, generics, const_name) -> (
+          assert (generics = TypesUtils.mk_empty_generic_args);
+          match trait_ref.trait_id with
+          | T.TraitImpl _ ->
+              (* This shouldn't happen: if we refer to a concrete implementation, we
+                 should directly refer to the top-level constant *)
+              raise (Failure "Unreachable")
+          | _ -> (
+              (* We refer to a constant defined in a local clause: simply
+                 introduce a fresh symbolic value *)
+              let ctx0 = ctx in
+              (* Lookup the trait declaration to retrieve the type of the symbolic value *)
+              let trait_decl =
+                C.ctx_lookup_trait_decl ctx
+                  trait_ref.trait_decl_ref.trait_decl_id
+              in
+              let _, (ty, _) =
+                List.find (fun (name, _) -> name = const_name) trait_decl.consts
+              in
+              (* Introduce a fresh symbolic value *)
+              let v = mk_fresh_symbolic_typed_value_from_ety V.TraitConst ty in
+              (* Continue the evaluation *)
+              let e = cf v ctx in
+              (* We have to wrap the generated expression *)
+              match e with
+              | None -> None
+              | Some e ->
+                  Some
+                    (SymbolicAst.IntroSymbolic
+                       ( ctx0,
+                         None,
+                         value_as_symbolic v.value,
+                         SymbolicAst.TraitConstValue
+                           (trait_ref, generics, const_name),
+                         e ))))
+      | E.CVar vid -> (
+          let ctx0 = ctx in
+          (* Lookup the const generic value *)
+          let cv = C.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
+          (* Continue *)
+          let e = cf v ctx in
+          (* We have to wrap the generated expression *)
+          match e with
+          | None -> None
+          | Some e ->
+              (* 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 (is_symbolic cv.V.value);
+              (* *)
+              Some
+                (SymbolicAst.IntroSymbolic
+                   ( ctx0,
+                     None,
+                     value_as_symbolic v.value,
+                     SymbolicAst.ConstGenericValue vid,
+                     e )))
+      | E.CFnPtr _ -> raise (Failure "TODO"))
+  | E.Copy p ->
       (* Access the value *)
       let access = Read in
       let cc = read_place access p in
@@ -283,7 +353,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
       in
       (* Compose and apply *)
       comp cc copy cf ctx
-  | Expressions.Move p ->
+  | E.Move p ->
       (* Access the value *)
       let access = Move in
       let cc = read_place access p in
@@ -358,7 +428,7 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand)
         match mk_scalar sv.int_ty i with
         | Error _ -> cf (Error EPanic)
         | Ok sv -> cf (Ok { v with V.value = V.Literal (PV.Scalar sv) }))
-    | E.Cast (src_ty, tgt_ty), V.Literal (PV.Scalar sv) -> (
+    | E.Cast (E.CastInteger (src_ty, tgt_ty)), V.Literal (PV.Scalar sv) -> (
         assert (src_ty = sv.int_ty);
         let i = sv.PV.value in
         match mk_scalar tgt_ty i with
@@ -384,7 +454,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
       match (unop, v.V.ty) with
       | E.Not, (T.Literal Bool as lty) -> lty
       | E.Neg, (T.Literal (Integer _) as lty) -> lty
-      | E.Cast (_, tgt_ty), _ -> T.Literal (Integer tgt_ty)
+      | E.Cast (E.CastInteger (_, tgt_ty)), _ -> T.Literal (Integer tgt_ty)
       | _ -> raise (Failure "Invalid input for unop")
     in
     let res_sv =
@@ -653,73 +723,46 @@ let eval_rvalue_aggregate (config : C.config)
    fun ctx ->
     (* Match on the aggregate kind *)
     match aggregate_kind with
-    | E.AggregatedTuple ->
-        let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
-        let v = V.Adt { variant_id = None; field_values = values } in
-        let ty = T.Adt (T.Tuple, [], tys, []) in
-        let aggregated : V.typed_value = { V.value = v; ty } in
-        (* Call the continuation *)
-        cf aggregated ctx
-    | E.AggregatedOption (variant_id, ty) ->
-        (* Sanity check *)
-        if variant_id = T.option_none_id then assert (values = [])
-        else if variant_id = T.option_some_id then
-          assert (List.length values = 1)
-        else raise (Failure "Unreachable");
-        (* Construt the value *)
-        let aty = T.Adt (T.Assumed T.Option, [], [ ty ], []) in
-        let av : V.adt_value =
-          { V.variant_id = Some variant_id; V.field_values = values }
-        in
-        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
-        (* Call the continuation *)
-        cf aggregated ctx
-    | E.AggregatedAdt (def_id, opt_variant_id, regions, types, cgs) ->
-        (* Sanity checks *)
-        let type_decl = C.ctx_lookup_type_decl ctx def_id in
-        assert (List.length type_decl.region_params = List.length regions);
-        let expected_field_types =
-          Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
-            types cgs
-        in
-        assert (
-          expected_field_types
-          = List.map (fun (v : V.typed_value) -> v.V.ty) values);
-        (* Construct the value *)
-        let av : V.adt_value =
-          { V.variant_id = opt_variant_id; V.field_values = values }
-        in
-        let aty = T.Adt (T.AdtId def_id, regions, types, cgs) in
-        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
-        (* Call the continuation *)
-        cf aggregated ctx
-    | E.AggregatedRange ety ->
-        (* There should be two fields exactly *)
-        let v0, v1 =
-          match values with
-          | [ v0; v1 ] -> (v0, v1)
-          | _ -> raise (Failure "Unreachable")
-        in
-        (* Ranges are parametric over the type of indices. For now we only
-           support scalars, which can be of any type *)
-        assert (literal_type_is_integer (ty_as_literal ety));
-        assert (v0.ty = ety);
-        assert (v1.ty = ety);
-        (* Construct the value *)
-        let av : V.adt_value =
-          { V.variant_id = None; V.field_values = values }
-        in
-        let aty = T.Adt (T.Assumed T.Range, [], [ ety ], []) in
-        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
-        (* Call the continuation *)
-        cf aggregated ctx
+    | E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
+        match type_id with
+        | Tuple ->
+            let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
+            let v = V.Adt { variant_id = None; field_values = values } in
+            let generics = TypesUtils.mk_generic_args [] tys [] [] in
+            let ty = T.Adt (T.Tuple, generics) in
+            let aggregated : V.typed_value = { V.value = v; ty } in
+            (* Call the continuation *)
+            cf aggregated ctx
+        | AdtId def_id ->
+            (* Sanity checks *)
+            let type_decl = C.ctx_lookup_type_decl ctx def_id in
+            assert (
+              List.length type_decl.generics.regions
+              = List.length generics.regions);
+            let expected_field_types =
+              Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
+                generics
+            in
+            assert (
+              expected_field_types
+              = List.map (fun (v : V.typed_value) -> v.V.ty) values);
+            (* Construct the value *)
+            let av : V.adt_value =
+              { V.variant_id = opt_variant_id; V.field_values = values }
+            in
+            let aty = T.Adt (T.AdtId def_id, generics) in
+            let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+            (* Call the continuation *)
+            cf aggregated ctx
+        | Assumed _ -> raise (Failure "Unreachable"))
     | E.AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
         assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
         assert (len = Z.of_int (List.length values));
-        let ty = T.Adt (T.Assumed T.Array, [], [ ety ], [ cg ]) in
+        let generics = TypesUtils.mk_generic_args [] [ ety ] [ cg ] [] in
+        let ty = T.Adt (T.Assumed T.Array, generics) in
         (* In order to generate a better AST, we introduce a symbolic
            value equal to the array. The reason is that otherwise, the
            array we introduce here might be duplicated in the generated
@@ -752,7 +795,7 @@ let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
   (* Delegate to the proper auxiliary function *)
   match rvalue with
   | E.Use op -> comp_wrap (eval_operand config op) ctx
-  | E.Ref (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
+  | E.RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
   | E.UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
   | E.BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
   | E.Aggregate (aggregate_kind, ops) ->