FormatJson: microoptimizations for UTF8_OK mode

FormatJson: microoptimizations for UTF8_OK mode

* Replace strtr with str_replace where faster.
* Use addcslashes to escape json_encode's output. Because no control
  characters are included, the only characters that have to be
  escaped are \ and ". (irrelevant for PHP 5.4+ installations)

Re-encoding a ~1.5 MB API response from the Chinese Wikipedia:
* PHP 5.3: 32% faster (from 347 ms to 239 ms)
* PHP 5.4: 70% faster (from 51 ms to 15 ms)
* HHVM: 42% faster (from 326 ms to 191 ms)

Change-Id: I7c9342682986d40a2f2436ac978390b6018a3521