ExpoSEJS / ExpoSE

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

How to understand output report ?? #113

Closed trungkien20020428 closed 7 months ago

trungkien20020428 commented 7 months ago

I run something in tests folder like :

./expoSE tests/regex/match/captures/anchors.js

and give some report like that :

[+] ExpoSE /home/kien/ExpoSE/tests/regex/match/captures/anchors.js concurrent: 8 timeout: 7200000 per-test: 2400000
[\] [0 done /0 queued / 1 running / 0 errors / 0% coverage ] ***(node:1001) [DEP0005] DeprecationWarning: Buffer() is deprecated due to security and usability issues. Please use the Buffer.alloc(), Buffer.allocUnsafe(), or Buffer.from() methods instead.
(Use `node --trace-deprecation ...` to show where the warning was created)
[-] [4 done /0 queued / 0 running / 3 errors / 32% coverage ] ***
[+] {"_bound":0,"X":""} took 5.923s
[+] {"X":"abc","_bound":14} took 4.932s
[!] Reachable
[!] expoSE replay '/home/kien/ExpoSE/tests/regex/match/captures/anchors.js' '{"X":"abc","_bound":14}'
[+] {"X":"abchello","_bound":19} took 6.257s
[!] Reachable
[!] expoSE replay '/home/kien/ExpoSE/tests/regex/match/captures/anchors.js' '{"X":"abchello","_bound":19}'
[+] {"X":"helloabc","_bound":18} took 6.267s
[!] Reachable
[!] expoSE replay '/home/kien/ExpoSE/tests/regex/match/captures/anchors.js' '{"X":"helloabc","_bound":18}'
[!] Stats
[+] General Function Call: 20
[+] Symbolic Values: 4
[+] Symbolic Primitives: 4
[+] Wrapped Constants: 20
[+] Symbolic Field: 4
[+] Modeled Function Call: {"#match":4}
[+] Regex Encoded: 4
[+] Regex Which May Need Checks: 4
[+] Regex Checks: 6
[+] Max Queries (Any): 1
[+] Max Queries (Succesful): 1
[+] Symbolic Binary: 16
[+] Failed Queries: 5
[!] Done
[+] /home/kien/ExpoSE/tests/regex/match/captures/anchors.js. Coverage (Term): 82% Coverage (Decisions): 69% Coverage (LOC): 100% Lines Of Code: 20 -*
[+] Total Lines Of Code 20
[+] Total Coverage: 1%
[+] EXPOSE_PRINT_COVERAGE=1 for line by line breakdown
[+] ExpoSE Finished. 4 paths, 3 errors

and it created a file like

