[inferhack] rebox Hack strings

Summary: Unboxed `HackString`s confuse existing pointer-based logic (leading to formulae like `0 < "foo"`). This restores boxing (similar to treatment of HackInt) for the time being

Reviewed By: jvillard

Differential Revision: D57492969

fbshipit-source-id: 977d7adac705def07eb42719dbe653908023b1da

infer/src/pulse/PulseModelsDSL.mli

@@ -116,8 +116,6 @@ module Syntax : sig
 
  val eval_deref_access : access_mode -> aval -> Access.t -> aval model_monad
 
- val and_dynamic_type_is : aval -> Typ.t -> unit model_monad
-
  val get_dynamic_type :
  ask_specialization:bool -> aval -> Formula.dynamic_type_data option model_monad
 

infer/src/pulse/PulseModelsHack.ml

@@ -26,11 +26,14 @@ let mixed_type_name = TextualSil.hack_mixed_type_name
 
 let hack_string_type_name = TextualSil.hack_string_type_name
 
+let string_val_field = Fieldname.make hack_string_type_name "val"
+
 let read_string_value address astate = PulseArithmetic.as_constant_string astate address
 
 let read_string_value_dsl aval : string option DSL.model_monad =
  let open PulseModelsDSL.Syntax in
- let operation astate = (read_string_value (fst aval) astate, astate) in
+ let* inner_val = eval_deref_access Read aval (FieldAccess string_val_field) in
+ let operation astate = (read_string_value (fst inner_val) astate, astate) in
  let* opt_string = exec_operation operation in
  ret opt_string
 
@@ -266,9 +269,8 @@ let int_to_hack_int n : DSL.aval DSL.model_monad =
 
 let hack_string_dsl str_val : DSL.aval DSL.model_monad =
  let open DSL.Syntax in
- let* () = and_dynamic_type_is str_val (Typ.mk_struct hack_string_type_name) in
- let* () = and_positive str_val in
- ret str_val
+ let* ret_val = constructor hack_string_type_name [("val", str_val)] in
+ ret ret_val
 
 
 let hack_string str_val : model =
@@ -942,13 +944,13 @@ let hhbc_cmp_same x y : model =
  value_equality_test x_val y_val )
  else if Typ.Name.equal x_typ_name hack_string_type_name then (
  L.d_printfln "hhbc_cmp_same: both are strings" ;
- let* opt_str_x = read_string_value_dsl x in
- let* opt_str_y = read_string_value_dsl y in
- match Option.both opt_str_x opt_str_y with
- | Some (str_x, str_y) ->
- String.equal str_x str_y |> make_hack_bool
- | None ->
- make_hack_random_bool )
+ let* x_val = eval_deref_access Read x (FieldAccess string_val_field) in
+ let* y_val = eval_deref_access Read y (FieldAccess string_val_field) in
+ disjuncts
+  [ (let* () = prune_eq x_val y_val in
+  make_hack_bool true )
+  ; (let* () = prune_ne x_val y_val in
+  make_hack_bool false ) ] )
  else (
  L.d_printfln "hhbc_cmp_same: not a known primitive type" ;
  (* TODO(dpichardie) cover the comparisons of vec, keyset, dict and
@@ -1398,9 +1400,12 @@ let hhbc_cast_string arg : model =
 let hhbc_concat arg1 arg2 : model =
  let open DSL.Syntax in
  start_model
- @@ let* res = eval_string_concat arg1 arg2 in
- let* res = hack_string_dsl res in
- assign_ret res
+ @@
+ let* arg1_val = eval_deref_access Read arg1 (FieldAccess string_val_field) in
+ let* arg2_val = eval_deref_access Read arg2 (FieldAccess string_val_field) in
+ let* res = eval_string_concat arg1_val arg2_val in
+ let* res = hack_string_dsl res in
+ assign_ret res
 
 
 let matchers : matcher list =

infer/tests/codetoanalyze/hack/pulse/issues.exp

@@ -219,10 +219,8 @@ strings.hack, StringTests::Tests$static.cast_bad, 3, TAINT_ERROR, no_bucket, ERR
 strings.hack, StringTests::Tests$static.is_v1_bad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
 strings.hack, StringTests::Tests$static.is_v2_bad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
 strings.hack, StringTests::Tests$static.concat_bad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
-strings.hack, StringTests::Tests$static.FP_concat_ok, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
 strings.hack, StringTests::Tests$static.inlined_concat_bad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
 strings.hack, StringTests::Tests$static.call_string_eq_bad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
-strings.hack, StringTests::Tests$static.FP_call_string_eq_ok, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
 strings.hack, StringTests::Tests$static.call_string_ne_bad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,flows to this sink: value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource()
 subclasstest.hack, SubClassTest::Wrapper.checkTransBad, 3, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated here,awaitable becomes unreachable here]
 subclasstest.hack, SubClassTest::Wrapper.belowFactImplicationBad, 3, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated here,awaitable becomes unreachable here]

infer/tests/codetoanalyze/hack/pulse/strings.hack

@@ -83,7 +83,7 @@ class Tests {
  }
  }
 
- public static function FP_concat_ok(): void {
+ public static function concat_ok(): void {
  if (Main::concat_test("hello", "world") == "hello world") {
  \Level1\taintSink(\Level1\taintSource());
  }
@@ -123,7 +123,7 @@ class Tests {
  }
  }
 
- public static function FP_call_string_eq_ok(): void {
+ public static function call_string_eq_ok(): void {
  $arg1 = self::get_foo_string();
  $arg2 = "bar";
  if (self::string_eq($arg1, $arg2)) {