Goose: Timeline

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

156 check-ins using file bs/ir/vecgenerator.h version b68308094b

2020-12-26
14:59		Build fix check-in: c8058eaaf9 user: achavasse tags: trunk
2020-12-18
01:29		References refactor: references are now values all the way to the llr, where a new "CalcAddress" instruction represents a conversion from a logical address (location + path) into an actual runtime or compilation time address. This is in preparation to allow references to be stored in variables or passed as parameters. (It just took 4.5 months to finish this... Refactoring just sucks) check-in: 8ddd71f9b2 user: achavasse tags: trunk
2020-08-02
19:26		Execute: use a proper call stack so that we'll be able later on to reference values living on the caller's stack to be able to pass references around at compilation time. check-in: 151e3b4d8c user: achavasse tags: trunk
2020-07-07
21:08		When creating a reference to a local variable, if it contains a reference, just unwrap it. check-in: 421381dc15 user: achavasse tags: trunk
2020-07-06
19:49		Fixes for the current git version of clang/llvm. check-in: 834d8f14b9 user: achavasse tags: trunk
2020-07-05
20:15		Implemented reference parsing. check-in: 086a58a7a3 user: achavasse tags: trunk
2020-07-04
13:08		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. check-in: e3b9bd4c1b user: achavasse tags: trunk
12:24		Verification: fixed a bug with address havocing. check-in: 879d75711b user: achavasse tags: trunk
2020-07-03
23:09		Removed a couple of obsolete comments. check-in: 4dd8529aac user: achavasse tags: trunk
23:03		Fixed reference typechecking issues. Fixed tuple initialization. Added verification tests involving values stored in tuples. check-in: 4be05b9f94 user: achavasse tags: trunk
2020-07-02
19:31		Added tests for tuples of references. check-in: 05ec684dbf user: achavasse tags: trunk
00:47		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. check-in: 04aea08600 user: achavasse tags: trunk
2020-06-27
22:05		Clearly separate the type checking rules and the unification rules, instead of lumping them all together in a single set of patterns which is increasingly confusing. check-in: b64ea47f6b user: achavasse tags: trunk
2020-06-26
23:34		Cleanup: 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. check-in: 568c366a36 user: achavasse tags: trunk
2020-06-20
19:59		Verifier: some fixes to correctly handle tuples. Still not quite working yet. check-in: 060e84f233 user: achavasse tags: trunk
16:07		Fixed one of the tuple unification rule. check-in: 48bb81ebdd user: achavasse tags: trunk
14:32		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). check-in: c3f897359f user: achavasse tags: trunk
2020-06-15
22:09		Refactored the integer/ct_int unification to defer the size/sign check to a postprocessing callback. check-in: ac4e681af3 user: achavasse tags: trunk
19:45		Call "Postprocess" on unification solutions during the best solution lookup, so that custom postprocessing callbacks can trigger the rejection of a solution. check-in: daee557086 user: achavasse tags: trunk
19:16		Moved some common code into a helper function to facilitate some future refactoring. check-in: df0ad9a7f1 user: achavasse tags: trunk
2020-06-13
22:59		Implemented Initialize overloads for tuples. Lots of cleanup. check-in: 947b9d7cfc user: achavasse tags: trunk
13:34		Implemented new rules for implicit dereferencing and implicit referencing. check-in: 4d5cc07d86 user: achavasse tags: trunk
13:15		Rewrote the reference unification rules. check-in: ba97c17dee user: achavasse tags: trunk
13:05		Fixed eager evaluation not failing gracefully in some cases. check-in: c70d722331 user: achavasse tags: trunk
12:51		Modify the reference IR representation so that we can have holes for the behavior. check-in: 385846b609 user: achavasse tags: trunk
2020-06-05
18:57		Verifier: loops: instead of tracking and havocing modified variables during loops, track modified addresses, so that modifying only some fields of a tuple will not result in forgetting everything about the other fields. check-in: 54ef60956e user: achavasse tags: trunk
00:42		Cleanup. check-in: ea28d09f80 user: achavasse tags: trunk
00:35		Verifier: handle "StoreToAddress" for addresses that point to tuple members. check-in: 077c944c02 user: achavasse tags: trunk
2020-06-03
23:08		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. check-in: b00c682e34 user: achavasse tags: trunk
2020-06-01
18:39		Verifier: go through the LowerConstantForVerification extension point when building a constant expression. check-in: 98739f02b6 user: achavasse tags: trunk
01:21		Cleanup. check-in: c793734a0a user: achavasse tags: trunk
01:06		Verifier: refactored type handling and extended it to handle tuple types. check-in: 6f98718d3b user: achavasse tags: trunk
2020-05-30
14:25		Enable's z3 new arith solver as the old one takes a very long time in one of the tests with the latest version of z3. check-in: 4b56796791 user: achavasse tags: trunk
2020-05-25
22:08		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. check-in: bb17e9f3dd user: achavasse tags: trunk
2020-05-23
12:58		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. check-in: c39a302502 user: achavasse tags: trunk
2020-05-21
17:26		Created a new term type to represent holes in IR expressions. The old system of representing holes using a vector of two values led to ambiguousness when creating some rule patterns: a tuple whose both type vector and payload vector were holes would be indistinguishable from a tuple containing two elements. check-in: 51c6751b6d user: achavasse tags: trunk
2020-05-19
17:07		Added an unification rule for computed tuples which creates constant references for each members and unifies them. check-in: 2ecfa85c23 user: achavasse tags: trunk
15:03		The TemporaryAddress address calculation mode now carries around the initializer value, in case the temporary doesn't already exist. This allows a reference to a temporary to be completely self contained in its value, rather than requiring a separate setup instruction to be emited in the cfg. check-in: 934090c5a8 user: achavasse tags: trunk
2020-05-18
12:39		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. check-in: 8818ea1872 user: achavasse tags: trunk
2020-05-17
17:30		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) check-in: 397f594186 user: achavasse tags: trunk
2020-05-16
19:32		Repo: fix syntax highlighting with the latest trunk verison of fossil. check-in: 807a4f208b user: achavasse tags: trunk
19:21		Minor cleanups. check-in: 6099081bdd user: achavasse tags: trunk
18:39		Now that we can assign mutable references, it is possible to assign to a tuple member. Added a test for that. check-in: 27a74436f3 user: achavasse tags: trunk
18:32		The builtin assignment operator overloads now return the reference to support chained assignments. check-in: ba2a02025d user: achavasse tags: trunk
2020-05-14
22:24		The compound assignment operators now take a mutable reference as the lhs. check-in: e4cd7e104e user: achavasse tags: trunk
2020-05-13
18:15		References: 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. check-in: ebdba2e941 user: achavasse tags: trunk
2020-05-04
18:43		Refactored the Initialize() extension point to take a mutable reference instead of directly taking a locvar. check-in: 10df99e08a user: achavasse tags: trunk
2020-05-03
15:32		Simplified the llr address representation. check-in: 0b4eb97a44 user: achavasse tags: trunk
2020-04-22
23:27		Removed llr::SetVar, now using the more generic llr::Store instead. check-in: 036092faf1 user: achavasse tags: trunk
2020-04-15
06:36		Removed llr::GetVar, now using the more generic llr::Load instead. check-in: 20c242dc4f user: achavasse tags: trunk
2020-04-11
23:33		Updated to the latest git version of llvm. check-in: d38aab5fc2 user: achavasse tags: trunk
21:01		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. check-in: e814ad7e23 user: achavasse tags: trunk
2020-03-11
22:11		Reference: implemented a pattern provider for mutable references. check-in: 58491e544e user: achavasse tags: trunk
2020-03-07
16:36		More work and fixes on references. Reading a tuple member using the . operator (which returns a constant reference) is now working. check-in: 1c33db7499 user: achavasse tags: trunk
2020-02-29
15:07		Implemented unification for references. check-in: 4940c5c904 user: achavasse tags: trunk
2020-02-27
22:15		Implemented the dot operator for tuples. check-in: 2f953408d9 user: achavasse tags: trunk
2020-02-26
22:48		builtins: added the reference type. check-in: b4dfb8c928 user: achavasse tags: trunk
2020-02-23
23:57		llr: added the load and store instructions. check-in: f34a90f312 user: achavasse tags: trunk
2020-02-22
21:22		llr: added the GEP instruction. check-in: 1f1bc22ffc user: achavasse tags: trunk
2020-02-20
22:44		Minor code formatting cleanup. check-in: 0af3d1c728 user: achavasse tags: trunk
22:42		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. check-in: 652107629a user: achavasse tags: trunk
2020-02-17
23:15		Register temporary values returned from function calls for destruction, so that DestroyValue() is invoked on them. check-in: a0ee0dfc2e user: achavasse tags: trunk
2020-02-15
15:13		Started to implement a virtual memory sub system for compilation time execution. check-in: f18062b8da user: achavasse tags: trunk
2020-02-09
19:23		Small cosmetic error messages fixes. check-in: edf6a9d2ed user: achavasse tags: trunk
19:02		Builtin operators: 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. check-in: c4a6d4d66b user: achavasse tags: trunk
16:55		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. check-in: 8c4fcc68b0 user: achavasse tags: trunk
2020-02-04
21:42		Builtins: implemented helpers to construct complex computed values using expression templates. check-in: 6ed2bd7a75 user: achavasse tags: trunk
20:20		Unfuck some documentation. check-in: 87f7150020 user: achavasse tags: trunk
2020-02-02
23:13		Docs: small layout improvement. check-in: 0521bfdcdf user: achavasse tags: trunk
23:10		Some documentation cleanup and update. check-in: c9186b7b9f user: achavasse tags: trunk
21:47		Refinement types: implemented tests and fixed some issues. check-in: 972099a359 user: achavasse tags: trunk
2020-02-01
23:28		Refinement types: Assert type predicates after a variable assignment Check type predicates when checking a compile-time function call check-in: 216ff2d9c8 user: achavasse tags: trunk
22:54		Refinement types: when calling a function, assert the param's predicates and assume the return type's predicates. check-in: d828564e66 user: achavasse tags: trunk
22:32		Refinement types: assert the return type predicates when returning from a function. check-in: 7259273cf9 user: achavasse tags: trunk
2020-01-28
21:52		Refinement types: assume parameter types predicates at the beginning of functions. check-in: 7f16edb82a user: achavasse tags: trunk
2020-01-27
00:24		Refinement types: parse predicates lazily to play well with templates. check-in: e57c63fea5 user: achavasse tags: trunk
2020-01-23
22:24		Refinement types: implemented the where operator to add predicates to a type. check-in: 9586391cdb user: achavasse tags: trunk
2020-01-22
22:14		Standardized the way type values are encoded to make room for an optional pointer to a list of predicates for refinement types. check-in: cc380f4f8f user: achavasse tags: trunk
2020-01-16
21:41		ir: also make void* always compare to true to make it easier to work with llvm type pointers embedded inside type IR expressions. check-in: 6680e30102 user: achavasse tags: trunk
20:46		ir: comparing ptr< void > is considered always true, to allow to more easily attach opaque data onto ir expressions without changing their semantics. check-in: 1a704c5a51 user: achavasse tags: trunk
2020-01-13
23:13		Renamed the runtime struct type to "record" to avoid future confusion since it's a much lower level type (essentially just a tuple restricted to runtime types) than the future "struct" type. check-in: b573d100cf user: achavasse tags: trunk
2020-01-12
21:10		builtins: added wrapper types to allow terms and values to be manipulated at low level within the language itself. check-in: ceb0b190d6 user: achavasse tags: trunk
20:03		builtins: added a wrapper for a CodeBuilder pointer. check-in: d4e5c46e57 user: achavasse tags: trunk
2020-01-11
18:28		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. check-in: b3aeaae2df user: achavasse tags: trunk
2020-01-05
21:46		Fix (inconsequential) missing else. check-in: 9ad87f2dcf user: achavasse tags: trunk
20:22		Split extpoints.cpp into several files. Fixed a tuple related bug that caused compilation failures when adding parentheses around expressions in some cases. check-in: 5967fcaf06 user: achavasse tags: trunk
17:41		Simplified the implementation of the comma operator. check-in: a25bb3bc5f user: achavasse tags: trunk
2020-01-04
23:44		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. check-in: f6e12ac41e user: achavasse tags: trunk
18:27		Verification: changed the syntax for the current function's return value to the more explicit "@result". check-in: cbbd282cfa user: achavasse tags: trunk
17:28		Loop verifier: when still finding counter-examples at max K unrolls, emit error messages for the failed conditions instead of a generic "couldn't verify loop" message. check-in: 23d2aa4c8a user: achavasse tags: trunk
15:48		Verifier: tweak the wording of the unsatisfiability error for consistency, also sort those by location ids to have a deterministic output. check-in: 264e55dac8 user: achavasse tags: trunk
15:17		verifier: check compilation-time function calls. verifier: improved error messages wording. check-in: 353fcc252a user: achavasse tags: trunk
2019-12-14
21:24		Verifier: fixed multiple issues with nested loop verification. check-in: 693415ce16 user: achavasse tags: trunk
2019-12-11
15:38		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. check-in: b702561850 user: achavasse tags: trunk
2019-12-05
17:40		Implemented a helper to check whether a type is compile-time only. check-in: 12f37d77cb user: achavasse tags: trunk
2019-12-03
20:34		Shift operators: the right hand side must be an unsigned int. Verifier: added tests to check that bitwise operations are properly translated to z3. check-in: 74b73239c8 user: achavasse tags: trunk
2019-12-01
20:17		Verifier: 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). check-in: f1e4ac80ba user: achavasse tags: trunk
2019-11-29
12:15		Verifier: handle phi instructions. check-in: b7dd8a4d25 user: achavasse tags: trunk
2019-11-28
17:53		Verifier: implemented most of the missing instructions (unsigned arithmetic and bitwise operations). check-in: 60e143d189 user: achavasse tags: trunk
2019-11-27
20:24		Verifier: 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. check-in: 18af6c1847 user: achavasse tags: trunk
2019-11-19
20:49		Store a location in loop headers, and use it to provide more context when diagnosing loop verification failures. check-in: 5f20eec65e user: achavasse tags: trunk
20:20		cfg: fix the way the variable ids modified by each loop are stored to avoid duplicate entries. check-in: 1c3ff200aa user: achavasse tags: trunk
00:04		cfg: now that we got rid of this crazy system where CFGs could "call" other CFGs that weren't really functions, removed that clumsy cfg index that was needed to identify temporaries everywhere. check-in: 238df77134 user: achavasse tags: trunk
2019-11-18
22:42		Removed the "inline CFG" llr instruction and related support code. check-in: 5329f83e33 user: achavasse tags: trunk
22:09		Refactor the logic and/or operator to directly append new basic blocks into the current CFG, rather than using a special llr instruction that embeds a nested CFG, whose implementation creates a lot of complexity everywhere. check-in: 70717f6b76 user: achavasse tags: trunk
01:40		Verifier: first seemingly working version of the k-induction loop checker. check-in: 477ef5b3d4 user: achavasse tags: trunk
2019-11-17
18:20		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. check-in: 02836c95bc user: achavasse tags: trunk
2019-11-16
16:27		while: remove code attempting to detect infinite loops, this will be best left to the verifier. verifier: loop unrolling now works. check-in: f7c8245cb2 user: achavasse tags: trunk
2019-11-08
11:48		Verifier: check assertions with z3 immediately instead of postponing it until we have built the entire formula for the function. check-in: e33c4ea6c1 user: achavasse tags: trunk
2019-11-04
19:53		Verifier: more work on loop verification. check-in: b4385d9930 user: achavasse tags: trunk
2019-10-30
22:09		Removed an obsolete comment. check-in: 626057ff22 user: achavasse tags: trunk
22:08		Verifier: more work on loop verification. check-in: c91249ffc7 user: achavasse tags: trunk
2019-10-27
21:31		Verifier: split func.cpp into multiple files to make navigation easier. check-in: f606dd6e5d user: achavasse tags: trunk
2019-10-22
22:11		Verifier: traverse basic blocks in breadth first order and make sure that the current block's predecessors are processed first, so that we don't rely anymore on the order in which they are created by the statements. check-in: d7e2fcc24f user: achavasse tags: trunk
2019-10-20
14:13		Verifier: more work on loop unrolling. check-in: 8082ea7f42 user: achavasse tags: trunk
2019-10-18
11:33		Verifier: 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. check-in: b6662af2e1 user: achavasse tags: trunk
2019-10-16
23:08		llr: detect and store relevant informations about loops in the CFG to be able to unroll them in the verifier. check-in: b1f107d1e7 user: achavasse tags: trunk
2019-10-15
00:04		llr: implemented a helper function to compute dominators. check-in: cfc94e192c user: achavasse tags: trunk
2019-10-12
17:25		Verifier: use z3 push/pop to check assertions one at a time, so that we can find and report multiple errors in the same function. check-in: b414bc18df user: achavasse tags: trunk
2019-10-11
22:24		Docs: add anchors on sub section titles. check-in: 4f4a1dc4aa user: achavasse tags: trunk
2019-10-10
01:00		Docs: typo fix. check-in: d167a0b946 user: achavasse tags: trunk
00:38		Some docs fixes. check-in: e36fbebe18 user: achavasse tags: trunk
00:26		Wrote some docs. check-in: 8f046020b6 user: achavasse tags: trunk
2019-10-09
19:42		Added .editorconfig file. check-in: ed08ba02f2 user: achavasse tags: trunk
19:34		Some more renaming. check-in: f65c08a1c5 user: achavasse tags: trunk
19:21		Some renaming for consistency and to match commonly used names for those things. check-in: 5e72e8e08c user: achavasse tags: trunk
2019-10-08
21:55		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. check-in: 09e8221436 user: achavasse tags: trunk
18:17		Expose "@" as a placeholder for the function's return value inside of ensures statements. check-in: 8541259c1c user: achavasse tags: trunk
18:02		Added the "placeholder" llr pseudo instruction. check-in: cc9ce06e64 user: achavasse tags: trunk
2019-10-07
22:04		Made the "assertion failure" error message lowercase to be consistent with other error messages. check-in: acbb4b30b8 user: achavasse tags: trunk
21:58		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. check-in: 717a1ea6d4 user: achavasse tags: trunk
2019-10-05
16:37		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. check-in: 3740e7a491 user: achavasse tags: trunk
14:50		verification: implemented a trace mode that only dumps the z3 expressions. check-in: 0b95fe304a user: achavasse tags: trunk
13:58		Implemented the conversion of GetVar/SetVar/GetTemporary/SetTemporary to z3 expressions. check-in: 3ae3c0b3ad user: achavasse tags: trunk
11:55		z3 builder: handle variables. check-in: 83476a562e user: achavasse tags: trunk
2019-10-03
20:01		Removed an obsolete TODO. check-in: 251bfddf8b user: achavasse tags: trunk
19:58		FuncValidator: model the execution flow in z3 by generating boolean expressions describing when each basic block is executed. check-in: 6c8e8075ff user: achavasse tags: trunk
2019-10-02
22:15		Typo fix. check-in: 57129c3f9a user: achavasse tags: trunk
22:11		z3 builder: instead of directly adding negated assertions to the solver, gather them into a conjunction and add that. check-in: 2734029a31 user: achavasse tags: trunk
20:09		FuncValidator: more work on the implementation. check-in: 98a85945f6 user: achavasse tags: trunk
19:30		Implemented a helper class allowing to wrap each z3 expression with a predicate indicating that the execution flow went through a certain basic block. check-in: 1d340c945f user: achavasse tags: trunk
2019-09-30
21:50		Began the implementation of the function verifier. check-in: a0c53b4adb user: achavasse tags: trunk
2019-09-29
23:11		repo: don't attempt to perform syntax highlighting on text files. check-in: be610f458b user: achavasse tags: trunk
22:30		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. check-in: 4ae6912760 user: achavasse tags: trunk
20:30		Added a specific llr instruction for 'not' for the sake of constructing z3 expressions. check-in: 2628782ef2 user: achavasse tags: trunk
2019-09-26
23:37		Refactored the parsing of verification statements so that it works properly in all cases (regular functions, template functions, function type expressions, lambdas). check-in: 4fe418f4d0 user: achavasse tags: trunk
00:27		Static analysis: check that function verification statements are satisfiable and emit relevant error messages if they aren't. check-in: 7f14d60722 user: achavasse tags: trunk
2019-09-25
19:16		Implemented a first batch of llr instruction to z3 expression conversions. check-in: b6b76a4e03 user: achavasse tags: trunk
2019-09-24
22:06		Began writing the static analyzer. check-in: d960d10be9 user: achavasse tags: trunk
19:52		Fix wrong file deletion. check-in: 103523bfe9 user: achavasse tags: trunk
19:50		Updated repo's syntax highlighting theme. check-in: 2aafe4e645 user: achavasse tags: trunk
19:13		Updated repo's syntax highlighting. check-in: af5df97f63 user: achavasse tags: trunk
2019-09-23
21:35		build: find the z3 library. check-in: b3c85287b1 user: achavasse tags: trunk
21:00		verification stmts: append to the assertion lists, instead of overwriting them. check-in: db3875c530 user: achavasse tags: trunk
2019-09-22
22:42		Implemented overloads of boolean or/and operators for verification expressions that don't do shortcut evaluation but simply emit the corresponding llr instruction. check-in: 7dcd0447a3 user: achavasse tags: trunk
14:37		Project renaming. check-in: af650a9e95 user: achavasse tags: trunk

Goose Timeline

156 check-ins using file bs/ir/vecgenerator.h version b68308094b