Merge pull request #587 from hacspec/inline-backend-macro

Inline backend macro

cli/driver/src/driver.rs

@@ -41,7 +41,7 @@ use callbacks_wrapper::*;
 use features::*;
 
 use const_format::formatcp;
-use hax_cli_options::{Command, ENV_VAR_OPTIONS_FRONTEND};
+use hax_cli_options::{BackendOptions, Command, ExporterCommand, ENV_VAR_OPTIONS_FRONTEND};
 
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::{interface, Queries};
@@ -165,6 +165,13 @@ fn main() {
                 "--cfg".into(),
                 hax_lib_macros_types::HAX_CFG_OPTION_NAME.into(),
             ])
+            .chain(match &options.command {
+                Some(Command::ExporterCommand(ExporterCommand::Backend(BackendOptions {
+                    backend,
+                    ..
+                }))) => vec!["--cfg".into(), format!("hax_backend_{backend}")],
+                _ => vec![],
+            })
             .chain(features.into_iter().map(|s| format!("-Zcrate-attr={}", s)))
             .chain(rustc_args[1..].iter().cloned())
             .collect();

engine/backends/coq/coq/coq_backend.ml

@@ -39,6 +39,7 @@ module SubtypeToInputLanguage
              and type for_loop = Features.Off.for_loop
              and type while_loop = Features.Off.while_loop
              and type for_index_loop = Features.Off.for_index_loop
+             and type quote = Features.Off.quote
              and type state_passing_loop = Features.Off.state_passing_loop) =
 struct
   module FB = InputLanguage

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -39,6 +39,7 @@ module SubtypeToInputLanguage
              and type monadic_action = Features.Off.monadic_action
              and type arbitrary_lhs = Features.Off.arbitrary_lhs
              and type nontrivial_lhs = Features.Off.nontrivial_lhs
+             and type quote = Features.Off.quote
              and type block = Features.Off.block) =
 struct
   module FB = InputLanguage

engine/backends/easycrypt/easycrypt_backend.ml

@@ -57,6 +57,7 @@ module RejectNotEC (FA : Features.T) = struct
         let block = reject
         let for_loop = reject
         let while_loop = reject
+        let quote = reject
         let construct_base _ _ = Features.On.construct_base
         let for_index_loop _ _ = Features.On.for_index_loop
 

engine/backends/fstar/fstar_backend.ml

@@ -11,6 +11,7 @@ include
       include On.Slice
       include On.Macro
       include On.Construct_base
+      include On.Quote
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -52,6 +53,7 @@ struct
         include Features.SUBTYPE.On.Construct_base
         include Features.SUBTYPE.On.Slice
         include Features.SUBTYPE.On.Macro
+        include Features.SUBTYPE.On.Quote
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -85,6 +87,9 @@ let doc_to_string : PPrint.document -> string =
 let term_to_string : F.AST.term -> string =
   FStar_Parser_ToDocument.term_to_document >> doc_to_string
 
+let pat_to_string : F.AST.pattern -> string =
+  FStar_Parser_ToDocument.pat_to_document >> doc_to_string
+
 let decl_to_string : F.AST.decl -> string =
   FStar_Parser_ToDocument.decl_to_document >> doc_to_string
 
