Merge pull request #48 from AeneasVerif/son_traits_types

Add support for traits

Makefile

@@ -34,10 +34,10 @@ generate-rust-toolchain-%:
 	cat rust-toolchain.template >> $*/rust-toolchain
 
 .PHONY: build
-build: build-charon-rust build-charon-ml build-bin-dir
+build: build-charon-rust build-charon-ml
 
 .PHONY: build-charon-rust
-build-charon-rust: generate-rust-toolchain
+build-charon-rust: generate-rust-toolchain build-bin-dir
 	cd charon && $(MAKE)
 
 .PHONY: build-charon-ml
@@ -47,8 +47,8 @@ build-charon-ml:
 .PHONY: build-bin-dir
 build-bin-dir:
 	mkdir -p bin
-	cp -f charon/target/debug/charon bin
-	cp -f charon/target/debug/charon-driver bin
+	cp -f charon/target/release/charon bin
+	cp -f charon/target/release/charon-driver bin
 
 # Build the tests crate, and run the cargo tests
 .PHONY: build-tests

README.md

@@ -95,7 +95,20 @@ Charon executable is located at `bin/charon`.
 Charon will build the crate and its dependencies, then extract the AST. Charon
 provides various options and flags to tweak its behaviour: you can display a
 detailed documentation with `--help`.
+In particular, you can print the LLBC generated by Charon with `--print-llbc`.
 
 **Remark**: because Charon is compiled with Rust nigthly (this is a requirement
 to implement a rustc driver), it will build your crate with Rust nightly. You
 can find the nightly version pinned for Charon in [`rust-toolchain.template`](rust-toolchain.template).
+
+## Debugging
+
+We are working on implementing proper error reporting. In the meanwhile, if Charon fails
+extracting information from a crate, you can set the `RUST_LOG` environment variable to
+generate an execution trace. For instance, if run the following command, Charon will print
+the name of all the definitions it explores, which can help pinpoint the problematic
+definition (which typically uses an unsupported feature).
+
+```
+RUST_LOG="charon_driver::translate_crate_to_ullbc=trace" charon
+```

charon-ml/src/Collections.ml

@@ -47,9 +47,15 @@ module List = struct
         let ls, last = pop_last ls in
         (x :: ls, last)
 
