Skip to content

Commit

Permalink
[textual] Adding closures -- parsing part
Browse files Browse the repository at this point in the history
Summary:
we provide Textual with a closure mechanism, in order to help frontend writers.

The syntax for a closure construction is

```
         n0 = fun (p1, p2, p3) -> C.foo(exp1, exp2, p1, p2, p3)
```

which has an "intuitive" semantics but is in fact quite constrained:
* `C.foo` must be implemented (not only declare) in the same file
* `p1, p2, p3` appear always twice. They are the closure parameters
* `exp1, exp2` are the value of the captured expressions

It is the responsability of the  frontend to generate a "lambda-lifted" closure like that. We don't know which capture strategy it will use.

*Example1*:
  let x = 3 in
  let f y = x + y in
should generate something like
  n0 = fun (y) -> add(3, y)
with
```
  declare add(x: int, y: int) : int {
  #entry:
    ret __sil_plus(x, y)
  }
```
*Example2*:
  let x = ref 3 in
  let f y = !x + 3 in
should generate something like
  n0 = fun (y) -> add(&x, y)
with
```
  declare add(x: *int, y: int) : int {
  #entry:
    n0 = load x
    ret __sil_plus(n0, y)
  }
```

**Parser horrors**
At parsing time, an expression like `n0(0)`or `x(0)` is hard to parse. It could be a regular call on a function names `n0` (or `x`), or a closure application. We give priority to the second case, using variable declarations. This is implemented after parsing with a new transformation pass.

Reviewed By: vsiles

Differential Revision: D49370340

fbshipit-source-id: 381ba0e77c01dc9a84b10a2e8e3e260312e289d8
  • Loading branch information
davidpichardie authored and facebook-github-bot committed Oct 4, 2023
1 parent a0207a9 commit db6e322
Show file tree
Hide file tree
Showing 17 changed files with 389 additions and 20 deletions.
26 changes: 23 additions & 3 deletions infer/src/textual/Textual.ml
Original file line number Diff line number Diff line change
Expand Up @@ -575,17 +575,19 @@ module Exp = struct
(* | Sizeof of sizeof_data *)
| Const of Const.t
| Call of {proc: QualifiedProcName.t; args: t list; kind: call_kind}
| Closure of {proc: QualifiedProcName.t; captured: t list; params: VarName.t list}
| Apply of {closure: t; args: t list}
| Typ of Typ.t

let call_non_virtual proc args = Call {proc; args; kind= NonVirtual}

let call_virtual proc recv args = Call {proc; args= recv :: args; kind= Virtual}

let call_sig qualified_name args = function
let call_sig qualified_name nb_args = function
| Some Lang.Hack ->
ProcSig.Hack {qualified_name; arity= Some (List.length args)}
ProcSig.Hack {qualified_name; arity= Some nb_args}
| Some Lang.Python ->
ProcSig.Python {qualified_name; arity= Some (List.length args)}
ProcSig.Python {qualified_name; arity= Some nb_args}
| Some Lang.Java | None ->
ProcSig.Other {qualified_name}

Expand All @@ -595,8 +597,12 @@ module Exp = struct
let cast typ exp = call_non_virtual ProcDecl.cast_name [Typ typ; exp]

let rec pp fmt = function
| Apply {closure; args} ->
F.fprintf fmt "%a%a" pp closure pp_list args
| Var id ->
Ident.pp fmt id
| Load {exp= Lvar x; typ= None} ->
F.fprintf fmt "%a" VarName.pp x
| Load {exp; typ= None} ->
F.fprintf fmt "[%a]" pp exp
| Load {exp; typ= Some typ} ->
Expand All @@ -619,6 +625,12 @@ module Exp = struct
L.die InternalError "virtual call with 0 args: %a" QualifiedProcName.pp proc )
| NonVirtual ->
F.fprintf fmt "%a%a" QualifiedProcName.pp proc pp_list args )
| Closure {proc; captured; params} ->
let captured_and_params =
captured @ List.map params ~f:(fun varname -> Load {exp= Lvar varname; typ= None})
in
F.fprintf fmt "(%a) -> %a(%a)" (pp_list_with_comma VarName.pp) params QualifiedProcName.pp
proc (pp_list_with_comma pp) captured_and_params
| Typ typ ->
F.fprintf fmt "<%a>" Typ.pp typ

