Merge branch 'main' into afromher_shifts

.github/workflows/ci.yml

@@ -0,0 +1,18 @@
+on:
+  push:
+    branches-ignore: [ '_**' ]
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  nix:
+    #runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, nix]
+    steps:
+      #- uses: cachix/install-nix-action@v22
+      - uses: actions/checkout@v4
+      - run: nix build -L .#charon
+      - run: nix build -L .#checks.x86_64-linux.tests
+      - run: nix build -L .#checks.x86_64-linux.tests-polonius
+      - run: nix build -L .#charon-ml
+      - run: nix build -L .#checks.x86_64-linux.charon-ml-tests

.gitignore

@@ -15,6 +15,7 @@ tests-polonius/ullbc
 tests-polonius/llbc
 tests-polonius/target
 charon-ml/_build
+charon-ml/name_matcher_parser/_build
 
 ##################
 # Generated by Nix

Makefile

@@ -34,22 +34,29 @@ 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-debug
+build-debug: build-charon-rust-debug build-charon-ml
 
 .PHONY: build-charon-rust
 build-charon-rust: generate-rust-toolchain
 	cd charon && $(MAKE)
+	mkdir -p bin
+	cp -f charon/target/release/charon bin
+	cp -f charon/target/release/charon-driver bin
 
-.PHONY: build-charon-ml
-build-charon-ml:
-	cd charon-ml && $(MAKE)
-
-.PHONY: build-bin-dir
-build-bin-dir:
+.PHONY: build-charon-rust-debug
+build-charon-rust-debug: generate-rust-toolchain
+	cd charon && cargo build
 	mkdir -p bin
 	cp -f charon/target/debug/charon bin
 	cp -f charon/target/debug/charon-driver bin
 
+.PHONY: build-charon-ml
+build-charon-ml:
+	cd charon-ml && $(MAKE)
+
 # Build the tests crate, and run the cargo tests
 .PHONY: build-tests
 build-tests:

README.md

@@ -20,7 +20,7 @@ present context, Charon allows us to go from the world of Rust programs to the w
 formal verification.
 
 We are **open to contributions**! Please contact us so that we can coordinate ourselves,