J$.iids = {"8":[12,6,12,17],"9":[3,10,3,17],"10":[8,11,8,24],"16":[16,6,16,28],"17":[3,18,3,22],"18":[12,6,12,17],"24":[10,5,10,22],"25":[3,10,3,23],"26":[16,8,16,20],"33":[3,10,3,23],"34":[16,6,16,28],"41":[3,10,3,23],"49":[4,9,4,11],"57":[4,19,4,22],"65":[4,24,4,26],"73":[4,9,4,27],"75":[4,9,4,18],"81":[4,9,4,27],"89":[4,9,4,27],"97":[8,1,8,3],"105":[8,11,8,12],"113":[8,11,8,19],"121":[8,22,8,24],"129":[8,1,8,25],"131":[8,1,8,10],"137":[8,1,8,26],"145":[10,5,10,14],"153":[10,20,10,21],"161":[10,5,10,22],"163":[10,5,10,19],"169":[12,6,12,7],"177":[12,8,12,9],"185":[12,6,12,10],"193":[12,14,12,17],"201":[13,9,13,22],"209":[13,9,13,22],"217":[13,3,13,23],"225":[16,6,16,7],"233":[16,8,16,9],"241":[16,8,16,16],"249":[16,19,16,20],"257":[16,6,16,21],"265":[16,25,16,28],"273":[17,9,17,22],"281":[17,9,17,22],"289":[17,3,17,23],"297":[20,8,20,19],"305":[20,8,20,19],"313":[20,2,20,20],"321":[1,1,21,2],"329":[1,1,21,2],"337":[1,1,21,2],"345":[12,2,14,3],"353":[16,2,18,3],"361":[10,1,21,2],"369":[1,1,21,2],"377":[1,1,21,2],"nBranches":6,"originalCodeFileName":"/home/kien/ExpoSE/tests/regex/anchors/both.js","instrumentedCodeFileName":"/home/kien/ExpoSE/tests/regex/anchors/both_jalangi_.js","code":"/* Copyright (c) Royal Holloway, University of London | Contact Blake Loring (blake@parsed.uk), Duncan Mitchell (Duncan.Mitchell.2015@rhul.ac.uk), or Johannes Kinder (johannes.kinder@rhul.ac.uk) for details or support | LICENSE.md for license details */\n\n'use strict';\nvar S$ = require('S$');\nvar q = S$.symbol(\"q\", '');\n\n//This assumption is required to make the testcase solve in reasonable time with Z3\n//This is not due to the regular expression but in fact due to the q.length and str.at\nS$.assume(q.length < 10);\n\nif (/^--.+=$/.test(q)) {\n\n\tif (q[0] != '-') {\n\t\tthrow 'Unreachable';\n\t}\n\n\tif (q[q.length - 1] != '=') {\n\t\tthrow 'Unreachable';\n\t}\n\n\tthrow 'Reachable';\n}\n"};
jalangiLabel0:
    while (true) {
        try {
            J$.Se(321, '/home/kien/ExpoSE/tests/regex/anchors/both_jalangi_.js', '/home/kien/ExpoSE/tests/regex/anchors/both.js');
            J$.N(329, 'S$', S$, 0);
            J$.N(337, 'q', q, 0);
            var S$ = J$.X1(41, J$.W(33, 'S$', J$.F(25, J$.R(9, 'require', require, 2), 0)(J$.T(17, 'S$', 21, false)), S$, 3));
            var q = J$.X1(89, J$.W(81, 'q', J$.M(73, J$.R(49, 'S$', S$, 1), 'symbol', 0)(J$.T(57, "q", 21, false), J$.T(65, '', 21, false)), q, 3));
            J$.X1(137, J$.M(129, J$.R(97, 'S$', S$, 1), 'assume', 0)(J$.B(10, '<', J$.G(113, J$.R(105, 'q', q, 1), 'length', 0), J$.T(121, 10, 22, false), 0)));
            if (J$.X1(361, J$.C(24, J$.M(161, J$.T(145, /^--.+=$/, 14, false), 'test', 0)(J$.R(153, 'q', q, 1))))) {
                if (J$.X1(345, J$.C(8, J$.B(18, '!=', J$.G(185, J$.R(169, 'q', q, 1), J$.T(177, 0, 22, false), 4), J$.T(193, '-', 21, false), 0)))) {
                    throw J$.X1(217, J$.Th(209, J$.T(201, 'Unreachable', 21, false)));
                }
                if (J$.X1(353, J$.C(16, J$.B(34, '!=', J$.G(257, J$.R(225, 'q', q, 1), J$.B(26, '-', J$.G(241, J$.R(233, 'q', q, 1), 'length', 0), J$.T(249, 1, 22, false), 0), 4), J$.T(265, '=', 21, false), 0)))) {
                    throw J$.X1(289, J$.Th(281, J$.T(273, 'Unreachable', 21, false)));
                }
                throw J$.X1(313, J$.Th(305, J$.T(297, 'Reachable', 21, false)));
            }
        } catch (J$e) {
            J$.Ex(369, J$e);
        } finally {
            if (J$.Sr(377)) {
                J$.L();
                continue jalangiLabel0;
            } else {
                J$.L();
                break jalangiLabel0;
            }
        }
    }
// JALANGI DO NOT INSTRUMENT

term '// JALANGI DO NOT INSTRUMENT' like me run something wrong ?

I am not know why total Coverage is so less.

And does it have something like string test make regex failed ? Thank you. Kien Hoang

trungkien20020428 commented 7 months ago

I already understand this report so i close this issue.