Commits · b843b3a27ec8522abead64c8758652d961217555 · paradise / mirror / DIVINE · GitLab

Jan 24, 2020
- 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
- UI: Parse --lamp-config and pass it onto mc::Bitcode. · a6dcb034
  Petr Rockai authored Jan 24, 2020
  
  a6dcb034
- MC: Add support for a --lamp-config option to Bitcode. · dbc67e05
  Petr Rockai authored Jan 24, 2020
  
  dbc67e05
- RT: Add support for linking in a specified LAMP module. · ae1e5221
  Petr Rockai authored Jan 24, 2020
  
  ae1e5221
- smt: Raise an error if we try to decide feasibility without a solver. · 861151e8
  Petr Rockai authored Jan 24, 2020
  
  861151e8
- MC: Error out if we encounter marked pointers during explicit state comparison. · afea4969
  Petr Rockai authored Jan 24, 2020
  
  afea4969
- bricks: Remove the (now obsolete) brick-smt module. · 73e448b8
  Petr Rockai authored Jan 24, 2020
  
  73e448b8
- bricks: A few minor tweaks in brick-smtlib. · 6cdbbd45
  Petr Rockai authored Jan 24, 2020
  
  6cdbbd45
- bricks: Improve formatting (printing) of smt_atom_t values. · de6bd086
  Petr Rockai authored Jan 24, 2020
  
  de6bd086
- bricks: Add a formatting operator for smt_op. · c73562b5
  Petr Rockai authored Jan 24, 2020
  
  c73562b5
- bricks: Add a bw() [bitwidth] method to smt_atom_t. · 2f4b28a4
  Petr Rockai authored Jan 24, 2020
  
  2f4b28a4
- bricks: Add value() and bounds() to smt_atom_t (for use with relevant ops). · 26fdfeb1
  Petr Rockai authored Jan 24, 2020
  
  26fdfeb1