Building An Abstract-Syntax-Tree-Oriented Symbolic Execution Engine For Php Programs