Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement open/write syscall in Engine #20

Closed
ChristianMoesl opened this issue Aug 30, 2020 · 1 comment
Closed

Implement open/write syscall in Engine #20

ChristianMoesl opened this issue Aug 30, 2020 · 1 comment
Assignees
Labels
feature New feature or request released

Comments

@ChristianMoesl
Copy link
Collaborator

ChristianMoesl commented Aug 30, 2020

No description provided.

@ChristianMoesl ChristianMoesl added the feature New feature or request label Aug 30, 2020
@ChristianMoesl ChristianMoesl removed this from the RISC-U Symbolic Executor milestone Feb 15, 2021
@ChristianMoesl ChristianMoesl changed the title Implement all 5 syscalls in Data-Flow-Graph Builder Implement all 5 syscalls in Engine Feb 15, 2021
@ChristianMoesl ChristianMoesl changed the title Implement all 5 syscalls in Engine Implement open syscalls in Engine Feb 15, 2021
@ChristianMoesl ChristianMoesl changed the title Implement open syscalls in Engine Implement open syscall in Engine Feb 15, 2021
@ChristianMoesl ChristianMoesl changed the title Implement open syscall in Engine Implement open/write syscall in Engine Mar 1, 2021
@mstarzinger mstarzinger self-assigned this Mar 1, 2021
mstarzinger added a commit that referenced this issue Mar 8, 2021
This commit adds support for the `write` syscall to symbolic execution and rarity simulation. It also changes how invalid addresses passed to `read` and `write` are handled by reporting them as bugs now.
ChristianMoesl pushed a commit that referenced this issue Mar 10, 2021
This commit adds support for the `write` syscall to symbolic execution and rarity simulation. It also changes how invalid addresses passed to `read` and `write` are handled by reporting them as bugs now.
ChristianMoesl pushed a commit that referenced this issue Mar 10, 2021
This commit adds support for the `write` syscall to symbolic execution and rarity simulation. It also changes how invalid addresses passed to `read` and `write` are handled by reporting them as bugs now.
ChristianMoesl pushed a commit that referenced this issue Mar 10, 2021
This commit adds support for the `write` syscall to symbolic execution and rarity simulation. It also changes how invalid addresses passed to `read` and `write` are handled by reporting them as bugs now.
ChristianMoesl pushed a commit that referenced this issue Mar 10, 2021
# [0.3.0](v0.2.0...v0.3.0) (2021-03-10)

### Bug Fixes

* ordering for harmonic mean (less is always better) ([#114](#114)) ([8ae2be8](8ae2be8))
* **rarity:** use right amount of values for mean calculation ([#114](#114)) ([c365767](c365767))
* broken build due to wrong Selfie repo URL ([883821b](883821b))
* enforce unique input variable names for Z3/Boolector ([#111](#111)) ([a0ed9d4](a0ed9d4))
* swapped handling of --iterations and --selection ([#113](#113)) ([c05c743](c05c743))
* **rarity:** Add warning message to ignored partial read ([43e8297](43e8297))
* **rarity:** detect REMU with 0 remainder as bug ([8e989cb](8e989cb))
* **rarity:** Fix filtering before enumerating skewing scoring counter index ([6e99b15](6e99b15))
* **rarity:** Fix rarity scoring ([ba7d0ed](ba7d0ed))
* **rarity:** implemented score algorithm exactly as in the paper ([afe4e9d](afe4e9d))
* **rarity:** push the raw input values only ([d6448bb](d6448bb))
* **rarity:** update dependencies to be compatible with Selfie ([0e86d8d](0e86d8d))
* **rarity:** Use correct format string flag for Format trait ([13cd96c](13cd96c))
* **rarity:** Use f64 for rarity score instead of u64 ([bd363e1](bd363e1))

### Features

* add coin-flip execution path exploration strategy ([081ec28](081ec28))
* create api for rarity simulation ([10aded4](10aded4))
* implement write syscall in engine ([#20](#20)) ([#109](#109)) ([d2fffde](d2fffde))
* **rarity:** adapt engine file for rarity simulation ([aa39116](aa39116))
* **rarity:** add benchmarks as submodule ([d4cb2be](d4cb2be))
* **rarity:** Add bytewise state comparator ([ef72317](ef72317))
* **rarity:** Add CLI parser config for rarity simulation ([7b9e001](7b9e001))
* **rarity:** CLI option to switch between harmonic and arithmetic mean ([90c4174](90c4174))
* **rarity:** detect bugs during concrete execution ([01ace2a](01ace2a))
* **rarity:** Implement copy-create ratio for newly created states ([00e3f10](00e3f10))
* **rarity:** implement search algorithm (breadth-first) ([09e5d64](09e5d64))
* **rarity:** Use harmonic mean as metric ([f30f41e](f30f41e))
ChristianMoesl added a commit that referenced this issue Jun 10, 2021
also implement BugFinder interface for symbolic execution engine

closes #20
ChristianMoesl added a commit that referenced this issue Jun 11, 2021
also implement BugFinder interface for symbolic execution engine

closes #20
ChristianMoesl added a commit that referenced this issue Jun 11, 2021
also implement BugFinder interface for symbolic execution engine

closes #20
ChristianMoesl pushed a commit that referenced this issue Jun 14, 2021
# [0.4.0](v0.3.0...v0.4.0) (2021-06-14)

### Bug Fixes

* **symbolic:** print actual progam exit status codes ([05d692e](05d692e))
* inverse value calculation for LHS of REMU ([#131](#131)) ([c24270a](c24270a))
* invertibility condition for SLTU (when `t != 0`) ([6947f52](6947f52))
* invertibility conditions DIVU and REMU ([#141](#141)) ([9c03995](9c03995))
* represent empty path condition as single true constant ([e1afdd6](e1afdd6))
* use ite to convert booleans to bitvectors ([5411f15](5411f15))
* **smt:** zero extend bitvectors for comp ops in external solver ([2576441](2576441))
* **test:** syntax errors in C* examples ([dc60453](dc60453))

### Features

* **symbolic:** add support for openat system call ([#20](#20)) ([de71a0c](de71a0c))
* create custom CLI command for SMT-lib file generation ([2e8eb46](2e8eb46))
* handle exit points with unknown satisfiability ([8891c64](8891c64))

### Performance Improvements

* switch rarity simulation to segmented memory ([7d31865](7d31865))
@github-actions
Copy link

🎉 This issue has been resolved in version 0.4.0 🎉

The release is available on:

Your semantic-release bot 📦🚀

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature New feature or request released
Projects
None yet
Development

No branches or pull requests

2 participants