From 1dd71ca1d37d5ca7fae5a7e9766e03194dfb764f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Feb 2022 19:22:30 +0100
Subject: Implement extraction of function calls

---
 src/Expressions.ml    |  20 ++++++
 src/ExtractToFStar.ml | 136 +++++++++++++++++++++++++++++++-----
 src/PureToExtract.ml  | 190 ++++++++++++++++++++++++++++++++------------------
 src/Types.ml          |   3 +
 4 files changed, 263 insertions(+), 86 deletions(-)

(limited to 'src')

diff --git a/src/Expressions.ml b/src/Expressions.ml
index 6e2b20d0..816870cd 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -47,6 +47,26 @@ type binop =
   | Shr
 [@@deriving show, ord]
 
+let all_binops =
+  [
+    BitXor;
+    BitAnd;
+    BitOr;
+    Eq;
+    Lt;
+    Le;
+    Ne;
+    Ge;
+    Gt;
+    Div;
+    Rem;
+    Add;
+    Sub;
+    Mul;
+    Shl;
+    Shr;
+  ]
+
 (** Constant value for an operand
 
     It is a bit annoying, but rustc treats some ADT and tuple instances as
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a4440071..100b5ecb 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -39,6 +39,21 @@ let fstar_keywords =
     "Type0";
   ]
 
+let fstar_int_name (int_ty : integer_type) =
+  match int_ty with
+  | Isize -> "isize"
+  | I8 -> "i8"
+  | I16 -> "i16"
+  | I32 -> "i32"
+  | I64 -> "i64"
+  | I128 -> "i128"
+  | Usize -> "usize"
+  | U8 -> "u8"
+  | U16 -> "u16"
+  | U32 -> "u32"
+  | U64 -> "u64"
+  | U128 -> "u128"
+
 let fstar_assumed_adts : (assumed_ty * string) list = [ (Result, "result") ]
 
 let fstar_assumed_structs : (assumed_ty * string) list = []
@@ -46,14 +61,76 @@ let fstar_assumed_structs : (assumed_ty * string) list = []
 let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list =
   [ (Result, result_return_id, "Return"); (Result, result_fail_id, "Fail") ]
 
