An executable formal semantics of PHP with applications to program analysis