+  (** Return the last element *)
+  let last (ls : 'a list) : 'a = snd (pop_last ls)
+
   (** Return the n first elements of the list *)
   let prefix (n : int) (ls : 'a list) : 'a list = fst (split_at ls n)
 
+  (** Drop the n first elements of the list *)
+  let drop (n : int) (ls : 'a list) : 'a list = snd (split_at ls n)
+
   (** Iter and link the iterations.
 
       Iterate over a list, but call a function between every two elements
@@ -100,6 +106,12 @@ module List = struct
 
   let rec repeat (n : int) (x : 'a) : 'a list =
     if n > 0 then x :: repeat (n - 1) x else []
+
+  let rec iter_times (n : int) (f : unit -> unit) : unit =
+    if n > 0 then (
+      f ();
+      iter_times (n - 1) f)
+    else ()
 end
 
 module type OrderedType = sig
@@ -515,3 +527,6 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
     let find_opt k = find_opt k !m in
     (m, add, mem, find, find_opt)
 end
+
+module StringSet = MakeSet (OrderedString)
+module StringMap = MakeMap (OrderedString)

charon-ml/src/Expressions.ml

@@ -3,12 +3,28 @@ open Types
 open PrimitiveValues
 module VarId = IdGen ()
 module GlobalDeclId = Types.GlobalDeclId
+module FunDeclId = IdGen ()
+
+type fun_decl_id = FunDeclId.id [@@deriving show, ord]
 
 (** We define this type to control the name of the visitor functions
     (see e.g., {!Charon.UllbcAst.iter_statement_base}).
   *)
 type var_id = VarId.id [@@deriving show, ord]
 
+type assumed_fun_id =
+  | BoxNew
+  | BoxFree
+  | ArrayIndexShared
+  | ArrayIndexMut
+  | ArrayToSliceShared
+  | ArrayToSliceMut
+  | ArrayRepeat
+  | SliceLen
+  | SliceIndexShared
+  | SliceIndexMut
+[@@deriving show, ord]
+
 (** Ancestor the field_proj_kind iter visitor *)
 class ['self] iter_field_proj_kind_base =
   object (_self : 'self)
@@ -34,11 +50,10 @@ class ['self] map_field_proj_kind_base =
 
 type field_proj_kind =
   | ProjAdt of type_decl_id * variant_id option
-  | ProjOption of variant_id
-      (** Option is an assumed type, coming from the standard library *)
   | ProjTuple of int  (** The integer gives the arity of the tuple *)
 [@@deriving
   show,
+    ord,
     visitors
       {
         name = "iter_field_proj_kind";
@@ -60,6 +75,7 @@ type field_proj_kind =
 type projection_elem = Deref | DerefBox | Field of field_proj_kind * field_id
 [@@deriving
   show,
+    ord,
     visitors
       {
         name = "iter_projection_elem";
@@ -80,6 +96,7 @@ type projection_elem = Deref | DerefBox | Field of field_proj_kind * field_id
 type projection = projection_elem list
 [@@deriving
   show,
+    ord,
     visitors
       {
         name = "iter_projection";
@@ -112,6 +129,7 @@ class ['self] map_place_base =
 type place = { var_id : var_id; projection : projection }
 [@@deriving
   show,
+    ord,
     visitors
       {
         name = "iter_place";
@@ -131,11 +149,15 @@ type place = { var_id : var_id; projection : projection }
 
 type borrow_kind = Shared | Mut | TwoPhaseMut | Shallow [@@deriving show]
 
-(* Remark: no `ArrayToSlice` variant: it gets eliminated in a micro-pass *)
+(* TODO: FnPtr *)
+type cast_kind = CastInteger of integer_type * integer_type
+[@@deriving show, ord]
+
+(* Remark: no `ArrayToSlice` variant: it gets eliminated in a micro-pass. *)
 type unop =
   | Not
   | Neg
-  | Cast of integer_type * integer_type
+  | Cast of cast_kind
       (** Cast an integer from a source type to a target type *)
 [@@deriving show, ord]
 
@@ -185,25 +207,105 @@ let all_binops =
     Shr;
   ]
 
+(** Ancestor for the constant_expr iter visitor *)
+class ['self] iter_constant_expr_base =
+  object (self : 'self)
+    inherit [_] iter_place
+    inherit! [_] iter_ty
+    method! visit_'r : 'env -> erased_region -> unit = self#visit_erased_region
+    method visit_ety : 'env -> ety -> unit = self#visit_ty
+    method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
+
+    method visit_egeneric_args : 'env -> egeneric_args -> unit =
+      self#visit_generic_args
+
+    method visit_etrait_ref : 'env -> etrait_ref -> unit = self#visit_trait_ref
+    method visit_fun_decl_id : 'env -> fun_decl_id -> unit = fun _ _ -> ()
+    method visit_assumed_fun_id : 'env -> assumed_fun_id -> unit = fun _ _ -> ()
+  end
+
+(** Ancestor the constant_expr map visitor *)
+class ['self] map_constant_expr_base =
+  object (self : 'self)
+    inherit [_] map_place
+    inherit! [_] map_ty
+
+    method visit_'r : 'env -> erased_region -> erased_region =
+      self#visit_erased_region
+
+    method visit_ety : 'env -> ety -> ety = fun _ x -> x
+
+    method visit_erased_region : 'env -> erased_region -> erased_region =
+      fun _ x -> x
+
+    method visit_egeneric_args : 'env -> egeneric_args -> egeneric_args =
+      self#visit_generic_args
+
+    method visit_etrait_ref : 'env -> etrait_ref -> etrait_ref =
+      self#visit_trait_ref
+
+    method visit_fun_decl_id : 'env -> fun_decl_id -> fun_decl_id = fun _ x -> x
+
+    method visit_assumed_fun_id : 'env -> assumed_fun_id -> assumed_fun_id =
+      fun _ x -> x
+  end
+
+type raw_constant_expr =
+  | CLiteral of literal
+  | CVar of const_generic_var_id
+  | CTraitConst of etrait_ref * egeneric_args * string
+  | CFnPtr of fn_ptr
+
+and constant_expr = { value : raw_constant_expr; ty : ety }
+
+and fn_ptr = {
+  func : fun_id_or_trait_method_ref;
+  generics : egeneric_args;
+  trait_and_method_generic_args : egeneric_args option;
+}
+
+and fun_id_or_trait_method_ref =
+  | FunId of fun_id
+  | TraitMethod of etrait_ref * string * fun_decl_id
+      (** The fun decl id is not really needed and here for convenience purposes *)
+
+and fun_id = Regular of fun_decl_id | Assumed of assumed_fun_id
+[@@deriving
+  show,
+    ord,
+    visitors
+      {
+        name = "iter_constant_expr";
+        variety = "iter";
+        ancestors = [ "iter_constant_expr_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      },
+    visitors
+      {
+        name = "map_constant_expr";
+        variety = "map";
+        ancestors = [ "map_constant_expr_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      }]
+
 (** Ancestor the operand iter visitor *)
 class ['self] iter_operand_base =
   object (_self : 'self)
-    inherit [_] iter_place
-    inherit! [_] iter_const_generic
-    method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
+    inherit [_] iter_constant_expr
   end
 
 (** Ancestor the operand map visitor *)
 class ['self] map_operand_base =
   object (_self : 'self)
-    inherit [_] map_place
-    inherit! [_] map_const_generic
-    method visit_ety : 'env -> ety -> ety = fun _ x -> x
+    inherit [_] map_constant_expr
   end
 
-type operand = Copy of place | Move of place | Constant of ety * literal
+type operand = Copy of place | Move of place | Constant of constant_expr
 [@@deriving
   show,
+    ord,
     visitors
       {
         name = "iter_operand";
@@ -225,16 +327,12 @@ type operand = Copy of place | Move of place | Constant of ety * literal
 class ['self] iter_aggregate_kind_base =
   object (_self : 'self)
     inherit [_] iter_operand
-    method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
   end
 
 (** Ancestor the operand map visitor *)
 class ['self] map_aggregate_kind_base =
   object (_self : 'self)
     inherit [_] map_operand
-
-    method visit_erased_region : 'env -> erased_region -> erased_region =
-      fun _ x -> x
   end
 
 (** An aggregated ADT.
@@ -259,16 +357,7 @@ class ['self] map_aggregate_kind_base =
     the field 0, etc.).
  *)
 type aggregate_kind =
-  | AggregatedTuple
-  | AggregatedOption of variant_id * ety
-  (* TODO: AggregatedOption should be merged with AggregatedAdt *)
-  | AggregatedAdt of
-      type_decl_id
-      * variant_id option
-      * erased_region list
-      * ety list
-      * const_generic list
-  | AggregatedRange of ety (* TODO: merge with the Rust *)
+  | AggregatedAdt of type_id * variant_id option * egeneric_args
   | AggregatedArray of ety * const_generic
 [@@deriving
   show,
@@ -308,9 +397,10 @@ class ['self] map_rvalue_base =
   end
 
 (* TODO: move the aggregate kind to operands *)
+(* TODO: we should prefix the type variants with "T", this would avoid collisions *)
 type rvalue =
   | Use of operand
-  | Ref of place * borrow_kind
+  | RvRef of place * borrow_kind
   | UnaryOp of unop * operand
   | BinaryOp of binop * operand * operand
   | Discriminant of place