Commits · c240ce49e96d84ccf11d58a93d59568f98207619 · paradise / mirror / DIVINE · GitLab

Jan 24, 2020
- lart: Construct a very simple load lifter around __lamp_load(). · c240ce49
  Petr Rockai authored Jan 24, 2020
  
  c240ce49
- lart: Re-use the generic binary lifter for stores as well. · 5897fd31
  Petr Rockai authored Jan 24, 2020
  
  5897fd31
- lart: Build the GEP lifter out of the generic binary template. · 98921e61
  Petr Rockai authored Jan 24, 2020
  
  98921e61
- lart: Rename Lifter::get_function_from_domain() to get_lamp_op(). · 28bc09cd
  Petr Rockai authored Jan 24, 2020
  
  28bc09cd
- lart: Use operation::impl metadata in Lifter::get_function_from_domain(). · 44b7d04b
  Petr Rockai authored Jan 24, 2020
  
  44b7d04b
- lart: Update a few synthetic calls to use the new __lamp_* functions. · 1484b7bf
  Petr Rockai authored Jan 24, 2020
  
  1484b7bf
- lart: Rename call_lifter() to call_lamp_op() to improve readability. · ce6eb03c
  Petr Rockai authored Jan 24, 2020
  
  ce6eb03c
- lamp: Add wrappers for basic operations on abstract arrays. · b339003e
  Petr Rockai authored Jan 24, 2020
  
  b339003e
- libc: Add a __flatten macro to sys/cdefs.h. · d65072cd
  Petr Rockai authored Jan 24, 2020
  
  d65072cd
- website: Make test timeouts stand out more on the status page. · af394ce8
  Petr Rockai authored Jan 24, 2020
  
  af394ce8
- lart: Patch up the 'abstrub' pass to work with LAMP. · 7ff8612e
  Petr Rockai authored Jan 24, 2020
  
  7ff8612e
- VM: Make the memory leak fault string a bit less terrible. · 1434b4b7
  Petr Rockai authored Jan 24, 2020
  
  1434b4b7
- lava: Revert to using an ArrayMap for holding fragments of the path condition. · f5d7e02a
  Petr Rockai authored Jan 24, 2020
  
  f5d7e02a
- rst: Take arguments in term::assume() as const references. · a927e974
  Petr Rockai authored Jan 24, 2020
  
  a927e974
- rst: Fix incorrect uses of bitcast in support code for the term domain. · a8580f75
  Petr Rockai authored Jan 24, 2020
  
  a8580f75
- lava: Fix term::any() for one-byte variables (i1 and i8). · 37051525
  Petr Rockai authored Jan 24, 2020
  
  37051525
- lava: Fix (static) bitwidth computation for boolean values. · fc48be5e
  Petr Rockai authored Jan 24, 2020
  
  fc48be5e
- lava: Drop a couple more redundant 'noexcept' specifiers from 'constant'. · 81c60983
  Petr Rockai authored Jan 24, 2020
  
  81c60983
- lava: Remove disabled legacy code from the constant domain. · c777cd01
  Petr Rockai authored Jan 24, 2020
  
  c777cd01
- lava: Implement resizing conversions (sext, zext, trunc) for 'constant'. · 82c28290
  Petr Rockai authored Jan 24, 2020
  
  82c28290
- lava: Add support for more integer types to 'constant'. · 4766cd98
  Petr Rockai authored Jan 24, 2020
  
  4766cd98
- lava: Cut down on constructors for abstract values. · fee046d9
  Petr Rockai authored Jan 24, 2020
  
  fee046d9
- lava: Get rid of noexcept qualifiers on constant::op_*. · 995d0c56
  Petr Rockai authored Jan 24, 2020
  
  995d0c56
- lava: Take arguments in term::op_* via const references. · f893e914
  Petr Rockai authored Jan 24, 2020
  
  f893e914
- smt: Port the Z3 solver glue to brick-nusmt. · 81495b01
  Petr Rockai authored Jan 24, 2020
  
  81495b01
- smt: Port the SMTLib2 builder to new APIs. · 9006bfc1
  Petr Rockai authored Jan 24, 2020
  
  9006bfc1
- smt: Port the STP builder to new APIs. · a6bab08a
  Petr Rockai authored Jan 24, 2020
  
  a6bab08a
- smt: Update the mk_un and mk_bin helper functions. · b843b3a2
  Petr Rockai authored Jan 24, 2020
  
  b843b3a2
- smt: Update the SMTLib solver to use new brick-smtlib class names. · 2f2d005e
  Petr Rockai authored Jan 24, 2020
  
  2f2d005e
- smt: Update the solver interface to use brick-nusmt opcodes. · 7d5e3191
  Petr Rockai authored Jan 24, 2020
  
  7d5e3191
- smt: Add a missing #include to solver.hpp. · 6648aced
  Petr Rockai authored Jan 24, 2020
  
  6648aced
- smt: Remove an unused function from solver.cpp. · d99870c3
  Petr Rockai authored Jan 24, 2020
  
  d99870c3
- smt: Rewrite the evaluator on top of brick-nusmt. · 6aea4876
  Petr Rockai authored Jan 24, 2020
  
  6aea4876
- smt: Update extract.hpp to use brq::smt_expr instead of the old RPN interface. · b7033700
  Petr Rockai authored Jan 24, 2020
  
  b7033700
- test: Update 'aggregate unit' testcases. · 714dc34c
  Petr Rockai authored Jan 24, 2020
  
  714dc34c
- lamp: Fix the implementation of __lamp_ne(). · 56750041
  Petr Rockai authored Jan 24, 2020
  
  56750041
- lamp: Add 'assume' (constraints) and 'decide' (conditional branching). · fe49e63c
  Petr Rockai authored Jan 24, 2020
  
  fe49e63c
- lamp: Add __lamp_freeze() and __lamp_melt() to wrapper.hpp. · 32d39a0e
  Petr Rockai authored Jan 24, 2020
  
  32d39a0e
- lamp: Add __lamp_any_* wrappers (for creating undetermined values). · 0cbb2260
  Petr Rockai authored Jan 24, 2020
  
  0cbb2260
- lamp: Add a header that describes the C interface (as sys/lamp.h). · 700f0807
  Petr Rockai authored Jan 24, 2020
  
  700f0807