@@ -568,6 +573,14 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
+    | Quote { contents; _ } ->
+        List.map
+          ~f:(function
+            | `Verbatim code -> code
+            | `Expr e -> pexpr e |> term_to_string
+            | `Pat p -> ppat p |> pat_to_string)
+          contents
+        |> String.concat |> F.term_of_string
     | _ -> .
 
   and parm { arm = { arm_pat; body } } = (ppat arm_pat, None, pexpr body)
@@ -1359,6 +1372,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Transform_hax_lib_inline
   |> Phases.Drop_sized_trait
   |> Phases.Simplify_question_marks
   |> Phases.And_mut_defsite

engine/backends/proverif/proverif_backend.ml

@@ -11,6 +11,7 @@ include
       include On.Question_mark
       include On.Early_exit
       include On.Slice
+      include On.Quote
       include On.Construct_base
     end)
     (struct
@@ -35,6 +36,7 @@ module SubtypeToInputLanguage
              and type slice = Features.On.slice
              and type question_mark = Features.On.question_mark
              and type macro = Features.On.macro
+             and type quote = Features.On.quote
              and type construct_base = Features.On.construct_base
     (* and type as_pattern = Features.Off.as_pattern *)
     (* and type nontrivial_lhs = Features.Off.nontrivial_lhs *)
@@ -883,6 +885,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.RawOrMutPointer(Features.Rust)
+    |> Phases.Transform_hax_lib_inline
     |> Phases.Simplify_question_marks
     |> Phases.And_mut_defsite
     |> Phases.Reconstruct_for_loops

engine/lib/ast.ml

@@ -258,6 +258,12 @@ functor
         }
       | Closure of { params : pat list; body : expr; captures : expr list }
       | EffectAction of { action : F.monadic_action; argument : expr }
+      | Quote of {
+          contents : [ `Verbatim of string | `Expr of expr | `Pat of pat ] list;
+          witness : F.quote;
+        }
+          (** A quotation is an inlined piece of backend code
+              interleaved with Rust code *)
 
     and expr = { e : expr'; span : span; typ : ty }
 

engine/lib/ast_utils.ml

@@ -54,6 +54,12 @@ module Make (F : Features.T) = struct
     let mut_borrow (e : expr) : expr option =
       match e.e with Borrow { kind = Mut _; e; _ } -> Some e | _ -> None
 
+    let borrow (e : expr) : expr option =
+      match e.e with Borrow { e; _ } -> Some e | _ -> None
+
+    let block (e : expr) : expr option =
+      match e.e with Block (e, _) -> Some e | _ -> None
+
     let deref (e : expr) : expr option =
       match e.e with
       | App { f = { e = GlobalVar (`Primitive Deref); _ }; args = [ e ]; _ } ->

engine/lib/ast_visitors.ml

@@ -434,6 +434,17 @@ functor
               in
               let argument = self#visit_expr env record_payload.argument in
               EffectAction { action; argument }
+          | Quote { contents; witness } ->
+              let contents =
+                self#visit_list
+                  (fun env -> function
+                    | `Verbatim code -> `Verbatim code
+                    | `Expr e -> `Expr (self#visit_expr env e)
+                    | `Pat p -> `Pat (self#visit_pat env p))
+                  env contents
+              in
+              let witness = self#visit_feature_quote env witness in
+              Quote { contents; witness }
 
         method visit_expr (env : 'env) (this : expr) : expr =
           let e = self#visit_expr' env this.e in
@@ -863,6 +874,8 @@ functor
         method visit_feature_nontrivial_lhs
             : 'env -> F.nontrivial_lhs -> F.nontrivial_lhs =
           fun _ x -> x
+
+        method visit_feature_quote : 'env -> F.quote -> F.quote = fun _ x -> x
       end
 
     class virtual ['self] mapreduce =
@@ -1448,6 +1461,22 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (EffectAction { action; argument }, reduce_acc)
+          | Quote { contents; witness } ->
+              let list, reduce_acc =
+                self#visit_list
+                  (fun env -> function
+                    | `Verbatim code -> (`Verbatim code, self#zero)
+                    | `Expr e ->
+                        let e, acc = self#visit_expr env e in
+                        (`Expr e, acc)
+                    | `Pat p ->
+                        let p, acc = self#visit_pat env p in
+                        (`Pat p, acc))
+                  env contents
+              in
+              let witness, reduce_acc' = self#visit_feature_quote env witness in
+              let reduce_acc = self#plus reduce_acc reduce_acc' in
+              (Quote { contents; witness }, reduce_acc)
 
         method visit_expr (env : 'env) (this : expr) : expr * 'acc =
           let e, reduce_acc = self#visit_expr' env this.e in
@@ -2061,6 +2090,9 @@ functor
         method visit_feature_nontrivial_lhs
             : 'env -> F.nontrivial_lhs -> F.nontrivial_lhs * 'acc =
           fun _ x -> (x, self#zero)
+
+        method visit_feature_quote : 'env -> F.quote -> F.quote * 'acc =
+          fun _ x -> (x, self#zero)
       end
 
     class virtual ['self] reduce =
@@ -2570,6 +2602,18 @@ functor
               let reduce_acc' = self#visit_expr env record_payload.argument in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
+          | Quote { contents; witness } ->
+              let reduce_acc =
+                self#visit_list
+                  (fun env -> function
+                    | `Verbatim code -> self#zero
+                    | `Expr e -> self#visit_expr env e
+                    | `Pat p -> self#visit_pat env p)
+                  env contents
+              in
+              let reduce_acc' = self#visit_feature_quote env witness in
+              let reduce_acc = self#plus reduce_acc reduce_acc' in
+              reduce_acc
 
         method visit_expr (env : 'env) (this : expr) : 'acc =
           let reduce_acc = self#visit_expr' env this.e in
@@ -3086,5 +3130,8 @@ functor
 
         method visit_feature_nontrivial_lhs : 'env -> F.nontrivial_lhs -> 'acc =
           fun _ _ -> self#zero
+
+        method visit_feature_quote : 'env -> F.quote -> 'acc =
+          fun _ _ -> self#zero
       end
   end

engine/lib/features.ml

@@ -22,6 +22,7 @@ loop,
   construct_base,
   monadic_action,
   monadic_binding,
+  quote,
   block]
 
 module Full = On
@@ -35,6 +36,7 @@ module Rust = struct
   include Off.Monadic_action
   include Off.Monadic_binding
   include Off.State_passing_loop
+  include Off.Quote
 end
 
 let _ = Enumeration.all

engine/lib/generic_printer/generic_printer.ml

@@ -225,6 +225,14 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
                 |> wrap_parens
             | MacroInvokation _ -> print#assertion_failure "MacroInvokation"
             | EffectAction _ -> print#assertion_failure "EffectAction"
+            | Quote { contents; _ } ->
+                List.map
+                  ~f:(function
+                    | `Verbatim code -> string code
+                    | `Expr e -> print#expr_at Expr_Quote e
+                    | `Pat p -> print#pat_at Expr_Quote p)
+                  contents
+                |> concat
             | App _ | Construct _ -> super#expr' ctx e
 
         method expr_monadic_let

engine/lib/generic_printer/generic_printer_base.ml

@@ -31,6 +31,7 @@ type ast_position =
   | Expr_Let_lhs
   | Expr_Let_rhs
   | Expr_Let_body
+  | Expr_Quote
   | Expr_Match_scrutinee
   | Expr_QuestionMark
   | Expr_Borrow

engine/lib/phases/phase_drop_references.ml

@@ -68,7 +68,8 @@ struct
 
     and dexpr' (span : span) (e : A.expr') : B.expr' =
       match (UA.unbox_underef_expr { e; span; typ = UA.never_typ }).e with
-      | [%inline_arms If + Literal + Array + Block + QuestionMark] -> auto
+      | [%inline_arms If + Literal + Array + Block + QuestionMark + Quote] ->
+          auto
       | Construct { constructor; is_record; is_struct; fields; base } ->
           Construct
             {