Expand All @@ -635,6 +647,10 @@ module Exp = struct
do_not_contain_regular_call exp1 && do_not_contain_regular_call exp2
| Call {proc; args} ->
ProcDecl.is_not_regular_proc proc && List.for_all args ~f:do_not_contain_regular_call
| Apply {closure; args} ->
do_not_contain_regular_call closure && List.for_all args ~f:do_not_contain_regular_call
| Closure {captured} ->
List.for_all captured ~f:do_not_contain_regular_call


let vars exp =
Expand All @@ -648,8 +664,12 @@ module Exp = struct
aux acc exp
| Index (exp1, exp2) ->
aux (aux acc exp1) exp2
| Apply {closure; args} ->
List.fold args ~init:(aux acc closure) ~f:aux
| Call {args} ->
List.fold args ~init:acc ~f:aux
| Closure {captured} ->
List.fold captured ~init:acc ~f:aux
in
aux Ident.Set.empty exp
end
Expand Down
4 changes: 3 additions & 1 deletion infer/src/textual/Textual.mli
Original file line number Diff line number Diff line change
Expand Up @@ -245,13 +245,15 @@ module Exp : sig
| Index of t * t (** an array index offset: [exp1\[exp2\]] *)
| Const of Const.t
| Call of {proc: QualifiedProcName.t; args: t list; kind: call_kind}
| Closure of {proc: QualifiedProcName.t; captured: t list; params: VarName.t list}
| Apply of {closure: t; args: t list}
| Typ of Typ.t

val call_non_virtual : QualifiedProcName.t -> t list -> t

val call_virtual : QualifiedProcName.t -> t -> t list -> t

val call_sig : QualifiedProcName.t -> t list -> Lang.t option -> ProcSig.t
val call_sig : QualifiedProcName.t -> int -> Lang.t option -> ProcSig.t

