summaryrefslogtreecommitdiff
path: root/test/mono
AgeCommit message (Collapse)Author
2019-05-06Handle type variables generated while inferring applications in monomorphisationBrian Campbell
Also handle any type variables from assignments and degrade gracefully during constant propagation when unification is not possible.
2019-04-26More constructor monomorphisation supportBrian Campbell
- handle multiple bitvector length variables - more fine-grained unnecessary cast insertion checks - add tuple matching support to constant propagation (for the test)
2019-04-25Get basic constructor monomorphisation working againBrian Campbell
- updates for type checking changes - handle a little more pattern matching in constant propagation - fix bug where false positive warnings were produced - ensure bitvectors in tuples are always monomorphised (to catch the case where the bitvectors only appear alone with a constant size)
2019-04-25Update prelude in mono testsBrian Campbell
2019-03-15Fix testsThomas Bauereiss
2019-02-08Updates for asl_parserAlasdair Armstrong
Tweak colours of monomorphistion test output
2019-02-07Add a symbol for new implicit arguments for backwards compatabilityAlasdair Armstrong
Fix monomorphisation tests
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-31Monomorphisation: improve cast insertion and nexp rewriting on variantsBrian Campbell
It now pushes casts into lets and constructor applications, and so supports the case needed for RISC-V.
2019-01-31Support case splitting on variables as well as sizeof in cast introductionBrian Campbell
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
Add an extra argument for Type_check.prove for the location of the prove call (as prove __POS__) to help debug SMT related issues
2018-12-03Fix = / == in a couple of monomorphisation testsBrian Campbell
2018-08-07Lem: print more bitvector typesBrian Campbell
Especially for return expressions, which fixes a test case
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
Fixes monomorphisation on files using mappings. Also extended constant propagation to handle pattern matches on bitvector expressions (because an earlier rewrite replaces the literals). Also moved L_undef rewriting because monomorphisation can handle them but not the replacement functions.
2018-06-18Mono test script updateBrian Campbell
(still need to sort out some string stuff, though)
2018-05-22Fix one part of cast introduction, leave another for laterBrian Campbell
2018-04-18Update mono test scriptBrian Campbell
2018-04-18Move Lem shl_int, shr_int implementations from aarch64_extras to sail libBrian Campbell
(note that they're already declared in lib/arith.sail)
2018-04-17Enable mono builtins test, tweak test outputBrian Campbell
2018-04-11Fix test preludeBrian Campbell
2018-04-06Test now passesBrian Campbell
2018-04-04Instantiate type properly when introducing mono castsBrian Campbell
(also reorder the phases a little)
2018-04-04Add bitvector casts to funcl bodies when necessaryBrian Campbell
2018-03-14Update mono testsBrian Campbell
2018-03-14Remove unnecessary size_itself_int uses in guards (for Lem)Brian Campbell
Doesn't remove them from function bodies because that can produce more work for the sizeof rewriting.
2018-03-13Add test for mutual recursion and monomorphisationBrian Campbell
2018-03-13Support a few more set constraints in monoBrian Campbell
2018-03-13Merge funcls for Lem output, making it suitable for testing with OCamlBrian Campbell
2018-03-13A couple of mono test tweaksBrian Campbell
2018-03-09Sort mono test cases, add missing filesBrian Campbell
2018-02-23Make mono test harness nicerBrian Campbell
2018-02-23Change monomorphisation tests to proper outputBrian Campbell
2018-02-23Update more monomorphisation testsBrian Campbell
2018-02-22Curtail at more false assertionsBrian Campbell
(plus some adjustments for the test case)
2018-02-22Start resurrecting monomorphisation testsBrian Campbell
2018-02-08Add (most of) the bitvector cast insertion transformationBrian Campbell
to help Lem go from a general type `bits('n)` to a specific type `bits(16)` at a case split, and the other way around for a returned value. Doesn't handle function clause patterns yet
2018-01-31Find buried set constraints in assertsBrian Campbell
2018-01-25Use set asserts as case splits in monomorphisationBrian Campbell
2018-01-15Support non-trivial literal patternsBrian Campbell
Previously we only did top-level literal pattern to guard conversion, this does it throughout any pattern
2018-01-10Fix control dependencies in monomorphisation analysisBrian Campbell
2017-12-07Support monomorphisation with set constrained integersBrian Campbell
Also, to support this, constant propagation for integer multiply, fix substitution of concrete values for nvars, size parameters in single argument functions, fix kind for itself, add eq_atom to prelude
2017-11-14During monomorphisation always refine constructors,Brian Campbell
not just when there's been a case split
2017-09-28Refine constructors during monomorphisationBrian Campbell
2017-09-14Better failure reporting on mono testsBrian Campbell
2017-08-28Improve test output for monomorphisationBrian Campbell
2017-08-28Update test script for gen_lib changesBrian Campbell
2017-08-23Update monomorphisation test scriptBrian Campbell
2017-08-22Adapt first part of union monomorphisation to existential typesBrian Campbell
2017-08-18Bit more monomorphisation testingBrian Campbell
2017-08-16Very basic start to monomorphisation testingBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:30:59 +0000