Goose  Timeline

• 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.

• Renamed the "assert" test helper function to "check".
• Implemented a builtin "assert" intrinsic that emits an Assert instruction for the verifier.
• Implemented a couple of tests to verify the generated z3 expressions for a couple of simple functions.
• Fixed a few issues when building the z3 expressions.

• Fixed some issues with implicit termination of void functions.
• llr: give an index to each basic block, and keep track of back links towards previous blocks.