A Dynamic Symbolic Execution (DSE) engine for JavaScript. ExpoSE is highly scalable, compatible with recent JavaScript standards, and supports symbolic modelling of strings and regular expressions.
MIT License
183
stars
36
forks
source link
Possibly incorrect outputs in OUTPUT_LOAD_EVENT #87
But according to this output, this OUTPUT_LOAD_EVENT has no parent process ("createdFromParent": "N/A") and is generated from the true branch of the previous PC's 24th assertion ("createdAtFork": 24). However, this PUUID doesn't have a 24th assertion, because it has only a single define-funs-rec. Am I misunderstanding something from here?
Also, multiple OUTPUT_LOAD_EVENT from the same PUUID: 11847 have the same "depth" and "createdAtDepth": they have the "depth" either 0 or 2. So we cannot distinguish where each OUTPUT_LOAD_EVENT node should be located in the tree. I thought "depth" within the same PUUID should be incremented whenever a new OUTPUT_LOAD_EVENT is created, isn't it?
If I run https://1688.com, I get the following output:
[249915:0905/001635.380864:INFO:CONSOLE(12207)] "PUUID: 11847, OUTPUT_LOADEVENT: !!!{"depth":0,"createdFromParent":"N/A","createdFrom":true,"createdAtDepth":2,"createdAtFork":24}!!! !!!Solver { (define-funs-rec ( ( str.repeat ((x!1 String) (x!2 Int)) String) ( str.whiteLeft ((x!1 String) (x!2 Int)) Int) ( str.whiteRight ((x!1 String) (x!2 Int)) Int)) ( (ite (<= x!2 0) "" (str.++ x!1 (( str.repeat 0) x!1 (- x!2 1)))) (ite (= (str.at x!1 x!2) " ") (( str.whiteLeft 0) x!1 (+ x!2 1)) x!2) (ite (= (str.at x!1 x!2) " ") (( str.whiteRight 0) x!1 (- x!2 1)) x!2))) }!!! !!!"https://astyle.alicdn.com/pkg/@alife/refly-vendors/1.0.0/src/browser-update/browser-update.css?_v=f5edf2a8db75a4731dfc4310931ef708.css"!!! !!!""!!!", source: https://www.1688.com/ (12207)
But according to this output, this OUTPUT_LOAD_EVENT has no parent process ("createdFromParent": "N/A") and is generated from the true branch of the previous PC's 24th assertion ("createdAtFork": 24). However, this PUUID doesn't have a 24th assertion, because it has only a single define-funs-rec. Am I misunderstanding something from here?
Also, multiple OUTPUT_LOAD_EVENT from the same PUUID: 11847 have the same "depth" and "createdAtDepth": they have the "depth" either 0 or 2. So we cannot distinguish where each OUTPUT_LOAD_EVENT node should be located in the tree. I thought "depth" within the same PUUID should be incremented whenever a new OUTPUT_LOAD_EVENT is created, isn't it?