Merge pull request #385 from hacspec/jonas/proverif-letfun-macros

ProVerif backend: Translation of `fn`s to `letfun`s

engine/backends/proverif/proverif_backend.ml

@@ -79,7 +79,6 @@ struct
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
 end
 
-module AST = Ast.Make (InputLanguage)
 module BackendOptions = Backend.UnitBackendOptions
 open Ast
 
@@ -88,11 +87,17 @@ module ProVerifNamePolicy = struct
 
   [@@@ocamlformat "disable"]
 
-  let index_field_transform index = "_" ^ index
+  let index_field_transform index = Fn.id index
 
   let reserved_words = Hash_set.of_list (module String) [
   "among"; "axiom"; "channel"; "choice"; "clauses"; "const"; "def"; "diff"; "do"; "elimtrue"; "else"; "equation"; "equivalence"; "event"; "expand"; "fail"; "for"; "forall"; "foreach"; "free"; "fun"; "get"; "if"; "implementation"; "in"; "inj-event"; "insert"; "lemma"; "let"; "letfun"; "letproba"; "new"; "noninterf"; "noselect"; "not"; "nounif"; "or"; "otherwise"; "out"; "param"; "phase"; "pred"; "proba"; "process"; "proof"; "public vars"; "putbegin"; "query"; "reduc"; "restriction"; "secret"; "select"; "set"; "suchthat"; "sync"; "table"; "then"; "type"; "weaksecret"; "yield"
   ]
+
+  let field_name_transform ~struct_name field_name = struct_name ^ "_" ^ field_name
+
+  let enum_constructor_name_transform ~enum_name constructor_name = enum_name ^ "_" ^ constructor_name ^ "_c"
+
+  let struct_constructor_name_transform constructor_name =  constructor_name ^ "_c"
 end
 
 module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (ProVerifNamePolicy)
@@ -114,72 +119,91 @@ module Print = struct
       method ty_int _ = string "bitstring"
 
       method! item' item =