-if you are willing to contribute.
+if you are willing to contribute. For this purpose you can join the [Zulip](https://aeneas-verif.zulipchat.com/).
 
 ## LLBC
 Charon converts MIR code to ULLBC (Unstructured Low-Level Borrow Calculus) then
@@ -95,6 +95,7 @@ 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

charon-ml/Makefile

@@ -7,7 +7,7 @@ build:
 # For instance: `CHARON_LOG=1 make tests`.
 .PHONY: tests
 tests: build copy-tests
-	dune runtest -p charon
+	dune test
 
 # Reformat the code
 .PHONY: format

charon-ml/dune-project

@@ -1,4 +1,5 @@
 (lang dune 3.7)
+(using menhir 2.1)
 
 (name charon)
 
@@ -29,3 +30,8 @@
    Charon. Charon acts as an interface between the rustc compiler and program
    verification projects.  Its purpose is to process Rust .rs files and convert
    them into files easy to handle by program verifiers."))
+
+(package
+ (name name_matcher_parser)
+ (synopsis "Parser to define name matchers")
+ (description ""))

charon-ml/name_matcher_parser.opam

@@ -0,0 +1,28 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.1"
+synopsis: "Parser to define name matchers"
+description: ""
+authors: ["Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"]
+license: "Apache-2.0"
+homepage: "https://github.com/AeneasVerif/charon"
+bug-reports: "https://github.com/AeneasVerif/charon/issues"
+depends: [
+  "dune" {>= "3.7"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/AeneasVerif/charon.git"

charon-ml/name_matcher_parser/Ast.ml

@@ -0,0 +1,39 @@
+(* TODO: this duplicates PrimitiveValues *)
+type big_int = Z.t
+
+let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
+  Format.pp_print_string fmt (Z.to_string bi)
+
+let compare_big_int (bi0 : big_int) (bi1 : big_int) : int = Z.compare bi0 bi1
+let show_big_int (bi : big_int) : string = Z.to_string bi
+
+type var = VarName of string | VarIndex of int [@@deriving show, ord]
+
+type literal = LInt of big_int | LBool of bool | LChar of char
+[@@deriving show, ord]
+
+(*type const_generic = CgVar of const_generic_var option | CgValue of Z.t*)
+type ref_kind = RMut | RShared [@@deriving show, ord]
+type region = RVar of var option | RStatic [@@deriving show, ord]
+type primitive_adt = TTuple | TArray | TSlice [@@deriving show, ord]
+
+type pattern = pattern_elem list
+and pattern_elem = PIdent of string * generic_args | PImpl of expr
+
+(** An expression can be a type or a trait ref.
+
+    Note that we put in separate cases the tuple, array, slice and reference
+    types because they have special syntax.
+ *)
+and expr =
+  | EComp of pattern
+      (** Compound expression: instantiated adt, primitive type, constant, etc.
+          Note that if a type has generic arguments, they will be grouped with
+          the last pattern elem.
+       *)
+  | EPrimAdt of primitive_adt * generic_args
+  | ERef of region * expr * ref_kind
+  | EVar of var option
+
+and generic_arg = GExpr of expr | GValue of literal | GRegion of region
+and generic_args = generic_arg list [@@deriving show, ord]

charon-ml/name_matcher_parser/Interface.ml

@@ -0,0 +1,15 @@
+open Lexing
+include Ast
+
+let colnum pos = pos.pos_cnum - pos.pos_bol - 1
+
+let pos_string pos =
+  let l = string_of_int pos.pos_lnum and c = string_of_int (colnum pos + 1) in
+  "line " ^ l ^ ", column " ^ c
+
+let parse_pattern (s : string) : pattern =
+  let lexbuf = Lexing.from_string s in
+  try Parser.full_pattern Lexer.token lexbuf
+  with Parser.Error ->
+    raise
+      (Failure ("Parse error at " ^ pos_string lexbuf.lex_curr_p ^ ":\n" ^ s))

charon-ml/name_matcher_parser/Lexer.mll

@@ -0,0 +1,41 @@
+{
+  open Parser
+  open Ast
+}
+
+let digit = ['0'-'9']
+let alpha = ['a'-'z' 'A'-'Z']
+let ident = (alpha) (alpha | digit | '_')*
+let whitespace = [' ']+
+
+(* Rules *)
+rule token = parse
+  | "::" { SEP }
+  | "mut" { MUT }
+  | "'static" { STATIC_REGION }
+  | ''' { REGION (index lexbuf) }
+  | "true" { TRUE }
+  | "false" { FALSE }
+  | ident { IDENT (Lexing.lexeme lexbuf) }
+  | digit { INT (Z.of_string (Lexing.lexeme lexbuf)) }
+  | '(' { LEFT_BRACKET }
+  | ')' { RIGHT_BRACKET }
+  | '{' { LEFT_CURLY }
+  | '}' { RIGHT_CURLY }
+  | '[' { LEFT_SQUARE }
+  | ']' { RIGHT_SQUARE }
+  | "@" { VAR(index lexbuf) }
+  | ';' { SEMICOL }
+  | '&' { AMPERSAND }
+  | whitespace { token lexbuf }
+  | eof { EOF }
+  | '<' { LEFT_ANGLE }
+  | '>' { RIGHT_ANGLE }
+  | ',' { COMMA } 
+  | _ { raise (Failure ("Character not allowed in source text: '" ^ Lexing.lexeme lexbuf ^ "'")) }
+
+and index = parse
+  | ident { Some (VarName (Lexing.lexeme lexbuf)) }
+  | digit+ { Some (VarIndex (int_of_string (Lexing.lexeme lexbuf))) }
+  | '_' { None }
+  | "" { None }

charon-ml/name_matcher_parser/Parser.mly

@@ -0,0 +1,85 @@
+%{
+open Ast
+%}
+
+%token <string> IDENT
+%token <Ast.var option> VAR // For types and const generics
+%token <Ast.var option> REGION
+%token <Z.t> INT
+%token STATIC_REGION
+%token SEP TRUE FALSE
+%token LEFT_BRACKET RIGHT_BRACKET
+%token LEFT_CURLY RIGHT_CURLY
+%token LEFT_SQUARE RIGHT_SQUARE
+%token LEFT_ANGLE RIGHT_ANGLE
+%token SEMICOL AMPERSAND MUT COMMA EOF
+
+/* Types */
+
+%type <pattern> full_pattern
+%type <pattern> pattern
+%type <pattern_elem> pattern_elem
+%type <expr> expr
+%type <region> region
+%type <generic_args> generic_args
+%type <generic_arg> generic_arg
+
+/* Entry point */
+
+%start full_pattern
+
+%%
+
+full_pattern:
+  | n=pattern EOF { n }
+
+pattern:
+  | e=pattern_elem { [e] }
+  | e=pattern_elem SEP n=pattern { e :: n }
+
+pattern_elem:
+  // (Instantiated) identifier
+  | id=IDENT { PIdent (id, []) }
+  | id=IDENT; LEFT_ANGLE; g=generic_args; RIGHT_ANGLE { PIdent (id, g) }
+  // Impl path elem
+  | LEFT_CURLY; ty=expr; RIGHT_CURLY { PImpl ty }
+
+expr:
+  // Compound types - note that if a type has generics, they will be grouped
+  // with the last pattern_elem of the name
+  | n=pattern { EComp n }
+  // Primitive ADT: Tuple
+  | LEFT_BRACKET; tys=separated_list(COMMA, expr); RIGHT_BRACKET {
+      EPrimAdt (TTuple, List.map (fun x -> GExpr x) tys) }
+  // Primitive ADT: Slice
+  | LEFT_SQUARE; ty=expr; RIGHT_SQUARE {
+      EPrimAdt (TSlice, [GExpr ty]) }
+  // Primitive ADT: Array
+  | LEFT_SQUARE; ty=expr; SEMICOL; cg=expr; RIGHT_SQUARE {
+      EPrimAdt (TArray, [GExpr ty; GExpr cg]) }
+  // References
+  | AMPERSAND; r=region; MUT; ty=expr {
+      ERef (r, ty, RMut) }
+  | AMPERSAND; r=region; ty=expr {
+      ERef (r, ty, RShared) }
+  // Variables
+  | v=VAR { EVar v }
+  ;
+
+region:
+  | STATIC_REGION { RStatic }
+  | r=REGION { RVar r }
+
+generic_args:
+  | g=generic_arg { [ g ] }
+  | g=generic_arg; COMMA; gl=generic_args { g :: gl }
+
+generic_arg:
+  // Expressions
+  | e=expr { GExpr e }
+  // Values
+  | TRUE { GValue (LBool true) }
+  | FALSE { GValue (LBool false) }
+  | v=INT { GValue (LInt v) }
+  // Regions
+  | r=region { GRegion r }

charon-ml/name_matcher_parser/dune

@@ -0,0 +1,13 @@
+(ocamllex Lexer)
+(menhir
+ (modules Parser)
+ (flags --explain --inspection --table --dump))
+
+(library
+ (name name_matcher_parser)
+ (public_name name_matcher_parser)
+ (preprocess (pps ppx_deriving.show ppx_deriving.ord))
+ (libraries zarith menhirLib)
+ (flags
+  ; menhir generates instances of the "unused rec flag" warning
+  (:standard -w -39)))

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,16 @@ 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 ()
+
+  let filter_mapi (f : int -> 'a -> 'b option) (l : 'a list) : 'b list =
+    let l = mapi f l in
+    filter_map (fun x -> x) l
 end
 
 module type OrderedType = sig
@@ -137,6 +153,7 @@ module type Map = sig
 
   val add_list : (key * 'a) list -> 'a t -> 'a t
   val of_list : (key * 'a) list -> 'a t
+  val keys : 'a t -> key list
   val values : 'a t -> 'a list
 
   (** "Simple" pretty printing function.
@@ -180,6 +197,7 @@ module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct
 
   let add_list bl m = List.fold_left (fun s (key, e) -> add key e s) m bl
   let of_list bl = add_list bl empty
+  let keys m = List.map fst (bindings m)
   let values m = List.map snd (bindings m)
 
   let to_string indent_opt a_to_string m =
@@ -515,3 +533,8 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
     let find_opt k = find_opt k !m in
     (m, add, mem, find, find_opt)
 end
+
+module IntSet = MakeSet (OrderedInt)
+module IntMap = MakeMap (OrderedInt)
+module StringSet = MakeSet (OrderedString)
+module StringMap = MakeMap (OrderedString)