[hack][textual] introducing a wildcard qualifier for fields and procn…

…ames

Summary:
The HackC compiler has not enough type information in hands to
fully qualify all fieldnames and procnames. In such a situation we prefer to introduce
a specific name ? and treat it specially when type-checking textual IR and emitting
SIL representation.

Reviewed By: vsiles

Differential Revision: D45601108

fbshipit-source-id: 903c5a456403fce5ed545f16aec7caf50d133b60

infer/src/IR/HackClassName.ml

@@ -19,6 +19,8 @@ let components {namespace; classname} =
   match namespace with Some ns -> [ns; classname] | _ -> [classname]
 
 
+let wildcard = make "?"
+
 let pp fmt {namespace; classname} =
   match namespace with
   | Some ns ->

infer/src/IR/HackClassName.mli

@@ -16,6 +16,8 @@ val classname : t -> string
 
 val components : t -> string list
 
+val wildcard : t
+
 val pp : F.formatter -> t -> unit
 
 val to_string : t -> string

infer/src/pulse/PulseModelsHack.ml

@@ -25,8 +25,7 @@ let hack_dim_field_get this_obj (field_string_obj, _) : model =
   match read_boxed_string_value field_string_obj astate with
   | Some string_val ->
       (* TODO: add a move up in the class hierarchy to find the right field declaration *)
-      let class_name = TextualSil.hack_mixed_type_name in
-      let field = Fieldname.make class_name string_val in
+      let field = TextualSil.wildcard_sil_fieldname Textual.Lang.Hack string_val in
       let<*> astate, this_val =
         PulseOperations.eval_access path Read location this_obj Dereference astate
       in

infer/src/textual/CombinedMenhir.mly

@@ -101,10 +101,12 @@
 %type <Attr.t> attribute
 %type <Module.decl> declaration
 %type <qualified_procname> qualified_pname
+%type <qualified_procname> opt_qualified_pname
 %type <ProcName.t> pname
 %type <FieldName.t> fname
 %type <NodeName.t> nname
 %type <TypeName.t> tname
+%type <TypeName.t> opt_tname
 %type <VarName.t> vname
 %type <Attr.t list> annots
 %type <Attr.t> annot
@@ -169,6 +171,12 @@ tname:
   | id=ident
     { { TypeName.value=id; loc=location_of_pos $startpos(id) } }
 
+opt_tname:
+  | tname=tname
+    { tname }
+  | QUESTION
+    { { TypeName.value="?"; loc=location_of_pos $startpos } }
+
 vname:
   | id=ident
     { { VarName.value=id; loc=location_of_pos $startpos(id) } }
@@ -179,6 +187,12 @@ qualified_pname:
   | name=pname
     { ( {enclosing_class=TopLevel; name} : qualified_procname ) }
 
+opt_qualified_pname:
+  | tname=opt_tname DOT name=pname
+    { ( {enclosing_class=Enclosing tname; name} : qualified_procname) }
+  | name=pname
+    { ( {enclosing_class=TopLevel; name} : qualified_procname ) }
+
 attribute:
   | DOT name=ident EQ value=STRING
     { {Attr.name=name; values=[value]; loc=location_of_pos $startpos} }
@@ -363,16 +377,16 @@ expression:
     { Exp.Var (Ident.of_int id) }
   | AMPERSAND name=vname
     { Exp.Lvar name }
-  | exp=expression DOT enclosing_class=tname DOT name=fname
+  | exp=expression DOT enclosing_class=opt_tname DOT name=fname
     { let field : qualified_fieldname = {enclosing_class; name} in
       Exp.Field {exp; field} }
   | e1=expression LSBRACKET e2=expression RSBRACKET
     { Exp.Index (e1, e2) }
   | c=const
     { Exp.Const c }
-  | proc=qualified_pname LPAREN args=separated_list(COMMA, expression) RPAREN
+  | proc=opt_qualified_pname LPAREN args=separated_list(COMMA, expression) RPAREN
     { Exp.Call {proc; args; kind= Exp.NonVirtual} }
-  | recv=expression DOT proc=qualified_pname LPAREN args=separated_list(COMMA, expression) RPAREN
+  | recv=expression DOT proc=opt_qualified_pname LPAREN args=separated_list(COMMA, expression) RPAREN
     { Exp.call_virtual proc recv args }
   | LABRACKET typ=typ RABRACKET
     { Exp.Typ typ }

infer/src/textual/Textual.ml

@@ -123,7 +123,15 @@ let builtin_lazy_class_initialize = "__sil_lazy_class_initialize"
 
 let builtin_cast = "__sil_cast"
 