-        let fun_and_reduc name variants =
-          let constructor = List.hd variants in
-          match constructor with
-          | None -> empty
-          | Some constructor ->
-              let field_prefix =
-                if constructor.is_record then empty
-                else print#concrete_ident name
-              in
-              let fun_args = constructor.arguments in
-              let fun_args_full =
-                separate_map
-                  (comma ^^ break 1)
-                  (fun (x, y, _z) ->
-                    field_prefix ^^ print#concrete_ident x ^^ string ": "
-                    ^^ print#ty_at Param_typ y)
-                  fun_args
-              in
-              let fun_args_names =
-                separate_map
-                  (comma ^^ break 1)
-                  (fst3 >> fun x -> field_prefix ^^ print#concrete_ident x)
-                  fun_args
-              in
-              let fun_args_types =
-                separate_map
-                  (comma ^^ break 1)
-                  (snd3 >> print#ty_at Param_typ)
-                  fun_args
-              in
-              let fun_line =
-                string "fun" ^^ space ^^ print#concrete_ident name
-                ^^ iblock parens fun_args_types
-                ^^ string ": state."
-              in
-              let reduc_line =
-                string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi
-              in
-              let build_accessor (ident, ty, attr) =
-                string "accessor_" ^^ print#concrete_ident name ^^ underscore
-                ^^ print#concrete_ident ident
-                ^^ iblock parens
-                     (print#concrete_ident name ^^ iblock parens fun_args_names)
-                ^^ blank 1 ^^ equals ^^ blank 1 ^^ field_prefix
-                ^^ print#concrete_ident ident
-              in
-              let reduc_lines =
-                separate_map (dot ^^ hardline)
-                  (fun arg ->
-                    reduc_line ^^ nest 4 (hardline ^^ build_accessor arg))
-                  fun_args
-              in
-              fun_line ^^ hardline ^^ reduc_lines ^^ dot
+        let fun_and_reduc base_name constructor =
+          let field_prefix =
+            if constructor.is_record then empty
+            else print#concrete_ident base_name
+          in
+          let fun_args = constructor.arguments in
+          let fun_args_full =
+            separate_map
+              (comma ^^ break 1)
+              (fun (x, y, _z) ->
+                print#concrete_ident x ^^ string ": " ^^ print#ty_at Param_typ y)
+              fun_args
+          in
+          let fun_args_names =
+            separate_map
+              (comma ^^ break 1)
+              (fst3 >> fun x -> print#concrete_ident x)
+              fun_args
+          in
+          let fun_args_types =
+            separate_map
+              (comma ^^ break 1)
+              (snd3 >> print#ty_at Param_typ)
+              fun_args
+          in
+          let constructor_name = print#concrete_ident constructor.name in
+
+          let fun_line =
+            string "fun" ^^ space ^^ constructor_name
+            ^^ iblock parens fun_args_types
+            ^^ string ": "
+            ^^ print#concrete_ident base_name
+            ^^ dot
+          in
+          let reduc_line =
+            string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi
+          in
+          let build_accessor (ident, ty, attr) =
+            string "accessor" ^^ underscore ^^ print#concrete_ident ident
+            ^^ iblock parens (constructor_name ^^ iblock parens fun_args_names)
+            ^^ blank 1 ^^ equals ^^ blank 1 ^^ print#concrete_ident ident
+          in
+          let reduc_lines =
+            separate_map (dot ^^ hardline)
+              (fun arg -> reduc_line ^^ nest 4 (hardline ^^ build_accessor arg))
+              fun_args
+          in
+          fun_line ^^ hardline ^^ reduc_lines
+          ^^ if reduc_lines == empty then empty else dot
         in
         match item with
         (* `fn`s are transformed into `letfun` process macros. *)
         | Fn { name; generics; body; params } ->
             let params_string =
               iblock parens (separate_map (comma ^^ break 1) print#param params)
             in
-            string "letfun" ^^ space ^^ print#concrete_ident name
-            ^^ params_string ^/^ equals
-            ^^ nest 4 (hardline ^^ print#expr_at Item_Fn_body body ^^ dot)
+            string "letfun" ^^ space
+            ^^ align
+                 (print#concrete_ident name ^^ params_string ^^ space ^^ equals
+                ^^ hardline
+                 ^^ print#expr_at Item_Fn_body body
+                 ^^ dot)
         (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *)
         | Type { name; generics; variants; is_struct } ->
-            if is_struct then fun_and_reduc name variants else empty
+            let type_line =
+              string "type " ^^ print#concrete_ident name ^^ dot
+            in
+            let type_converter_line =
+              string "fun " ^^ print#concrete_ident name
+              ^^ string "_to_bitstring"
+              ^^ iblock parens (print#concrete_ident name)
+              ^^ string ": bitstring [typeConverter]."
+            in
+            if is_struct then
+              let struct_constructor = List.hd variants in
+              match struct_constructor with
+              | None -> empty
+              | Some constructor ->
+                  type_line ^^ hardline ^^ type_converter_line ^^ hardline
+                  ^^ fun_and_reduc name constructor
+            else
+              type_line ^^ hardline ^^ type_converter_line ^^ hardline
+              ^^ separate_map (hardline ^^ hardline)
+                   (fun variant -> fun_and_reduc name variant)
+                   variants
         | _ -> empty
 
       method! expr_let : lhs:pat -> rhs:expr -> expr fn =
@@ -224,7 +248,14 @@ module Print = struct
           let dummy_fn =
             match List.length args with
             | n when n < 8 -> string "dummy_fn_" ^^ PPrint.OCaml.int n
-            | _ -> string "not_supported"
+            | _ ->
+                Error.raise
+                  {
+                    kind =
+                      ExplicitRejection
+                        { reason = "Unsupported function arity." };
+                    span = current_span;
+                  }
           in
           let args =
             separate_map
@@ -237,15 +268,19 @@ module Print = struct
 
       method! literal : Generic_printer_base.literal_ctx -> literal fn =
         fun _ctx -> function
-          | String s -> string "no char literals in ProVerif"
-          | Char c -> string "no char literals in ProVerif"
           | Int { value; negative; _ } ->
               string "int2bitstring"
               ^^ iblock parens
                    (string value |> precede (if negative then minus else empty))
-          | Float { value; kind; negative } ->
-              string "no float literals in ProVerif"
           | Bool b -> OCaml.bool b
+          | _ ->
+              Error.raise
+                {
+                  kind =
+                    ExplicitRejection
+                      { reason = "Literal unsupported by ProVerif backend." };
+                  span = current_span;
+                }
     end
 
   include Api (struct
@@ -257,7 +292,21 @@ end
 let insert_top_level contents = contents ^ "\n\nprocess\n    0\n"
 
 (* Insert ProVerif code that will be necessary in any development.*)
-let insert_preamble contents = "channel c.\ntype state.\n" ^ contents
+let insert_preamble contents =
+  "channel c.\n\
+   type state.\n\
+   fun int2bitstring(nat): bitstring.\n\
+   fun dummy_fn_0(): bitstring.\n\
+   fun dummy_fn_1(bitstring): bitstring.\n\
+   fun dummy_fn_2(bitstring, bitstring): bitstring.\n\
+   fun dummy_fn_3(bitstring, bitstring, bitstring): bitstring.\n\
+   fun dummy_fn_4(bitstring, bitstring, bitstring, bitstring): bitstring.\n\
+   fun dummy_fn_5(bitstring, bitstring, bitstring, bitstring, bitstring): \
+   bitstring.\n\
+   fun dummy_fn_6(bitstring, bitstring, bitstring, bitstring, bitstring, \
+   bitstring): bitstring.\n\
+   fun dummy_fn_7(bitstring, bitstring, bitstring, bitstring, bitstring, \
+   bitstring, bitstring): bitstring.\n" ^ contents
 
 let is_process_read : attrs -> bool =
   Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessRead])

tests/Cargo.toml

@@ -24,6 +24,7 @@ members = [
         "nested-derefs",
         "proverif-minimal",
         "proverif-basic-structs",
-        "proverif-ping-pong"
+        "proverif-ping-pong",
+        "proverif-fn-to-letfun"
 ]
 resolver = "2"

tests/proverif-basic-structs/Cargo.toml

@@ -1,5 +1,5 @@
 [package]
-name = "proverif-basic-structs"
+name = "basic-structs"
 version = "0.1.0"
 edition = "2021"
 

tests/proverif-fn-to-letfun/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "fn-to-letfun"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/proverif-fn-to-letfun/src/lib.rs

@@ -0,0 +1,34 @@
+struct A {
+    x: usize,
+    y: u8,
+}
+struct B {
+    b: bool,
+}
+
+fn some_function() -> bool {
+    true
+}
+
+fn some_other_function(b: bool) -> u8 {
+    5
+}
+
+fn longer_function(x: &str) -> A {
+    let b = some_function();
+    let d = some_other_function(b);
+
+    A { x: 12usize, y: 9u8 }
+}
+
+fn another_longer_function() -> B {
+    let b = some_function();
+    let d = some_other_function(b);
+
+    B { b: false }
+}
+
+fn void_function() {
+    let b = some_function();
+    let d = some_other_function(b);
+}

tests/proverif-minimal/Cargo.toml

@@ -1,5 +1,5 @@
 [package]
-name = "proverif-minimal"
+name = "minimal"
 version = "0.1.0"
 edition = "2021"