summaryrefslogtreecommitdiff
path: root/test/mono
AgeCommit message (Collapse)Author
2020-04-21Take kid synonyms into account when propagating constantsThomas Bauereiss
For example, in let datasize = e in ... the typechecker will generate a kid '_datasize if e has an existential type (with one kid), and in let 'datasize = e in ... the typechecker will bind both 'datasize and '_datasize. If we substitute one as part of constant propagation, this patch will make constant propagation also substitute the other.
2020-04-21Mono: Check for non-constant calls to make_the_valueThomas Bauereiss
... and try to resolve them using constant propagation.
2019-11-22Add tests for monomorphisation improvement in eb0e17f2Brian Campbell
2019-11-07Make the world a slightly more sane and consistent placeAlasdair Armstrong
2019-11-04Some almost-forgotten mono testsBrian Campbell
2019-08-29Clean up some mono testsBrian Campbell
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
In particular, bitvector subrange updates work with this version.
2019-06-19Monomorphisation improvements for aarch64_smallBrian Campbell
- additional rewrites (signed extend of subrange@zeros, subrange assignment, variants with casts) - drop # from new top-level type variables (e.g., n_times_8) so that the rewriter knows that they're safe to include in casts - add casts in else-branches when only one possible value for a size is left - add casts when assertions force a size to be a particular value - don't use types to detect set constraints in analysis because we won't know which part of the assertion should be replaced - also use non-top-level type variables when simplifying sizes in analysis (useful when it can from pattern matching on an ast) - cope with repeated int('n) in a pattern match (!)
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 13:55:37 +0000