-module TypeName : NAME = Name
+module TypeName : sig
+  include NAME
+
+  val wildcard : t
+end = struct
+  include Name
+
+  let wildcard = {value= "?"; loc= Location.Unknown}
+end
 
 type enclosing_class = TopLevel | Enclosing of TypeName.t [@@deriving equal, hash]
 
@@ -142,6 +150,14 @@ let pp_qualified_procname fmt ({enclosing_class; name} : qualified_procname) =
   F.fprintf fmt "%a%a" pp_enclosing_class enclosing_class ProcName.pp name
 
 
+let qualified_procname_contains_wildcard {enclosing_class} =
+  match enclosing_class with
+  | Enclosing class_name ->
+      TypeName.equal class_name TypeName.wildcard
+  | TopLevel ->
+      false
+
+
 type qualified_fieldname = {enclosing_class: TypeName.t; name: FieldName.t}
 (* field name [name] must be declared in type [enclosing_class] *)
 

infer/src/textual/Textual.mli

@@ -51,7 +51,12 @@ module FieldName : NAME (* field names, without their enclosing types *)
 
 module NodeName : NAME (* node names, also called labels *)
 
-module TypeName : NAME (* structured value type name *)
+module TypeName : sig
+  (* structured value type name *)
+  include NAME
+
+  val wildcard : t
+end
 
 type enclosing_class = TopLevel | Enclosing of TypeName.t
 
@@ -61,6 +66,8 @@ type qualified_procname = {enclosing_class: enclosing_class; name: ProcName.t}
 
 val pp_qualified_procname : F.formatter -> qualified_procname -> unit
 
+val qualified_procname_contains_wildcard : qualified_procname -> bool
+
 type qualified_fieldname = {enclosing_class: TypeName.t; name: FieldName.t}
 (* field name [name] must be declared in type [enclosing_class] *)
 

infer/src/textual/TextualBasicVerification.ml

@@ -50,13 +50,19 @@ let verify_decl ~env errors (decl : Module.decl) =
     else UnknownLabel {label; pname} :: errors
   in
   let verify_field errors field =
-    if TextualDecls.is_field_declared env field then errors else UnknownField field :: errors
+    if
+      TypeName.equal field.enclosing_class TypeName.wildcard
+      || TextualDecls.is_field_declared env field
+    then errors
+    else UnknownField field :: errors
   in
   let verify_call loc errors proc args =
     if ProcDecl.is_not_regular_proc proc then errors
     else
       let procsig = Exp.call_sig proc args (TextualDecls.lang env) in
       match TextualDecls.get_procdecl env procsig with
+      | None when qualified_procname_contains_wildcard proc ->
+          errors
       | None ->
           UnknownProc {proc; args= List.length args} :: errors
       | Some {formals_types= Some formals_types} ->

infer/src/textual/TextualSil.ml

@@ -155,6 +155,14 @@ let mangle_java_procname jpname =
   F.asprintf "%s%a" method_name pp_java_types parameter_types
 
 
+let wildcard_sil_fieldname lang name =
+  match (lang : Lang.t) with
+  | Java | Python ->
+      L.die InternalError "a wildcard fieldname is only supported in Hack"
+  | Hack ->
+      SilFieldname.make (HackClass HackClassName.wildcard) name
+
+
 module TypBridge = struct
   open Typ
 
