Commits · 1434b4b774f6e4ddad5afaa534cbf3cf7f1b966f · paradise / mirror / DIVINE · GitLab

Jan 24, 2020
- 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
- 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