bdemsky [Mon, 31 May 2004 14:19:40 +0000 (14:19 +0000)]
1) Instrumentation code to count model rebuilds, etc...
2) Don't generate code for model definition rules made to make set
constraints explicit.
3) Loop invariant hoisting. We're not too aggressive here...
4) Mechanism to store precomputed values of exprs (for 3)
5) Improvements to Hash function - it now rehashes...
bdemsky [Wed, 19 May 2004 19:06:18 +0000 (19:06 +0000)]
Fixed inteferes bug, improved precision of other analysis to allow
specs to still work.
bdemsky [Wed, 19 May 2004 05:48:34 +0000 (05:48 +0000)]
Worklist items from a previous model build stay in the worklist...this causes lots of problems. We've added a reset method to take care of this...
bdemsky [Wed, 19 May 2004 05:26:41 +0000 (05:26 +0000)]
This one is Dan's. He misparses OR's as AND's for the model definition language. Surprisingly enough, this causes the CTAS spec to have some small problems.
bdemsky [Tue, 18 May 2004 19:11:07 +0000 (19:11 +0000)]
Bugs with generating ands and ors...ahh.
bdemsky [Tue, 18 May 2004 16:46:47 +0000 (16:46 +0000)]
Debug flag bug
bdemsky [Tue, 18 May 2004 16:37:34 +0000 (16:37 +0000)]
C interface to the instrument interface
bdemsky [Tue, 18 May 2004 04:37:21 +0000 (04:37 +0000)]
Need {} around case statements because we define variables...C++ is lame.
bdemsky [Tue, 18 May 2004 04:31:35 +0000 (04:31 +0000)]
Bugs:
1) Sources file assumed filesystem example
2) Bug where we were generating bad code for computing cheapest repair
3) Bug where we were generating if condition for typechecks when we shouldn't be.
bdemsky [Tue, 18 May 2004 04:10:56 +0000 (04:10 +0000)]
Freeciv spec
bdemsky [Tue, 18 May 2004 02:51:28 +0000 (02:51 +0000)]
Filesystem benchmark
bdemsky [Mon, 17 May 2004 22:04:32 +0000 (22:04 +0000)]
Enable quiet output...
bdemsky [Mon, 17 May 2004 22:01:36 +0000 (22:01 +0000)]
getrelation2 can return 0 in cases of a relation that maps objects to ints. This causes the modify update method to get called in the wrong way...Fixed the bug...
bdemsky [Mon, 17 May 2004 21:41:38 +0000 (21:41 +0000)]
Fixed a variety of bugs...
bdemsky [Wed, 12 May 2004 21:40:03 +0000 (21:40 +0000)]
More bugs...
bdemsky [Wed, 12 May 2004 19:03:33 +0000 (19:03 +0000)]
More bug fixes...and debug flags
bdemsky [Tue, 11 May 2004 21:14:26 +0000 (21:14 +0000)]
Code to improve search by pruning certain types of repair..
bdemsky [Tue, 11 May 2004 20:57:57 +0000 (20:57 +0000)]
Various bug fixes.
bdemsky [Tue, 11 May 2004 19:33:49 +0000 (19:33 +0000)]
Forgot to implement this method.
bdemsky [Tue, 11 May 2004 17:12:17 +0000 (17:12 +0000)]
1) Further updates to specifications.
2) Further updates to search algorith.
bdemsky [Mon, 10 May 2004 21:55:09 +0000 (21:55 +0000)]
Improved search....Updated filesystem model. Added -aggressivesearch option.
bdemsky [Sun, 9 May 2004 00:47:18 +0000 (00:47 +0000)]
1) Added useDescriptor method to Expr's.
2) Generalized analysis to determine that an update effecting a rule won't change other bindings of the same rule...
bdemsky [Thu, 6 May 2004 21:17:45 +0000 (21:17 +0000)]
Moved makelib
bdemsky [Thu, 6 May 2004 21:16:22 +0000 (21:16 +0000)]
Moved the interpreter
bdemsky [Thu, 6 May 2004 20:59:21 +0000 (20:59 +0000)]
Organizing
bdemsky [Thu, 6 May 2004 20:56:32 +0000 (20:56 +0000)]
Cleaning up more files
bdemsky [Thu, 6 May 2004 20:55:24 +0000 (20:55 +0000)]
Checking in specs
bdemsky [Thu, 6 May 2004 20:54:36 +0000 (20:54 +0000)]
Moving these
bdemsky [Thu, 6 May 2004 20:53:22 +0000 (20:53 +0000)]
Useless files
bdemsky [Thu, 6 May 2004 20:50:17 +0000 (20:50 +0000)]
These files aren't useful.
bdemsky [Thu, 6 May 2004 20:43:46 +0000 (20:43 +0000)]
size.h is automatically generated
bdemsky [Thu, 6 May 2004 20:41:15 +0000 (20:41 +0000)]
1) Checking in filesystem example
2) Checking in code to handle Booleans/other expressions
3) Added invariants to updatenodes...
bdemsky [Thu, 6 May 2004 06:09:55 +0000 (06:09 +0000)]
Random small changes...
bdemsky [Thu, 6 May 2004 02:05:51 +0000 (02:05 +0000)]
Lots of bugfixes...
bdemsky [Fri, 30 Apr 2004 21:01:35 +0000 (21:01 +0000)]
Added array bounds checks...
bdemsky [Fri, 30 Apr 2004 04:28:22 +0000 (04:28 +0000)]
Should do array index calculations...Wonder if it works correctly?
cristic [Thu, 29 Apr 2004 20:05:08 +0000 (20:05 +0000)]
Don't need "Did you mean literal(...)?" anymore.
bdemsky [Thu, 29 Apr 2004 16:32:08 +0000 (16:32 +0000)]
*** empty log message ***
bdemsky [Thu, 29 Apr 2004 04:47:36 +0000 (04:47 +0000)]
Added improvements to ImplicitSchema analysis, bug fixes to ImplicitSchema
and SetAnalysis, added edges for abstract repairs.
bdemsky [Tue, 27 Apr 2004 21:33:04 +0000 (21:33 +0000)]
Bug in the analysis...oops
bdemsky [Tue, 27 Apr 2004 21:06:40 +0000 (21:06 +0000)]
Added array analysis (computes paths used to add elements/tuples to sets/relations.
Added a bug fix to the graphanalysis routine (must consider nodes not involved in cycles also for removal).
cristic [Mon, 26 Apr 2004 20:44:56 +0000 (20:44 +0000)]
Adding functionality for printing sets.
cristic [Fri, 23 Apr 2004 20:22:14 +0000 (20:22 +0000)]
Grammar changes made today:
G1. Got rid of literal(keyword) thing. Now we can simply use the keywords true, false, etc.
G2. Added keywords NULL=null=0
G3. != works
bdemsky [Thu, 22 Apr 2004 20:55:30 +0000 (20:55 +0000)]
Added code to correctly order checks...
Added code to search through sets for bindings of size 1.
bdemsky [Wed, 21 Apr 2004 21:16:15 +0000 (21:16 +0000)]
Changes:
1) Cleaned up CLI/Compiler classes that Dan provided.
2) Typecheck Constraints.
3) Repair dependence analysis (to order repair of constraints)
A) checks for functions
4) Added class to compute exact sizes of sets (and constraints which
establish these sizes)
bdemsky [Mon, 19 Apr 2004 21:48:08 +0000 (21:48 +0000)]
Update:
1. Removes some old debugging code
2. Simplifies some complex case statements
3. Uses maxsize calculations for set additions
4. Starts to support create/search new element type bindings.
bdemsky [Sat, 17 Apr 2004 00:30:28 +0000 (00:30 +0000)]
Added code to compute maximum sizes of sets. So we can eliminate set removes
when they aren't necessary.
cristic [Fri, 16 Apr 2004 23:14:33 +0000 (23:14 +0000)]
Another bug of cristians
cristic [Fri, 16 Apr 2004 23:03:42 +0000 (23:03 +0000)]
Fixed cristian bug
cristic [Fri, 16 Apr 2004 22:51:51 +0000 (22:51 +0000)]
More bugs fixed.
bdemsky [Fri, 16 Apr 2004 21:13:37 +0000 (21:13 +0000)]
Cristian bug fixes.
bdemsky [Fri, 16 Apr 2004 03:24:53 +0000 (03:24 +0000)]
Fixed some bugs in the analysis.
bdemsky [Fri, 16 Apr 2004 00:19:44 +0000 (00:19 +0000)]
Additional enhancements to compute mustremove and cantremove sets for
node elimination.
cristic [Thu, 15 Apr 2004 23:01:22 +0000 (23:01 +0000)]
*** empty log message ***
cristic [Thu, 15 Apr 2004 22:11:48 +0000 (22:11 +0000)]
Nicer semantic error messages, removed duplicates.
bdemsky [Thu, 15 Apr 2004 22:05:22 +0000 (22:05 +0000)]
Checking in some checks...
cristic [Thu, 15 Apr 2004 21:18:06 +0000 (21:18 +0000)]
OK, the parser now looks more decent.
Still have to work on the semantics errors.
cristic [Thu, 15 Apr 2004 20:20:48 +0000 (20:20 +0000)]
Added the name of the file to the error report.
Changed some error msgs.
bdemsky [Thu, 15 Apr 2004 20:05:54 +0000 (20:05 +0000)]
Committing changes to leftsize->rightSize, more comments, and handling
of MODIFYRELATION.
bdemsky [Thu, 15 Apr 2004 05:42:07 +0000 (05:42 +0000)]
Started adding analysis for modifyrelation nodes.
Added check flag.
bdemsky [Thu, 15 Apr 2004 00:53:00 +0000 (00:53 +0000)]
Bug fixes to make Cristian happy...
bdemsky [Wed, 14 Apr 2004 21:39:30 +0000 (21:39 +0000)]
We don't obey this constraint...
cristic [Wed, 14 Apr 2004 21:08:30 +0000 (21:08 +0000)]
Some modifications to allow to print the name of the file when a syntax error is reported.
cristic [Wed, 14 Apr 2004 19:16:27 +0000 (19:16 +0000)]
The steps necessary to run the compiler on a new set of specs.
bdemsky [Tue, 6 Apr 2004 20:12:45 +0000 (20:12 +0000)]
Example program.
cristic [Tue, 6 Apr 2004 20:02:51 +0000 (20:02 +0000)]
Strange formatting issues changed...
bdemsky [Tue, 6 Apr 2004 19:57:17 +0000 (19:57 +0000)]
Checking in redblack sources
cristic [Tue, 6 Apr 2004 19:49:26 +0000 (19:49 +0000)]
Forgot this file.
cristic [Tue, 6 Apr 2004 19:42:05 +0000 (19:42 +0000)]
...
bdemsky [Tue, 6 Apr 2004 02:48:30 +0000 (02:48 +0000)]
Made flag work for checking only...Added support for modify relation updates.
bdemsky [Fri, 2 Apr 2004 19:56:07 +0000 (19:56 +0000)]
Changed iterator behavior...It only iterates over the items in the set
at the iterators creation time.
bdemsky [Fri, 2 Apr 2004 19:31:11 +0000 (19:31 +0000)]
Compute strongly connected components of model rules, and do computations the correct way...
bdemsky [Fri, 2 Apr 2004 19:29:48 +0000 (19:29 +0000)]
Fixed random bugs in the runtime.
bdemsky [Thu, 1 Apr 2004 18:45:12 +0000 (18:45 +0000)]
Replaced findcycles method with something more efficient based on SCC computation.
bdemsky [Thu, 1 Apr 2004 16:23:06 +0000 (16:23 +0000)]
Added Strongly Connected Component support into GraphNodes.
bdemsky [Wed, 10 Mar 2004 06:49:50 +0000 (06:49 +0000)]
Fix random errors/typos...
bdemsky [Wed, 10 Mar 2004 06:15:03 +0000 (06:15 +0000)]
Added:
Concrete Interference rule that falsify a rule that quantifies over a set can't
remove the last element of the set.
Concrete Interference rule that updates that definitely falsify a rule can't modify
the inclusion condition causing a possible addition.
Intelligence in the GraphAnalysis package that computes must & cant remove sets.
Search through only unique combinations.
bdemsky [Mon, 8 Mar 2004 00:28:36 +0000 (00:28 +0000)]
Added support for stack allocation. Check for NULL before calling memory checker.
bdemsky [Mon, 8 Mar 2004 00:27:52 +0000 (00:27 +0000)]
Added support for stack allocation...
bdemsky [Sun, 7 Mar 2004 22:02:43 +0000 (22:02 +0000)]
Still buggy, but getting closer...
bdemsky [Sun, 7 Mar 2004 22:00:14 +0000 (22:00 +0000)]
Added:
3 value logic for Expr's...This will break dan's stuff, but arguably
it is the first step in fixing his stuff...
Runtime support for checking type sanity/etc...
bdemsky [Fri, 5 Mar 2004 05:26:51 +0000 (05:26 +0000)]
Runtime for checker...
bdemsky [Mon, 1 Mar 2004 17:29:14 +0000 (17:29 +0000)]
Mistake in interface assumptions...
bdemsky [Mon, 1 Mar 2004 05:40:13 +0000 (05:40 +0000)]
*** empty log message ***
bdemsky [Fri, 27 Feb 2004 20:34:48 +0000 (20:34 +0000)]
Creating a runtime directory...
bdemsky [Fri, 27 Feb 2004 08:22:55 +0000 (08:22 +0000)]
Dan was leaking memory via iterators... This leak is fixed now (stack allocation of iterators).
bdemsky [Fri, 27 Feb 2004 07:41:19 +0000 (07:41 +0000)]
Checking in super-optimized SimpleHash code... Good for a little performance increase...
bdemsky [Fri, 27 Feb 2004 05:52:04 +0000 (05:52 +0000)]
Checking in update to hashtable code...
bdemsky [Thu, 26 Feb 2004 22:51:10 +0000 (22:51 +0000)]
Adding test case & bug fixes to generate code for test case...
bdemsky [Thu, 26 Feb 2004 20:13:49 +0000 (20:13 +0000)]
Fixed Dan's confusion regarding alignment of fields. Modified the
OpExpr class to support more operations, and to actually perform the
operations when possible. (I like readable code!)
Wrote code to write to data structures...Should be the last major
component..
bdemsky [Wed, 25 Feb 2004 22:38:02 +0000 (22:38 +0000)]
Checking in code that:
1) performs consistency checks
2) doesn abstract repairs
3) calls/schedules data structure updates
4) partially data structure update code
bdemsky [Wed, 25 Feb 2004 00:06:15 +0000 (00:06 +0000)]
Updating files...
bdemsky [Tue, 17 Feb 2004 19:43:40 +0000 (19:43 +0000)]
New runtime for repair system.
bdemsky [Tue, 17 Feb 2004 18:53:08 +0000 (18:53 +0000)]
These checking do the reconstruction of the model and invoke concrete repairs.
bdemsky [Thu, 12 Feb 2004 06:53:39 +0000 (06:53 +0000)]
Adding code to generate repair algorithms. Its not complete yet...
This checkin sets defaults to repair...
bdemsky [Fri, 6 Feb 2004 22:33:01 +0000 (22:33 +0000)]
Checking in code to perform safety checks on repair dependency graph.
bdemsky [Thu, 5 Feb 2004 07:18:20 +0000 (07:18 +0000)]
Added support to printout data structure update nodes (bindings/updates)
Added support to simplify updates/determine if they are self consistent
Added support to sequence updates
Improved precision of data structure update analysis
bdemsky [Wed, 4 Feb 2004 15:39:15 +0000 (15:39 +0000)]
Adding changes to cvs...
bdemsky [Fri, 23 Jan 2004 03:58:49 +0000 (03:58 +0000)]
Fix some of Dan's bugs (code generation for relation quantifiers misstyped), didn't allow for relation quantifier in constraints, and my bugs.
bdemsky [Sat, 10 Jan 2004 05:00:03 +0000 (05:00 +0000)]
Fixed lot of random bugs. Added code generate strings for expr's.
More code to generate concrete updates. Initial code for computing
interference....