d1m0
|
9e3f4e9195
|
Cleanup for PR #123 (#129)
* Fix bextend semantics; Change smtlib.py to use z3 python bindings for query building instead of raw strings
* Forgot the mypy stubs for z3
|
2017-07-31 16:02:27 -07:00 |
|
Dimo
|
a324d60ccc
|
Cleanup, typechecking and documentation nits
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
9767654dd7
|
Add semantics for several more iadd with carry; Add xform_correct() and doc cleanup
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
c3092d680f
|
Add smtlib.py
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
59e204cec2
|
Fix broken test_elaborate tests after the moving of is_concrete/cleanup_concrete_rtl
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
e346bd50c8
|
Add primitive bvult, bvzeroext; Add semantics for bextend, icmp (partial - only for <) iadd_cout
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
ec9e9bd1ca
|
cleanup_semantics() should remove repeated prim_from_bv(x)
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
93b57a5209
|
Nit: Make elaborate return a new Rtl instead of modifying the existing rtl inplace
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
80a42fdeaa
|
Move apply() -> Xform.apply(); is_concrete_rtl() -> Rtl.is_concrete(); cleanup_concrete_rtl() -> Rtl.cleanup_concrete_rtl(). Documnetation nits in semantics.elaborate
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
a92021ebce
|
With multiple semantic transforms mentioning Enumerators, it may be possible for there not to be a substitution from the concrete rtl to some of the transforms. This is not an error - just a case where a given semantic transform doesnt apply. (e.g. icmp being described by different transforms with concrete intcc condition codes)
|
2017-07-28 10:47:08 -07:00 |
|
Dimo
|
345d6754f5
|
Change TV ranking to select src vars as a representative during unification; Nit: cleanup dot() emitting code; Nit: fix small bug in verify_semantics() - make an internal copy of src rtl to avoid clobbering of typevars re-used in multiple definitions
|
2017-07-25 15:38:48 -07:00 |
|
Dimo
|
736b6a44a7
|
Fix CI: Var was only imported when mypy was present.
|
2017-07-24 14:08:44 -07:00 |
|
Dimo
|
12db123606
|
TI failure due to misplaced import
|
2017-07-24 14:08:44 -07:00 |
|
Dimo
|
9258283e14
|
Documentation nits; Sematnics syntax cleanup
|
2017-07-24 14:08:44 -07:00 |
|
Dimo
|
40c86d58b9
|
Add insturction semantics. Add semantics for vsplit,vconcat,iadd. Add initial tests
|
2017-07-24 14:08:44 -07:00 |
|