@@ -499,6 +507,8 @@ module ExpBridge = struct
           Lvar pvar
       | Field {exp; field} -> (
         match TextualDecls.get_fielddecl decls_env field with
+        | None when TypeName.equal field.enclosing_class TypeName.wildcard ->
+            Lfield (aux exp, wildcard_sil_fieldname lang field.name.value, SilTyp.mk SilTyp.Tvoid)
         | None ->
             L.die InternalError "field %a.%a has not been declared" TypeName.pp
               field.enclosing_class FieldName.pp field.name
@@ -655,6 +665,11 @@ module InstrBridge = struct
           match TextualDecls.get_procdecl decls_env procsig with
           | Some procname ->
               procname
+          | None when qualified_procname_contains_wildcard proc ->
+              { ProcDecl.qualified_name= proc
+              ; formals_types= None
+              ; result_type= Typ.mk_without_attributes Typ.Void
+              ; attributes= [] }
           | None ->
               let msg =
                 lazy (F.asprintf "the expression in %a should start with a regular call" pp i)

infer/src/textual/TextualSil.mli

@@ -22,3 +22,5 @@ val hack_mixed_type_name : Typ.name
 val hack_mixed_static_companion_type_name : Typ.name
 
 val hack_builtins_type_name : Typ.name
+
+val wildcard_sil_fieldname : Textual.Lang.t -> string -> Fieldname.t

infer/src/textual/TextualTypeVerification.ml

@@ -45,7 +45,7 @@ let rec compat ~assigned:(t1 : Typ.t) ~given:(t2 : Typ.t) =
 
 let is_ptr = function Typ.Ptr _ -> true | _ -> false
 
-let is_ptr_struct = function Typ.Ptr (Struct _) -> true | _ -> false
+let is_ptr_struct = function Typ.Ptr (Struct _) | Typ.Void -> true | _ -> false
 
 let is_int = function Typ.Int -> true | _ -> false
 
@@ -213,6 +213,8 @@ let typeof_var var : Typ.t monad =
 let typeof_field field : Typ.t monad =
  fun state ->
   match TextualDecls.get_fielddecl state.decls field with
+  | None when TypeName.equal field.enclosing_class TypeName.wildcard ->
+      ret Typ.Void state
   | None ->
       (* such an error should have been caught in TextualVerification *)
       L.die InternalError "Textual type verification: field %a is unknown" pp_qualified_fieldname
@@ -293,6 +295,8 @@ let typeof_procname (procsig : ProcSig.t) : (Typ.t * Typ.t list option) monad =
         |> Option.map ~f:(fun formals_types -> List.map formals_types ~f:(fun {Typ.typ} -> typ))
       in
       ret (procdecl.result_type.typ, formals_types) state
+  | None when ProcSig.to_qualified_procname procsig |> qualified_procname_contains_wildcard ->
+      ret (Typ.Void, None) state
   | None ->
       ret (typeof_reserved_proc (ProcSig.to_qualified_procname procsig)) state
 

infer/tests/codetoanalyze/sil/pulse/Makefile

@@ -15,6 +15,6 @@ CAPTURE_CMD = $(patsubst %.sil, --capture-textual %.sil,$(SOURCES))
 default: test
 
 $(INFER_OUT)/report.json: $(SOURCES) $(INFER_BIN)
-	$(INFER_BIN) --quiet --no-progress-bar --pulse-only \
+	$(INFER_BIN) --quiet --no-progress-bar --pulse-only\
           --debug-exceptions --dump-duplicate-symbols -o $(INFER_OUT) $(CAPTURE_CMD) \
           --capture-textual models/models.sil

infer/tests/codetoanalyze/sil/pulse/hack_dim_field_get.sil

@@ -7,9 +7,7 @@
 
 type cell = { value:int; next: *cell }
 
-type list extends HackMixed = {}
-
-type HackMixed = { header: *cell }
+type list = {}
 
 define bad(l: *list) : void {
   local temp : **list
@@ -19,7 +17,7 @@ define bad(l: *list) : void {
     n2 = $builtins.hack_dim_field_get(n0, n1)
     store n2 <- null: *cell
     n3: *list = load &l
-    n4: *cell = load n3.HackMixed.header
+    n4: *cell = load n3.?.header
     n5: *cell = load n4.cell.next
     ret null
 }
@@ -32,7 +30,7 @@ define good(l: *list) : void {
     n2 = $builtins.hack_dim_field_get(n0, n1)
     store n2 <- __sil_allocate(<cell>): *cell
     n3: *list = load &l
-    n4: *cell = load n3.HackMixed.header
+    n4: *cell = load n3.?.header
     n5: *cell = load n4.cell.next
     ret null
 }

infer/tests/codetoanalyze/sil/pulse/hack_object.sil

@@ -100,7 +100,7 @@ local $a: *void, $0: *void, $1: *void, $2: *void
   prune $builtins.hack_is_true(n7)
   n8: *HackMixed = load &$2
   n9 = $builtins.hhbc_cast_vec($builtins.hhbc_new_col_vector())
-  n10 = n8.HackMixed._86reifiedinit(n9)
+  n10 = n8.?._86reifiedinit(n9)
   jmp b6
   .handlers b7
 #b5:
@@ -124,7 +124,7 @@ local $a: *void, $0: *void, $1: *void, $2: *void
   store &$1 <- null: *HackMixed
   store &$2 <- null: *HackMixed
   n16: *HackMixed = load &$f
-  n17 = n13.HackMixed.__construct(n16)
+  n17 = n13.?.__construct(n16)
   n18 = $builtins.hhbc_lock_obj(n13)
   n24 = $builtins.hhbc_is_type_struct_c(n13, n0, $builtins.hack_int(1))
   n25 = $builtins.hhbc_verify_type_pred(n13, n24)
@@ -142,9 +142,9 @@ local $a: *A
   n2 = make(n0, n1)
   store &$a <- n2: *HackMixed
   n20: *HackMixed = load &$a
-  n21 = n20.HackMixed.setField(null)
+  n21 = n20.?.setField(null)
   n22: *HackMixed = load &$a
-  n23 = n22.HackMixed.getField()
+  n23 = n22.?.getField()
   n24 : *HackMixed = load n23.F.val
   ret null
 }
@@ -160,9 +160,9 @@ local $a: *A
   n2 = make(n0, n1)
   store &$a <- n2: *HackMixed
   n20: *HackMixed = load &$a
-  n21 = n20.HackMixed.setField(__sil_allocate(<F>))
+  n21 = n20.?.setField(__sil_allocate(<F>))
   n22: *HackMixed = load &$a
-  n23 = n22.HackMixed.getField()
+  n23 = n22.?.getField()
   n24 : *HackMixed = load n23.F.val
   ret null
 }