+let fstar_assumed_functions :
+    (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
+  []
+
 let fstar_names_map_init =
   {
     keywords = fstar_keywords;
     assumed_adts = fstar_assumed_adts;
     assumed_structs = fstar_assumed_structs;
     assumed_variants = fstar_assumed_variants;
+    assumed_functions = fstar_assumed_functions;
   }
 
+let fstar_extract_unop (ctx : extraction_ctx) (fmt : F.formatter)
+    (extract_expr :
+      extraction_ctx -> F.formatter -> bool -> texpression -> extraction_ctx)
+    (inside : bool) (unop : unop) (arg : texpression) : extraction_ctx =
+  let unop =
+    match unop with
+    | Not -> "not"
+    | Neg int_ty -> fstar_int_name int_ty ^ "_neg"
+  in
+  if inside then F.pp_print_string fmt "(";
+  F.pp_print_string fmt unop;
+  F.pp_print_space fmt ();
+  let ctx = extract_expr ctx fmt true arg in
+  if inside then F.pp_print_string fmt ")";
+  ctx
+
+let fstar_extract_binop (ctx : extraction_ctx) (fmt : F.formatter)
+    (extract_expr :
+      extraction_ctx -> F.formatter -> bool -> texpression -> extraction_ctx)
+    (inside : bool) (binop : E.binop) (int_ty : integer_type)
+    (arg0 : texpression) (arg1 : texpression) : extraction_ctx =
+  if inside then F.pp_print_string fmt "(";
+  let ctx =
+    match binop with
+    | Eq ->
+        let ctx = extract_expr ctx fmt false arg0 in
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "=";
+        F.pp_print_space fmt ();
+        let ctx = extract_expr ctx fmt false arg1 in
+        ctx
+    | _ ->
+        let binop =
+          match binop with
+          | Eq -> failwith "Unreachable"
+          | Lt -> "lt"
+          | Le -> "le"
+          | Ne -> "ne"
+          | Ge -> "ge"
+          | Gt -> "gt"
+          | Div -> "div"
+          | Rem -> "rem"
+          | Add -> "add"
+          | Sub -> "sub"
+          | Mul -> "mul"
+          | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented
+        in
+        F.pp_print_string fmt (fstar_int_name int_ty ^ "_" ^ binop);
+        F.pp_print_space fmt ();
+        let ctx = extract_expr ctx fmt false arg0 in
+        F.pp_print_space fmt ();
+        let ctx = extract_expr ctx fmt false arg1 in
+        ctx
+  in
+  if inside then F.pp_print_string fmt ")";
+  ctx
+
 (**
  * [ctx]: we use the context to lookup type definitions, to retrieve type names.
  * This is used to compute variable names, when they have no basenames: in this
@@ -90,22 +167,10 @@ let fstar_names_map_init =
  * up type checking. Note that some languages actually forbids the name clashes
  * (it is the case of F* ).
  *)
-let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
-  let int_name (int_ty : integer_type) =
-    match int_ty with
-    | Isize -> "isize"
-    | I8 -> "i8"
-    | I16 -> "i16"
-    | I32 -> "i32"
-    | I64 -> "i64"
-    | I128 -> "i128"
-    | Usize -> "usize"
-    | U8 -> "u8"
-    | U16 -> "u16"
-    | U32 -> "u32"
-    | U64 -> "u64"
-    | U128 -> "u128"
-  in
+let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
+    formatter =
+  let int_name = fstar_int_name in
+
   (* For now, we treat only the case where type names are of the
    * form: `Module::Type`
    *)
@@ -158,6 +223,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
     (* Concatenate *)
     fname ^ suffix
   in
+
   let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
       : string =
     (* If there is a basename, we use it *)
@@ -194,6 +260,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
   let append_index (basename : string) (i : int) : string =
     basename ^ string_of_int i
   in
+
   let extract_constant_value (fmt : F.formatter) (_inside : bool)
       (cv : constant_value) : unit =
     match cv with
@@ -225,6 +292,8 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
     type_var_basename;
     append_index;
     extract_constant_value;
+    extract_unop = fstar_extract_unop;
+    extract_binop = fstar_extract_binop;
   }
 
 (** [inside] constrols whether we should add parentheses or not around type
@@ -628,7 +697,38 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (e : texpression) : extraction_ctx =
   match e.e with
   | Value (rv, _) -> extract_typed_rvalue ctx fmt inside rv
-  | Call call -> raise Unimplemented
+  | Call call -> (
+      match (call.func, call.args) with
+      | Unop unop, [ arg ] ->
+          ctx.fmt.extract_unop ctx fmt extract_texpression inside unop arg
+      | Binop (binop, int_ty), [ arg0; arg1 ] ->
+          ctx.fmt.extract_binop ctx fmt extract_texpression inside binop int_ty
+            arg0 arg1
+      | Regular (fun_id, rg_id), _ ->
+          if inside then F.pp_print_string fmt "(";
+          (* Open a box for the function call *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          (* Print the function name *)
+          let fun_name = ctx_get_function fun_id rg_id ctx in
+          F.pp_print_string fmt fun_name;
+          (* Print the type parameters *)
+          List.iter
+            (fun ty ->
+              F.pp_print_space fmt ();
+              extract_ty ctx fmt true ty)
+            call.type_params;
+          (* Print the input values *)
+          let ctx =
+            List.fold_left
+              (fun ctx ve -> extract_texpression ctx fmt true ve)
+              ctx call.args
+          in
+          (* Close the box for the function call *)
+          F.pp_close_box fmt ();
+          (* Return *)
+          if inside then F.pp_print_string fmt ")";
+          ctx
+      | _ -> failwith "Unreachable")
   | Let (monadic, lv, re, next_e) ->
       (* Open a box for the let-binding *)
       F.pp_open_hovbox fmt ctx.indent_incr;
@@ -729,8 +829,8 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hvbox fmt 0;
   (* Extract the body *)
   let _ = extract_texpression ctx fmt false def.body in
-  F.pp_close_box fmt ();
   (* Close the box for the body *)
+  F.pp_close_box fmt ();
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 8c8ab76a..54b59141 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -31,7 +31,7 @@ module StringMap = Collections.MakeMap (Collections.OrderedString)
 
 type name = Identifiers.name
 
-type formatter = {
+type 'ctx g_formatter = {
   bool_name : string;
   char_name : string;
   int_name : integer_type -> string;
@@ -105,6 +105,45 @@ type formatter = {
           - [inside]: if `true`, the value should be wrapped in parentheses
             if it is made of an application (ex.: `U32 3`)
        *)
+  extract_unop :
+    'ctx ->
+    F.formatter ->
+    ('ctx -> F.formatter -> bool -> texpression -> 'ctx) ->
+    bool ->
+    unop ->
+    texpression ->
+    'ctx;
+      (** Format a unary operation
+      
+          Inputs:
+          - extraction context (see below)
+          - formatter
+          - expression formatter
+          - [inside]
+          - unop
+          - argument
+       *)
+  extract_binop :
+    'ctx ->
+    F.formatter ->
+    ('ctx -> F.formatter -> bool -> texpression -> 'ctx) ->
+    bool ->
+    E.binop ->
+    integer_type ->
+    texpression ->
+    texpression ->
+    'ctx;
+      (** Format a binary operation
+      
+          Inputs:
+          - extraction context (see below)
+          - formatter
+          - expression formatter
+          - [inside]
+          - binop
+          - argument 0
+          - argument 1
+       *)
 }
 (** A formatter's role is twofold:
     1. Come up with name suggestions.
@@ -118,73 +157,6 @@ type formatter = {
     2. Format some specific terms, like constants.
  *)
 
-let compute_type_def_name (fmt : formatter) (def : type_def) : string =
-  fmt.type_name def.name
-
-(** A helper function: generates a function suffix from a region group
-    information.
-    TODO: move all those helpers.
-*)
-let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
-    : string =
-  (* There are several cases:
-     - [rg] is `Some`: this is a forward function:
-       - we add "_fwd"
-     - [rg] is `None`: this is a backward function:
-       - this function has one region group: we add "_back"
-       - this function has several backward function: we add "_back" and an
-         additional suffix to identify the precise backward function
-     Note that we always add a suffix (in case there are no region groups,
-     we could not add the "_fwd" suffix) to prevent name clashes between
-     definitions (in particular between type and function definitions).
-  *)
-  match rg with
-  | None -> "_fwd"
-  | Some rg ->
-      assert (num_region_groups > 0);
-      if num_region_groups = 1 then (* Exactly one backward function *)
-        "_back"
-      else if
-        (* Several region groups/backward functions:
-           - if all the regions in the group have names, we use those names
-           - otherwise we use an index
-        *)
-        List.for_all Option.is_some rg.region_names
-      then
-        (* Concatenate the region names *)
-        "_back" ^ String.concat "" (List.map Option.get rg.region_names)
-      else (* Use the region index *)
-        "_back" ^ RegionGroupId.to_string rg.id
-
-(** Extract information from a function, and give this information to a
-    [formatter] to generate a function's name.
-    
-    Note that we need region information coming from CFIM (when generating
-    the name for a backward function, we try to use the names of the regions
-    to 
- *)
-let compute_fun_def_name (ctx : trans_ctx) (fmt : formatter) (fun_id : A.fun_id)
-    (rg_id : RegionGroupId.id option) : string =
-  (* Lookup the function CFIM signature (we need the region information) *)
-  let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
-  let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in
-  (* Compute the regions information *)
-  let num_region_groups = List.length sg.regions_hierarchy in
-  let rg_info =
-    match rg_id with
-    | None -> None
-    | Some rg_id ->
-        let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in
-        let regions =
-          List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions
-        in
-        let region_names =
-          List.map (fun (r : T.region_var) -> r.name) regions
-        in
-        Some { id = rg.id; region_names }
-  in
-  fmt.fun_name fun_id basename num_region_groups rg_info
-
 (** We use identifiers to look for name clashes *)
 type id =
   | FunId of A.fun_id * RegionGroupId.id option
@@ -266,6 +238,11 @@ let names_map_add_assumed_variant (id : assumed_ty) (variant_id : VariantId.id)
     (name : string) (nm : names_map) : names_map =
   names_map_add (VariantId (Assumed id, variant_id)) name nm
 
+let names_map_add_assumed_function (fid : A.assumed_fun_id)
+    (rg_id : RegionGroupId.id option) (name : string) (nm : names_map) :
+    names_map =
+  names_map_add (FunId (A.Assumed fid, rg_id)) name nm
+
 (* TODO: remove those functions? We use the ones of extraction_ctx *)
 let names_map_get (id : id) (nm : names_map) : string =
   IdMap.find id nm.id_to_name
@@ -321,6 +298,8 @@ type extraction_ctx = {
     functions, etc.
  *)
 
+and formatter = extraction_ctx g_formatter
+
 let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
   (* TODO : nice debugging message if collision *)
   let names_map = names_map_add id name ctx.names_map in
@@ -472,6 +451,7 @@ type names_map_init = {
   assumed_adts : (assumed_ty * string) list;
   assumed_structs : (assumed_ty * string) list;
   assumed_variants : (assumed_ty * VariantId.id * string) list;
+  assumed_functions : (A.assumed_fun_id * RegionGroupId.id option * string) list;
 }
 
 (** Initialize a names map with a proper set of keywords/names coming from the
@@ -490,6 +470,7 @@ let initialize_names_map (init : names_map_init) : names_map =
    * - the assumed types
    * - the assumed struct constructors
    * - the assumed variants
+   * - the assumed functions
    *)
   let nm =
     List.fold_left
@@ -507,5 +488,78 @@ let initialize_names_map (init : names_map_init) : names_map =
         names_map_add_assumed_variant type_id variant_id name nm)
       nm init.assumed_variants
   in
+  let nm =
+    List.fold_left
+      (fun nm (fun_id, rg_id, name) ->
+        names_map_add_assumed_function fun_id rg_id name nm)
+      nm init.assumed_functions
+  in
   (* Return *)
   nm
+
+let compute_type_def_name (fmt : formatter) (def : type_def) : string =
+  fmt.type_name def.name
+
+(** A helper function: generates a function suffix from a region group
+    information.
+    TODO: move all those helpers.
+*)
+let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
+    : string =
+  (* There are several cases:
+     - [rg] is `Some`: this is a forward function:
+       - we add "_fwd"
+     - [rg] is `None`: this is a backward function:
+       - this function has one region group: we add "_back"
+       - this function has several backward function: we add "_back" and an
+         additional suffix to identify the precise backward function
+     Note that we always add a suffix (in case there are no region groups,
+     we could not add the "_fwd" suffix) to prevent name clashes between
+     definitions (in particular between type and function definitions).
+  *)
+  match rg with
+  | None -> "_fwd"
+  | Some rg ->
+      assert (num_region_groups > 0);
+      if num_region_groups = 1 then (* Exactly one backward function *)
+        "_back"
+      else if
+        (* Several region groups/backward functions:
+           - if all the regions in the group have names, we use those names
+           - otherwise we use an index
+        *)
+        List.for_all Option.is_some rg.region_names
+      then
+        (* Concatenate the region names *)
+        "_back" ^ String.concat "" (List.map Option.get rg.region_names)
+      else (* Use the region index *)
+        "_back" ^ RegionGroupId.to_string rg.id
+
+(** Extract information from a function, and give this information to a
+    [formatter] to generate a function's name.
+    
+    Note that we need region information coming from CFIM (when generating
+    the name for a backward function, we try to use the names of the regions
+    to 
+ *)
+let compute_fun_def_name (ctx : trans_ctx) (fmt : formatter) (fun_id : A.fun_id)
+    (rg_id : RegionGroupId.id option) : string =
+  (* Lookup the function CFIM signature (we need the region information) *)
+  let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
+  let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in
+  (* Compute the regions information *)
+  let num_region_groups = List.length sg.regions_hierarchy in
+  let rg_info =
+    match rg_id with
+    | None -> None
+    | Some rg_id ->
+        let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in
+        let regions =
+          List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions
+        in
+        let region_names =
+          List.map (fun (r : T.region_var) -> r.name) regions
+        in
+        Some { id = rg.id; region_names }
+  in
+  fmt.fun_name fun_id basename num_region_groups rg_info
diff --git a/src/Types.ml b/src/Types.ml
index 70ab3978..44302f8a 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -80,6 +80,9 @@ type integer_type =
   | U128
 [@@deriving show, ord]
 
+let all_integer_types =
+  [ Isize; I8; I16; I32; I64; I128; Usize; U8; U16; U32; U64; U128 ]
+
 type ref_kind = Mut | Shared [@@deriving show, ord]
 
 type assumed_ty = Box [@@deriving show, ord]
-- 
cgit v1.2.3