(* logical not ! *)
val not : t -> t
Expand Down
16 changes: 11 additions & 5 deletions infer/src/textual/TextualBasicVerification.ml
Original file line number Diff line number Diff line change
Expand Up @@ -56,18 +56,18 @@ let verify_decl ~env errors (decl : Module.decl) =
then errors
else UnknownField field :: errors
in
let verify_call loc errors proc args =
let verify_call loc errors proc nb_args =
if ProcDecl.is_not_regular_proc proc then errors
else
let procsig = Exp.call_sig proc args (TextualDecls.lang env) in
let procsig = Exp.call_sig proc nb_args (TextualDecls.lang env) in
match TextualDecls.get_procdecl env procsig with
| None when QualifiedProcName.contains_wildcard proc ->
errors
| None ->
UnknownProc {proc; args= List.length args} :: errors
UnknownProc {proc; args= nb_args} :: errors
| Some {formals_types= Some formals_types} ->
let formals = List.length formals_types in
let args = List.length args in
let args = nb_args in
if not (Int.equal args formals) then WrongArgNumber {proc; args; formals; loc} :: errors
else errors
| Some {formals_types= None} ->
Expand All @@ -87,7 +87,13 @@ let verify_decl ~env errors (decl : Module.decl) =
verify_exp loc errors e2
| Call {proc; args} ->
let errors = List.fold ~f:(verify_exp loc) ~init:errors args in
verify_call loc errors proc args
verify_call loc errors proc (List.length args)
| Closure {proc; captured; params} ->
let errors = List.fold ~f:(verify_exp loc) ~init:errors captured in
verify_call loc errors proc (List.length captured + List.length params)
| Apply {closure; args} ->
let errors = verify_exp loc errors closure in
List.fold ~f:(verify_exp loc) ~init:errors args
in
let verify_instr errors (instr : Instr.t) =
let loc = Instr.loc instr in
Expand Down
4 changes: 4 additions & 0 deletions infer/src/textual/TextualDecls.ml
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,8 @@ let get_procdesc_referenced_types (pdesc : ProcDesc.t) =
(* Helpers *)
let rec from_exp (exp : Exp.t) =
match exp with
| Apply {closure; args} ->
List.iter (closure :: args) ~f:from_exp
| Typ typ ->
get_typ_name typ |> Option.iter ~f:add_to_referenced
| Var _ | Lvar _ | Const _ ->
Expand All @@ -237,6 +239,8 @@ let get_procdesc_referenced_types (pdesc : ProcDesc.t) =
from_exp idx
| Call {args} ->
List.iter args ~f:from_exp
| Closure {captured} ->
List.iter captured ~f:from_exp
and from_bexp (bexp : BoolExp.t) =
match bexp with
| Exp exp ->
Expand Down
2 changes: 2 additions & 0 deletions infer/src/textual/TextualLexer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,8 @@ let build_mainlex keywords =
| "#", ident ->
let lexeme = Lexbuf.lexeme lexbuf in
LABEL (String.subo ~pos:1 lexeme)
| "fun", blanks, "(" ->
FUN
| ("?" | ident), blanks, ".", blanks, ident, blanks, "(" -> (
let lexeme = Lexbuf.lexeme lexbuf in
match String.split_on_chars lexeme ~on:['.'; '('] with
Expand Down
28 changes: 28 additions & 0 deletions infer/src/textual/TextualMenhir.mly
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
%token EXTENDS
%token FALSE
%token FLOAT
%token FUN
%token GLOBAL
%token HANDLERS
%token IF
Expand Down Expand Up @@ -422,7 +423,34 @@ expression:
{ Exp.Const c }
| proc=opt_qualified_pname_and_lparen args=separated_list(COMMA, expression) RPAREN
{ Exp.Call {proc; args; kind= Exp.NonVirtual} }
| closure=expression LPAREN args=separated_list(COMMA, expression) RPAREN
(* remark: the lexer will never generate the sequence IDENT LPAREN because PROC_AND_LPAREN
is more prioritary. We will fix that using TextualTransform.FixClosureAppExpr later *)
{ Exp.Apply {closure; args} }
| recv=expression DOT proc=opt_qualified_pname_and_lparen args=separated_list(COMMA, expression) RPAREN
{ Exp.call_virtual proc recv args }
| FUN params=separated_list(COMMA, vname) RPAREN ARROW
proc=opt_qualified_pname_and_lparen args=separated_list(COMMA, expression) RPAREN
{
let syntax_error () =
let loc = location_of_pos $startpos(params) in
let string = F.asprintf "call inside closure should end with %a"
(Pp.seq ~sep:"," VarName.pp) params in
raise (SpecialSyntaxError (loc, string))
in
let nb_params = List.length params in
let nb_args = List.length args in
if nb_params > nb_args then syntax_error ()
else
let captured, params2 = List.split_n args (nb_args - nb_params) in
let match_param (e: Exp.t) (x: VarName.t) =
match e with
| Exp.Load {exp=Lvar varname; typ=None} -> VarName.equal varname x
| _ -> false
in
if List.for_all2_exn ~f:match_param params2 params then
Exp.Closure {proc; captured; params}
else syntax_error ()
}
| LABRACKET typ=typ RABRACKET
{ Exp.Typ typ }
3 changes: 3 additions & 0 deletions infer/src/textual/TextualParser.ml
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,9 @@ let parse_buf sourcefile filebuf =
let parsed =
MenhirLib.Convert.Simplified.traditional2revised TextualMenhir.main lexer sourcefile
in
(* the parser needs context to understand ident(args) expression because ident may be
a variable or a procname *)
let parsed = TextualTransform.fix_closure_app parsed in
let errors, decls_env = TextualDecls.make_decls parsed in
let errors = List.map errors ~f:(fun x -> DeclaredTwiceError x) in
if List.is_empty errors then
Expand Down
33 changes: 23 additions & 10 deletions infer/src/textual/TextualSil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,18 @@ let python_mixed_type_name = SilTyp.PythonClass (PythonClassName.make "PyObject"

let mk_python_mixed_type_textual loc = Typ.Struct TypeName.{value= "PyObject"; loc}

let default_return_type (lang : Lang.t option) loc =
match lang with
| Some Hack ->
Typ.Ptr (mk_hack_mixed_type_textual loc)
| Some Python ->
Typ.Ptr (mk_python_mixed_type_textual loc)
| Some other ->
L.die InternalError "Unexpected return type outside of Hack/Python: %s" (Lang.to_string other)
| None ->
L.die InternalError "Unexpected return type outside of Hack/Python: None"


let mangle_java_procname jpname =
let method_name =
match Procname.Java.get_method jpname with "<init>" -> "__sil_java_constructor" | s -> s
Expand Down Expand Up @@ -583,7 +595,7 @@ module ExpBridge = struct
| Call {proc; args= [Typ typ; exp]} when ProcDecl.is_cast_builtin proc ->
Cast (TypBridge.to_sil lang typ, aux exp)
| Call {proc; args} -> (
let procsig = Exp.call_sig proc args (TextualDecls.lang decls_env) in
let procsig = Exp.call_sig proc (List.length args) (TextualDecls.lang decls_env) in
match
( TextualDecls.get_procdecl decls_env procsig
, ProcDecl.to_unop proc
Expand All @@ -605,6 +617,8 @@ module ExpBridge = struct
(* FIXME: transform instruction to put call at head of expressions *) )
| Typ _ ->
L.die InternalError "Internal error: type expressions should not appear outside builtins"
| Closure _ | Apply _ ->
L.die InternalError "Internal error: closures should not appear inside sub-expressions"
in
aux exp
end
Expand Down Expand Up @@ -743,7 +757,7 @@ module InstrBridge = struct
Call ((ret, class_type), builtin, args, loc, CallFlags.default)
| Let {id; exp= Call {proc; args; kind}; loc} ->
let ret = IdentBridge.to_sil id in
let procsig = Exp.call_sig proc args (TextualDecls.lang decls_env) in
let procsig = Exp.call_sig proc (List.length args) (TextualDecls.lang decls_env) in
let ({formals_types} as callee_procname : ProcDecl.t) =
match TextualDecls.get_procdecl decls_env procsig with
| Some procname ->
Expand All @@ -752,14 +766,7 @@ module InstrBridge = struct
let textual_ret_typ =
(* Declarations with unknown formals are expected in Hack/Python. Assume that unknown
return types are *HackMixed/*PyObject respectively. *)
match lang with
| Lang.Hack ->
Typ.Ptr (mk_hack_mixed_type_textual loc)
| Lang.Python ->
Typ.Ptr (mk_python_mixed_type_textual loc)
| other ->
L.die InternalError "Unexpected return type outside of Hack/Python: %s"
(Lang.to_string other)
default_return_type (Some lang) loc
in
{ ProcDecl.qualified_name= proc
; formals_types= None
Expand Down Expand Up @@ -803,6 +810,12 @@ module InstrBridge = struct
let cf_virtual = Exp.equal_call_kind kind Virtual in
let cflag = {CallFlags.default with cf_virtual} in
Call ((ret, result_type), Const (Cfun pname), args, loc, cflag)
| Let {exp= Closure _; loc} ->
let msg = lazy "closure construction should have been transformed before SIL conversion" in
raise (TextualTransformError [{loc; msg}])
| Let {exp= Apply _; loc} ->
let msg = lazy "closure call should have been transformed before SIL conversion" in
raise (TextualTransformError [{loc; msg}])
| Let {loc; _} ->
let msg = lazy (F.asprintf "the expression in %a should start with a regular call" pp i) in
raise (TextualTransformError [{loc; msg}])
Expand Down
2 changes: 2 additions & 0 deletions infer/src/textual/TextualSil.mli
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ val from_java : filename:string -> Tenv.t -> Cfg.t -> unit
val dump_module : filename:string -> Textual.Module.t -> unit
(** generate a .sil file with name [filename] with all the content of the input module *)

val default_return_type : Textual.Lang.t option -> Textual.Location.t -> Textual.Typ.t

val hack_dict_type_name : Typ.name

val hack_vec_type_name : Typ.name
Expand Down
Loading

0 comments on commit db6e322

Please sign in to comment.