WIP: symbolic opcodes #3
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Owner
mmcloughlin
commented
Oct 4, 2024
mmcloughlin
commented
- Floating Point Fixes - Remove throws from generated code - Block inlining on FPRecipEstimate - Convert enums to bvs as a post-transform - Alter semantics to permit int/enum comparison, improving coverage testing results
- Update coverage results for new behaviour
- Add total case simplification
- ci: use nix
- ci: add vanilla opam build.
- dune: add yojson dependency
- add :aslt command for writing raw semantics (#39)
- readme: add publication (#54)
- Fix a typo and stub out some complex behaviours in spec
- Add bool prims to prim list
- Add missing prims for type inference in transforms
- StatefulIntToBit fixes
- Pass to remove temp dynamic bitvectors
- Rework mask support to reduce to bitops
- Centralise no_inline sets
- Extend stmt append to halt on terminal stmts
- Symbolic array accesses
- Some helpers for dealing with fn signatures
- Mostly working offline partial eval pipeline
- Build decoder tests without patterns or early returns
- Functionality to get the type of an expression post-dis
- Add entry point, coverage testing for offline
- Add a pass to replace register types with bits
- Add req transform for cases
- Extend offline to integer operations
- Add coverage script for offline
- Hack in prj file support to offline coverage, matching existing results
- Reduce debug printing
- Fixes for branches
- Fixes for memory operations
- Prevent large vector ops for now
- Partially extend req patterns
- Extend symbolic to support reducing HiLo widths
- Coverage fixes
- Consider producing many individual files
- Add getlast util
- Extend offline to support floats
- Clean out redundant transforms, filters
- Fix IntToBit for cvt_int_bits
- Prune useless globals
- Generalise req patterns to capture generic case & LowestSetBit
- Improve sub_int simplification
- Rather than failing on unsupported PSTATE mods, insert assert
- Ocaml backend cleanup
- Prune unsupported impdefs, block insts with unsupported state access
- Offline lifter cleanup, push to all of aarch64
- Collect TODOs
- Cleanup build, bundle empty implementation to avoid costly builds
- Fixups for coverage
- Convert tuple return from FPToFixedJS to bitvec
- Offline transform cleanup
- Replace bool impdefs with false rather than assert
- Add missing fp op
- Fix sed usage
- Fix coverage for FPToFixedJS
- Extend ocaml backend to produce many files
- Eliminate unnecessary temps in offline transform
- match raw pretty printing of optional_else and indented_block (#51)
- dune-project: enable cram tests.
- cram: add golden tests for disassembling particular opcodes.
- coverage: use dune to run coverage testing
- ci: use dune-based coverage test
- dune: do not run tests during build
- aslt: compact indented blocks when empty.
- aslt: quote ident names
- aslt: display integers and bits as bare literals
- aslt: semicolon for stmt lists
- cram: add ldp/stp
- aslt: reduce redundant parens in expr list and slice list.
- cram: separate ops.txt file.
- aslt: fix some missing quotes and fix conflict.
- aslt: remove parens around var decl names
- aslt: touch up antlr grammar
- docs: update with new aslt and testing
- ci: runtest
- cram: output aslt instead of antlr tree
- cram: intersperse opcodes in test_cntlm.t
- cram: update output after offline partial eval.
- Ocaml version to 4.14
- Fix more references to OCaml 4.09
- Limit CSE to generating bitvec temps
- Add missing prims
- **gitattributes: ignore .t and .asl files
- support multiple :gen backends (#63)
- remove ./asli script (#65)
- gitattributes: ignore vendored aslp-cpp lib directory (#66)
- server: fix unused variable warnings (#69)
- rename redefined variables (#67)
- cram: add test case for local variable redefinition (#68)
- add linter for whitespace checking (#64)
- Compress rt branch construction
- Prune redundant context switches
- Fix coverage script
- Fix remaining vector requirements
- Add install alias to default build target
- Small improvements to RemoveUnused
- working on backwards visitor
- fix generic and restore compatibility.
- add aslBackwardsVisitor
- aslVisitor: change vstmt to return stmt list
- fix backwards visitor and rearrange code
- support -x 0 to print encoding name. (#78)
- correctly set default debug-level to no debugging output. (#87)
- support a subset of .prj syntax in the pre-built aarch64 env (#86)
- update cntlm-ops.txt with float operations (#88)
- readme: add instructions to install package with opam (#94)
- Support compilation to Javascript (#90)
- support non 32-bit length opcodes (#89)
- dis: add function to extract disasm name
- server: return 'encoding' field
- aslp-cpp: also return encoding name
- avoid regex for debug indentation (#97)
- grammar: fix TypeBoolean (#96)
- Push loops through online PE
- Add vectorization pass
- Division & power of 2
- Replace '000..0':bv with ZeroExtend(bv)
- Do division properly
- Coverage fixes for vector ops
- add flags for controlling vectoriser
- add flag handling to aslp-server
- aslp-cpp: support extra query params
- update test results for elem operations and power-of-2 widths
- flush output during :gen
- fix loop unroll bound and add sdiv
- fix off_run.sh with embedded asl files
- Re-enable push down of slicing operations
- Fixes: - Extend vectorizer to visit conditional loops - Don't rerun StatefulIntToBits for widening of an integer, it won't actually change anything - Add ite size
- Update test outputs
- aslp-cpp: fix initialisation order warning
- test_aslt: adjust sed syntax
- add Elem functions to offline_utils
- ci: add offline-coverage
- inline Elem operations when vectoriser disabled (still not working)
- only emit Elem[] when using vectoriser
- ci: fix coverage artifact
- tests: update to remove Elem[]
- Extend IntToBits narrowing to track types for variables
- dis: do not emit slices with dynamic indices
- Re-enable last minute slice removal
- Fix tests results to remove use of mul_int
- ignore generated lifter
- Revert "dis: do not emit slices with dynamic indices"
- cpp backend (#62)
- tests: add simple output tests with vectoriser
- ci: add offline c++ lifter syntax checking (#101)
- Scala backend & lifter-optimiser bdd copyprop (#102)
- ci: add scala lifter compilation (#104)
- handle mul_bits in bits_coerce_narrow
- update comment
- update testdata
- Additional symbolic rewrites, refactor for better reuse
- rebase experimental implementation WIP: symbolic opcode #1
- parse opcode segments
- special case for and of append bits
- Remove throws from generated code - Block inlining on FPRecipEstimate - Convert enums to bvs as a post-transform - Alter semantics to permit int/enum comparison, improving coverage testing results
Match if (x = constant) then r := constant else ... patterns and attempt to replace with r := f x for simple mappings between constant pairs.
Floating Point Cleanup
Update test.yml Update test.yml Update test.yml Update test.yml Update test.yml Update test.yml Update test.yml Update test.yml Update test.yml boopfdsa no opam asd add bash arguments. update workflow
touch touch remove pr trigger run on github changes Update opam.yml Update opam.yml opam exec dune
ci: use nix
Correct visit order bug in StatefulIntToBit, support register type
Some common idioms can be easily rewritten, avoiding complexity udring dis. Currently unused.
Masks are never symbolic, so they can be trivially rewritten as a masking and equiv test if needed.
May want to make this a configuration option to dis
Cuts of prefix early, even if prefix does not end with terminal
Assumes no mixed use of array indices
Capable of extracting and simplifying behaviours for most of the instruction encodings on AArch64. Offline gen is missing specs for primitives as well as the prelude required for the ocaml backend.
Some differences in exception printing, unclear
Vectorisation, loops, and division improvements
also fixup extraction due to missed case in nested slice we should now have all static-low-index extractions
This reverts commit 4f7eca7.
Offline lifter backend for C++, including IBI instantiation to emit LLVM IR * offline-cpp: create directory. * add boilerplate cpp files * working on cpp backend. to do: implement f_gen_* functions. * stashing work to add types rt_expr and rt_label. * stub all f_ functions. * implement template-based generation * update stubs with new interface * fix some bigint/bits bugs and clean up includes. * fix cmake, do not inherit. * add gitignore for cpp * fix bits/bigint oopsie * stub v_ variables * implement v_ variable prefixing (we compile now!!) * use traits class * temp * stub implementations * compiling fr now * fix typo-ed names and change to _impl.hpp * temporarily do the scoping thing :( * disable scoping hack * working on f_gen methods * starting restructure for compile speed * work on explicit instantiation * refactor to cpp_fun_sig * clean up and fix. split compilation working now! * restore aslp_lifter_impl.hpp * collate decode_tests and split llvm traits * generating basic llvm? * touch * typename * implement missing registers and intrinsics for non-float ops. * fix with new branch intrinsics. * restructure * restructuring aslp-lifter-gen now works with pkg-config maybe * meson build system * merge to aslp-lifter project, distrubute src files, remove old cmakes * compile speedups with clang+lld * ci * Update build.sh * Update test.yml * use absolute paths in ci CXX CXX_LD * use llvm-15 * Update test.yml * fix important warnings * fix ci nix overrides CXX variable when entering shell, predictably * no ci * fix uninit warnings * add minimal cmakelists for non-installed use only * update to generate in external repository * copy support files when generating cpp lifter this allows keeping versioning the lifter_interface alongside the backend code which uses it. * add cpp build files into repository * do not copy headers and fix mkdir_p * add warning to user to copy c++ build files. * update cpp readme to suit in-repository location * set default cpp gen dir to within subprojects * generate meson file * use %blob in cpp_backend * update comment in cpp_backend * add cpp build instructions to cpp readme * add gitignore to offlineasl-cpp * add check.py to perform syntax-checking of generated cpp it would be nice to run this in ci. note llvm 17 dependency * meson: restrict to llvm 17 * chdir in check.py
* ci: add offline c++ lifter syntax checking * use ubuntu 24.04 for llvm 17 * allow LLVM 16 * use llvm 17 * install ninja * ci: only run opam on opam.yml changes
tests: add simple output tests with vectoriser
* Add scala backend for BASIL * Add lifttime PC variable Optional support for offline lifter to specify the PC value at lifttime. * Remove problematic list, add missing variables * Optional pass to remove unsupported globals * Whitespace in transforms * Re-enable case simp for offline * Decoder cleanup and sanity checks * Simplify reachability based on enc * Add lifttime PC variable Optional support for offline lifter to specify the PC value at lifttime. * Remove problematic list, add missing variables * Optional pass to remove unsupported globals * Whitespace in transforms * Re-enable case simp for offline * Decoder cleanup and sanity checks * Simplify reachability based on enc * wip rt copyprop * use bdd lattice for clobbered & read * refac * untested xform to ternary * not working * refactor so analysis and transform both called into from bdd AI walk * fix anlaysis a bit and add bvadd * cleanup bvops * Eliminate comparisons during IntToBits Leverage interval information to reduce trivial comparisons during post-passes, then cleanup in RemoveUnused. * fix rebuild expr * passing cov disabled * test and fix bdd sle/slt * Merged backends (#80) * Add scala backend for BASIL * Add C++ Backend for LLVM * add aslBackwardsVisitor * aslVisitor: change vstmt to return stmt list BREAKING! This change affects the signature of the Asl_visitor.visit_stmt method. For compatibility, a visit_stmt_single method is provided with equivalent behaviour to the old visit_stmt. There is also an added helper function to convert visitActions on single statements to visitActions on a list of statements. Both of these compatibility helpers WILL THROW if used with a visitor that returns non-singleton statement lists. This gives the user the flexibility to insert new statements or delete statements entirely. On the other hand, post-functions in ChangeDoChildrenPost will need to handle lists of functions as well. This follows the original CIL visitor: https://people.eecs.berkeley.edu/~necula/cil/api/Cil.cilVisitor.html * fix backwards visitor and rearrange code it is no longer a good idea for the backwards and forwards visitors to have a subtyping relation. * support -x 0 to print encoding name. (#78) this is very useful when looking for the name of an encoding, without cluttering the output with the disassembly trace. the default debug_level has been lowered to -1 to support -x 0 as a non-default level. we cannot print by default since that would clutter stdout when used as a library. Co-authored-by: rina <[email protected]> * progress * possibly working * build standalone * print lifted semantics * readme * add mill script * add generic lifter interface * delete old utils * generate separate scala assembly file * cleanup * update tests * marshall offline lifter * fix symbolic lifter merge * update action * update cpp lifter * cpp: allow llvm 18 * cpp: clean up offlineASL-cpp folder delete old hpp files in root reset meson.build to empty --------- Co-authored-by: Nicholas Coughlin <[email protected]> Co-authored-by: rina <[email protected]>
* ci: add scala lifter compilation * use coursier/setup-action * java 17 * add note about notimplemented [no ci] * fix readme steps and remove sbt
New rewrites for: - Slice over integer addition - Slice over UInt - Trivial integer equivalence cases - Reduce (x = false) to not x Probably some room to generalise these further.
…-mul Handle `mul_bits` in `bits_coerce_narrow` transform
Additional symbolic rewrites
|
Github struggled with this. Replaced by #4. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.