@@ -176,10 +176,6 @@ declare $builtins.hhbc_is_type_struct_c(...): *HackMixed
 declare $builtins.hhbc_lock_obj(...): *HackMixed
 declare $builtins.hhbc_throw(...): *HackMixed
 declare $builtins.hhbc_verify_type_pred(...): *HackMixed
-declare HackMixed._86reifiedinit(...): *HackMixed
-declare HackMixed.__construct(...): *HackMixed
-declare HackMixed.getField(...): *HackMixed
-declare HackMixed.setField(...): *HackMixed
 
 declare $builtins.hack_dim_field_get(**HackMixed, *HackMixed): **HackMixed
 declare $builtins.hack_int(int): *HackInt

infer/tests/codetoanalyze/sil/verif/basic.sil

@@ -27,6 +27,8 @@ define f(x: int, y: float, n: *node, a: *int[]) : void {
     n4: *node = load &n
     store n4.node.val <- n1:int
     store n3.node.val <- n1:int
+    store n4.?.val <- n1:int
+    n5 = ?.cons(1, n3)
     ret n2
   #lab2:
     store &z <- 1: int

infer/tests/codetoanalyze/sil/verif/issues.exp

@@ -3,16 +3,16 @@ annotated.sil, line 22, column 4: textual type error: expression &n has type **n
 basic.sil, line 17, column 4: textual type error: expression &y has type *float, while a subtype of *int was expected
 basic.sil, line 18, column 4: textual type error: expression &n has type **node, while a pointer of array type was expected
 basic.sil, line 20, column 4: textual type error: expression n1 has type int, while a subtype of *node was expected
-basic.sil, line 33, column 4: textual type error: variable u has not been declared
-basic.sil, line 34, column 4: textual type error: ident n0 is given the type float, but it has already been given the type int at line 17
+basic.sil, line 35, column 4: textual type error: variable u has not been declared
+basic.sil, line 36, column 4: textual type error: ident n0 is given the type float, but it has already been given the type int at line 17
 basic.sil, line 24, column 4: textual type error: expression n0 has type int, while a subtype of float was expected
 basic.sil, line 24, column 4: textual type error: expression &x has type *int, while a supertype of *float was expected
 basic.sil, line 25, column 4: textual type error: expression n1 has type int, while a subtype of float was expected
 basic.sil, line 25, column 4: textual type error: expression &x has type *int, while a pointer of array type was expected
 basic.sil, line 29, column 4: textual type error: expression n3 has type *int[], while a pointer of struct type was expected
-basic.sil, line 47, column 4: textual type error: ident n1 is read before being written
-basic.sil, line 58, column 4: textual type error: builtin __sil_allocate is called with 2 arguments while it expects 1
-basic.sil, line 60, column 4: textual type error: expression 0 has type int, while the type of all types was expected
+basic.sil, line 49, column 4: textual type error: ident n1 is read before being written
+basic.sil, line 60, column 4: textual type error: builtin __sil_allocate is called with 2 arguments while it expects 1
+basic.sil, line 62, column 4: textual type error: expression 0 has type int, while the type of all types was expected
 basic_error_argnum.sil, line 12, column 17: SIL consistency error: function $builtins.bar which can be called with 0 arguments is not declared
 error1.sil, line 12, column 4: SIL syntax error: unexpected token x
 error2.sil, line 19, column 9: SIL consistency error: function g which can be called with 0 arguments is not declared