Goose  Timeline

• refactored the ref syntax again: "ref" is now an infix operator that takes an "AccessLevel" compile time value (mut/const/temp) on the lhs, or a TVar to capture/constrain it
• used the above feature to fix the constref verification _ConvertArg overload which was silently dereferencing the arg, causing it to get converted to a temp ref in all cases

• References: ref now creates a template type accepting any kind of reference, and mut/const/temp are prefix operators turning that into a ref (or template ref) type of the corresponding kind (this also changes the syntax from ref mut XXX to mut ref XXX which is more natural)
• Fixed the bizarely broken implicit referencing typechecking rule that performed a superfluous intermediate TypeCheck that crashed on non mutable template reference types
• Fixed builtin function wrapper that omitted a cast of the return value to the specified type, which allowed builtin functions to silently return values of a different type than advertised, resulting in fun type checking errors
• Fixed a bunch of fucked up return types that worked by chance (because of the above) in several g0 api functions
• Implemented non mutable reference passing verification + related tests (it doesn't work yet but too many fixes need to be committed first)

• Reverted most of the horribly complicated changes done since [b3ff9af3c2fe4925], other than the ability to hash all terms, values, instructions and predicates
• Solved the problem for which tests were added in [b3ff9af3c2fe4925] in a much simpler way

• Fixed type predicate hashing
• Template: create a monomorphization specific identity for verification (as opposed to the instance specific identity in which we ignore predicate hashes)

• Fixed a couple of verification bugs and added related tests
• Added some tests for currently broken verification scenarios involving template functions

• Fixed assignment of tuples whose content is not known at compile time
• templates: fixed forwarding TVars not retrieving their bound value
• g0 api: fixed type predicates retrieval
• Prelude: implemented a first rough version of predicate type checking when passing mutable references to functions

• improved diagnostics for ambiguous typechecking rules
• fixed quote type checking rules
• fixed linux target compilation

• fix stringid static members
• fix build and crashes on mac

• Fixed a handful of parsing issues related to templates
• Added missing export of "ref" to g1

• Fixed TypeType's representation. Declaring a type, non-template parameter (for compile time functions) now works
• Removed the trie comparison algorithm from eir that was never used
• Misc code cleanup

• Refactored LocationId into a separate class and actually use it everywhere instead of uint32_t, this makes it easier to make generic wrappers for APIs
• g0 api: more work on the CIR api

• extended the generic TypeWrapper to handle pointers to types that aren't part of the Term variant
• more work on the CIR api

• VecOfLength() will now match vectors of compatible length, taking repetition terms into account
• Vector unification and typechecking rules now handle vectors of variable lengths

• Implemented a generic wrapper for the simple native types that can be embedded in Terms
• Added more specific overloads for the assignment operator that should work only on builtin types, so that library and user defined types will be able to choose whether they're copyable
• The EIR representation for all builtin runtime types are now prefixed with "rt_type" to more easily write generic matching rules against them
• EIR: Fixed long standing bugs in Enumerate and Decompose that surfaced because of the above
• Miscellaneous code cleaning

• Fixed TermRef
• Began implementing the api to manipulate the EIR

• Started work on extensibility api
• some code cleanup

• Fixed execution of void intrinsic function causing a bogus error message
• Fixed the intrinsic operator

• template functions can now be intrinsic
• implemented the "intrinsic" operator to create intrinsic functions
• some code cleanup

• Added extension points to transform parameter types and function arguments
• Fixed the incorrect type predicate type checking rule which should just preserve the argument's predicates as is
• Fixed verification of return intructions that were checking the returned value's predicates, instead of the return type predicates (which happened to work anyway until the above fix)

• Type predicates' identity and placeholder are now created immediately, rather than when parsing their content
• Added missing type predicates lazy parsing during typechecking
• Fixed a type checking rule falling back to unification, which is no longer needed

• Instead of falling back to unification as the default type checking rule, implemented default type checking rules similar to the default unification ones
• Fixed a nasty generator bug
• Fixed reference type parsing not generating a location
• Fixed where operator not generating a location that spanned both the types and the predicates
• Various fixes to accomodate random api changes in the latest llvm
• Updates fmt and catch2 versions

• Removed the Conversion step, it could all be done using PostProcessing callback, there were just TypeChecking rules missing to unwrap the callbacks...
• Fixed some ill defined reference type checking rules
• Runtime integers no longer have a default initializer of 0. This isn't that useful considering that 0 may not be valid depending on the refinement conditions applied to the type

• Added a Conversion step after typechecking, to take care of conversions that aren't practical to do during typechecking itself.
• Added back a proper ct_int to rt_int conversion step that diagnoses out of range integer constants

• Refactored and simplified the way integer and string constants are handled: we no longer try to resolve them during typechecking, this breaks when parametric types are involved and also it makes no sense, typechecking is about types, not values
• Fixed multiple places where locationIds weren't propagated
• Verifier: variable assignments now verify the destination variable type's refinement conditions
• Fixed a test where the above change detected a bug, kept the bugged version as a new verification failure test

Then fixed a MILLION horrible problems caused by all that. Now almost everything works again. *sobs* check-in: 9b058524b4 user: achavasse tags: trunk

• Verifier: fixed havocing of individual members of aggregate types not working.
• Added verification loop tests (both passing and failing) that modify a tuple inside of the loop.

• Fixed reference typechecking issues.
• Fixed tuple initialization.
• Added verification tests involving values stored in tuples.

• Added overloads to the comma operator to be able to construct tuples of references.
• Fixed reference typechecking rules so that overloads taking values directly have priority over overloads taking references.
• Fixed a template function expression parsing bug.

• Removed the poorly thought out "domain" system that was intended to allow for different implementations of functions for runtime and for compilation time, which was adding an absurd amount of crap everywhere and should be unnecessary with the current planned approach for implementing data structures.
• The using statement doesn't do lazy parsing anymore. Lazy parsing is better left to specific constructs that require them (such as function bodies and later on class/structs). This removes the only case of significant newline character in the language.

• Got rid of the gross system of performing unifications twice in all cases. It's only really needed when invoking template functions.
• Since the above had the unexpected side effect of fixing the tuple Initialize() overloads not being called, fixed those (which were actually broken).

• Implemented Initialize overloads for tuples.
• Lots of cleanup.

• Verifier: a bunch of refactoring to better keep track of the types of the z3 expressions stored in variables.
• Verifier: handle "LoadFromAddress" for addresses that point to tuple members.

• Added a "LowerConstantForRuntime" extension point, similar to LowerTypeForRunTime.
• Added a way to represent Record constants.
• Implemented LowerConstantForRunTime for tuples, which lowers them into a constant record.
• Implemented codegen for constant records.
• Implemented codegen for storing an aggregate constant.
• Implemented a way (not exposed in the syntax for now) to create vararg function types, to be able to call vararg external functions such as printf.
• Enabled the tuple runtime/compilation combined test which is now working.
• Various bug fixes.

• Fixed the hole matching score which prevented some unification rules to be selected.
• Implemented LowerTypeForRuntime for tuples.
• Implemented an unification rule for constant tuples.
• Added some debugging helpers.

• Renamed the LowerType extension point to LowerTypeForRuntime as we'll need a similar "LowerTypeForVerification" later on.
• The function type case of LowerTypeForRuntime is no longer hardcoded in the c++ utility function of the same name but implemented as an overload of the extension point.

• Clean up the "default return value from top level file functions" stuff.
• Standardize to a default return value of 0 for the top level file both in execution mode and in compilation mode.
• Implemented a combined execution/compilation test for tuples in preparation for implementing tuple compilation. (not enabled yet)

• When doing variable declaration local type inference, look for an initialization function that takes a mutable reference on the lhs, instead of a local variable.
• As a result of the above, got rid of Initialize() overloads for local variables.
• The assignment operator now takes a mutable reference on the lhs, instead of directly working on a local variable.

• Implemented load, store and pointers in execute and codegen.
• Implemented load and pointers in verify.
• When unifying a local variable against a parameter, generate a reference.

• Wrap function parameters into local variables, which will make it easier later on to distinguish temporaries from stack values when implementing references.
• Register parameters for destruction, which was missing.
• Added an invocation rule for local variables, so that they can be invoked if they contain an invokable object.

• Verification time assertion failure errors for builtin division, module and shift operators are anchored to a valid source code location.
• Added custom error messages for the above.
• Added tests for the above.

• The builtin integer division and modulo operators now require a compile-time proof that the divider is not zero.
• The builtin integer left shit and right shift operators now require a compile-time proof that the rhs value is less than the bitsize of lhs.

• Assert type predicates after a variable assignment
• Check type predicates when checking a compile-time function call

• Moved the cfg and lifetime management stuff into a CodeBuilder object owned by sema::Context. This is in preparation to allow alternative implementations of the builder, for instance to build classes.
• Pass the context to intrinsic functions, which removes their dependency to the parser the need for the ugly "GetCurrentParser" static function.

• Split extpoints.cpp into several files.
• Fixed a tuple related bug that caused compilation failures when adding parentheses around expressions in some cases.

• Fixed crash when an undefined symbol is encountered in a verification condition.
• Fixed crash when a non-boolean expression is encountered in a verification condition.

• verifier: check compilation-time function calls.
• verifier: improved error messages wording.

• Compile-time execution: don't attempt to perform a compile time evaluation of every invocation. Instead, wait until a type is being used by a decl to try and evaluate it.
• Diagnostics: simplify accordingly (no need for the mode that silences all errors during attempted comptime evaluation)
• Added some verification conditions to the mandelbrot sample, and created a broken variant as a verification diagnostics test.

• Shift operators: the right hand side must be an unsigned int.
• Verifier: added tests to check that bitwise operations are properly translated to z3.

• Fixed incorrect cfg walking order, which sometimes didn't properly process all the predecessors of a basic block first.
• Preserve the unique id counter of the remapper when saving/restoring its state. Fixes breakage with nested loops.
• Added tests for the logic or/and operators (which are really tests of the phi operator and of basic block processing order).

• Unsigned ints are represented using z3 bitvecs.
• The original type is carried around along with z3 exprs to be able to convert ints to bitvecs of the right size.
• Insert int2bv conversions as necessary when encountering integer/bitvec mixed operations.
• The logic and and logic or instructions are implemented on integers, which are converted to bitvecs.

• cfg: compute a list of every variable modified by each loop.
• verifier: added a function to "havoc" a variable at the start of a given basic block.

• while: remove code attempting to detect infinite loops, this will be best left to the verifier.
• verifier: loop unrolling now works.

• Removed some hackish code to work around loops (not needed anymore now that loops edges are properly identified)
• Added a placeholder class to track the state of loop unrolling and started plugging it into the existing code.

• Verifier: handle calls (assert the callee's preconditions and assume its postconditions)
• Verifier: handle return value placeholder in the post conditions.
• Verifier: fixes.
• Verifier: context descriptions and locations can be attached to assertions.
• Lexer: fix incorrect location length on integer literals.
• Added some tests for successful and failed verification of functions pre-conditions and post-conditions.

• Fixed incorrect logic when generating z3 expressions to track the value of variables accross basic blocks.
• Implemented basic error reporting for verification failure that highlights all the failed assertions.
• Added a test program that demonstrates a simple case of failed static verification.