Commits · fc48be5e73e1a9ef1c0ab998344cd0259c1a8edc · paradise / mirror / DIVINE · GitLab

Jan 24, 2020
- 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
- lamp: Split 'wrap' (returns a pointer) from 'lift' (returns a tainted scalar). · 45210334
  Petr Rockai authored Jan 24, 2020
  
  45210334
- lart: Put code for inheriting metadata back into the tainting pass. · 618bc23a
  Petr Rockai authored Jan 24, 2020
  
  618bc23a
- lart: Add a metadata tag for 'faultable' function calls. · 38d96d9c
  Petr Rockai authored Jan 24, 2020
  
  38d96d9c
- lart: A few minor style fixes under abstract/. · 878c10dc
  Petr Rockai authored Jan 24, 2020
  
  878c10dc
- lart: Update add_meta() calls in the DFA pass. · 9b5bf2d8
  Petr Rockai authored Jan 24, 2020
  
  9b5bf2d8
- lart: Attach LAMP operations as metadata to instructions to be abstracted. · 0739dadb
  Petr Rockai authored Jan 24, 2020
  
  0739dadb
- lart: Allow function pointers to be stashed in metadata. · e090c110
  Petr Rockai authored Jan 24, 2020
  
  e090c110
- lart: Get rid of domain indices in the Synthesize pass. · aa3f6bca
  Petr Rockai authored Jan 24, 2020
  
  aa3f6bca
- lart: Remove the InitAbstractions pass (responsible for identifying domains). · 657f1372
  Petr Rockai authored Jan 24, 2020
  
  657f1372
- bricks: Prevent constructor calls when bitcasting from non-trivial types. · 022a06e7
  Petr Rockai authored Jan 24, 2020
  
  022a06e7
- dbg: Fix a segfault in Context::is_same(), plus a style fix. · b0290bb4
  Petr Rockai authored Jan 24, 2020
  
  b0290bb4
- dbg: Use smt::extract::to_string() instead of a locally grown variant thereof. · 44e974a4
  Petr Rockai authored Jan 24, 2020
  
  44e974a4
- MC: Replace copy-pasta with smt::extract::to_string(). · f9d5ec60
  Petr Rockai authored Jan 24, 2020
  
  f9d5ec60
- smt: Add an extract::to_string() helper function. · 1b58e802
  Petr Rockai authored Jan 24, 2020
  
  1b58e802
- UI: Enable non-interactive mode if TRACE is set (instead of BRICK_TRACE). · 5d558e84
  Petr Rockai authored Jan 24, 2020
  
  5d558e84
- UI: If --symbolic is given, set the default LAMP config to 'symbolic'. · db11ba5c
  Petr Rockai authored Jan 24, 2020
  
  db11ba5c