Commits · e7a720b41ced485f01c7517826502e78262369ec · paradise / mirror / DIVINE · GitLab

Jan 26, 2020
- bricks: Rename brick-nusmt back to brick-smt now that it works. · e7a720b4
  Petr Rockai authored Jan 26, 2020
  
  e7a720b4
- test: Update the list of bricks unit tests. · fd7e394a
  Petr Rockai authored Jan 26, 2020
  
  fd7e394a
- test: Fix the brick-update script. · 1b9d0155
  Petr Rockai authored Jan 26, 2020
  
  1b9d0155
- test: Fix a copy-pasta buffer overflow in mstring-null-termination. · 33f88097
  Petr Rockai authored Jan 26, 2020
  
  33f88097
- lamp: Cut down on the runtime overhead of __lamp_* wrappers. · ac63fd3e
  Petr Rockai authored Jan 26, 2020
  
  ac63fd3e
- lamp: Sprinkle __inline around semilattice to flatten the abstraction tower. · 6450bf1c
  Petr Rockai authored Jan 26, 2020
  
  6450bf1c
- smt: Fix argument order in Z3::constant(). · cf474e3d
  Petr Rockai authored Jan 26, 2020
  
  cf474e3d
- lamp: Add semilattice::op_zfit(). · 8e37d3e5
  Petr Rockai authored Jan 26, 2020
  
  8e37d3e5
- lava: Add a fake 'zfit' operation to mstring. · 1f641b5c
  Petr Rockai authored Jan 26, 2020
  
  1f641b5c
- lava: Fix memcpy() support in mstring. · 566958cd
  Petr Rockai authored Jan 26, 2020
  
  566958cd
- lart: Fix the definition of type_onion::maybe_aggregate(). · 8b43cf0a
  Petr Rockai authored Jan 26, 2020
  
  8b43cf0a
- test: Run basic mstring tests in both symbolic- and constant-based configs. · ac125adc
  Petr Rockai authored Jan 26, 2020
  
  ac125adc
- test: Cut the mstring null termination test in half. · 46ae169e
  Petr Rockai authored Jan 26, 2020
  
  46ae169e
- lava: Add domain_mixin::fn_memcpy(). · d3ff22d2
  Petr Rockai authored Jan 26, 2020
  
  d3ff22d2
- lamp: Add support for fn_memcpy(). · c2f1cf88
  Petr Rockai authored Jan 26, 2020
  
  c2f1cf88
- lart: Re-enable memcpy lowering in DFA since now it mysteriously works. · 4e8386f3
  Petr Rockai authored Jan 26, 2020
  
  4e8386f3
- dios: Call destructors when moving data due to Array::insert(). · 572d17fb
  Petr Rockai authored Jan 26, 2020
  
  572d17fb
- lava: Rebuild mstring on top of new base classes and interfaces. · df9e991e
  Petr Rockai authored Jan 26, 2020
  
  df9e991e
- lava: Add missing bitwidth coercions to mstring::fn_strcmp(). · b3c4f755
  Petr Rockai authored Jan 26, 2020
  
  b3c4f755
- lava: Remove redundant uses of static_cast< bool >() in mstring. · a55fdf39
  Petr Rockai authored Jan 26, 2020
  
  a55fdf39
- lava: Cut down on copying 'constant' values. · 3d4f2174
  Petr Rockai authored Jan 26, 2020
  
  3d4f2174
- lava: Assert that all arguments of 'constant' ops have the same bitwidth. · 951a35fd
  Petr Rockai authored Jan 26, 2020
  
  951a35fd
- lamp: Advise caution when dealing with the coercion in semilattice::cast_one(). · f8f32c05
  Petr Rockai authored Jan 26, 2020
  
  f8f32c05
- lava: Add a (very unsafe) pointer access hatch to tagged_array. · ed79e020
  Petr Rockai authored Jan 26, 2020
  
  ed79e020
- lava: Add placeholders for string.h functions to domain_mixin. · a01aabf3
  Petr Rockai authored Jan 26, 2020
  
  a01aabf3
- lava: Add domain_mixin::op_{not,neg} placeholders. · 8be5ca8c
  Petr Rockai authored Jan 26, 2020
  
  8be5ca8c
- lava: By default, make each domain its own scalar and index domain. · ed9fc59a
  Petr Rockai authored Jan 26, 2020
  
  ed9fc59a
- lava: Fix domain_mixin::op_{gep,store}. · f4225a27
  Petr Rockai authored Jan 26, 2020
  
  f4225a27
- bricks: Replace forwarding with 'using' of base ctors in smt_expr. · a85174bb
  Petr Rockai authored Jan 26, 2020
  
  a85174bb
- lava: Properly call constructors & destructors in tagged_storage. · d74ef1c8
  Petr Rockai authored Jan 26, 2020
  
  d74ef1c8
- lava: Add a rudimentary term::op_gep() implementation. · 9e507657
  Petr Rockai authored Jan 26, 2020
  
  9e507657
- lava: Add logical operators (and, or, not) to 'scalar'. · 0d8f0963
  Petr Rockai authored Jan 26, 2020
  
  0d8f0963
- lava: Fix two minor issues in 'scalar'. · 924d884a
  Petr Rockai authored Jan 26, 2020
  
  924d884a
- lava: Take arguments of 'scalar' operators as const references. · a01a1b88
  Petr Rockai authored Jan 26, 2020
  
  a01a1b88
- lava: Drop redundant 'noexcept' qualifiers on 'scalar' operators. · a61debe2
  Petr Rockai authored Jan 26, 2020
  
  a61debe2
- lava: Add op_not() and op_neg() to 'term' and 'constant'. · 9223becc
  Petr Rockai authored Jan 26, 2020
  
  9223becc
- lava: Tighten the constructors of term. · 5fdeaa49
  Petr Rockai authored Jan 26, 2020
  
  5fdeaa49
- lava: Add missing unit::op_zfit(). · c90c5a28
  Petr Rockai authored Jan 26, 2020
  
  c90c5a28
- lava: Accept arbitrary scalars & indices in unit::op_{gep,store}. · fef038bd
  Petr Rockai authored Jan 26, 2020
  
  fef038bd
- lamp: Add mstring-based configs -- constant (for testing) and symbolic. · afab0f78
  Petr Rockai authored Jan 26, 2020
  
  afab0f78