Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

C++: static cast fails to invoke #convertStatic #263

Closed
h0nzZik opened this issue Feb 13, 2017 · 5 comments
Closed

C++: static cast fails to invoke #convertStatic #263

h0nzZik opened this issue Feb 13, 2017 · 5 comments
Assignees

Comments

@h0nzZik
Copy link
Contributor

h0nzZik commented Feb 13, 2017

I have some partial/experimental implementation of C++ enumerators, and for debugging purpuses I wanted to static_cast them to integers and back. Static cast, as described in 5.2.9:4-5 and implemented in cpp14/language/translation/expr/cast.k, first tries to direct-initialize a new temporary variable, and if that fails, it performs some conversion from 5.2.9:6-12 (implemented by #convertStatic). However I encountered some problems while casting integers to enums.

Ints are not implicitly convertible to enums, so they should be converted by #convertStatic. First problem is that some rules in cpp14/language/common/conversion.k allow implicit conversion of ints to enums. That is easy to fix.

But after fixing that (and implemeting some productions like min, max etc) I was not able to make figureInit() rewrite to ill-formed (or cannot-convert) in compile time (while running static semantics). For the cast in this piece of code

enum E{};
int main() {
    int a = 4;
    (E)a;
}

the translation semantics yields

`ExpressionStmt`(lecpp(`ExprLoc`(`CabsLoc`(...),
`_:=__CPP-SYNTAX`(
	lecpp(
		temp(...),
		hasTrace(...),
		tcpp(...,..,unscopedEnum(...))
	),
	`ConvertType`(
		tcpp(...,...,unscopedEnum(...)),
		`ExprLoc`(`CabsLoc`(...),`ExprLoc`(`CabsLoc`(...),
			`Name`(`NoNNS`(.KList),`Identifier`(#token("\"a\"","String")))
		))
	)
)),hasTrace(...),tcpp(...,...,unscopedEnum(...))))

which then evaluates to cannot-convert during runtime. I was trying to check the ill-formedness in assignment.k, but without much success, because the convertType(_,_) gets rewritten to ConvertType(,), which does not get rewritten anymore if the second parameter is a variable.

When trying to convert constant (e.g. (E)5), then convertType correctly rewrites to cannot-convert. @dwightguth any idea?

@dwightguth
Copy link
Member

so, first of all, you are correct that we should probably add notBool isCPPEnumType(T) to the side condition of the rules in conversion.k. They exist in that form because they need to be able to handle char16_t, char32_t, and wchar_t, which are integer types but neither signed nor unsigned types. It was written without thinking that far ahead about enumerations at the time.

I believe what you want to try to do is to add a side condition to the rule that creates ConvertType nodes in the tree which asserts that the types involved make the conversion possible in some fashion.

@dwightguth
Copy link
Member

I am working on a fix for this issue and should have it out soon. I would wait and come back to this once that's done.

@dwightguth dwightguth self-assigned this Feb 14, 2017
@h0nzZik
Copy link
Contributor Author

h0nzZik commented Feb 14, 2017

I have already created something for both parts. Do you think it would not be sufficient, or it is too ad-hoc?

@dwightguth
Copy link
Member

Yes, this is too ad-hoc. I will have something out in the near future that should work without breaking the structure that I already began laying out

@h0nzZik
Copy link
Contributor Author

h0nzZik commented Feb 26, 2017

This was probably fixed in 6cd2af9. Can we close it?

@h0nzZik h0nzZik closed this as completed Mar 9, 2017
rv-jenkins pushed a commit that referenced this issue Dec 20, 2017
* Squashed 'errors/' changes from 2f076ad..7867856

7867856 fix issue with relative path to rv-error parent pom (#599)
0103eb1 Fixes #552 (#567)
4aed6116 HTML report for mobile device (#563)
6a033bc HTML report local variables table (#542)
cc8e363 MISRA-C citations. (#539)
5b4f246 Added type descriptions (#526)
aaeeff1 fix ocaml warnings and change build system to mark most ocaml warning… (#511)
2ffe5dd Setjmp (#527)
422ae42 Support for asprintf, vasprintf. (#524)
2cb6696 html report improvement 1 (#521)

git-subtree-dir: errors
git-subtree-split: 7867856d7766253eb9000146539d4b6ea88304ce

* Squashed 'errors/' changes from 7867856..43ff95c

43ff95c Resolve rv-error subtree conflict.   (#830)
9475042 Merge pull request #823 from runtimeverification/independent-ocaml-build
05bcf1c Merge pull request #822 from runtimeverification/multiple-races-per-report
509fbdc Merge pull request #821 from runtimeverification/fix-path-shortening-and-indentation
43bdfab Make RV-Predict use its own OCaml/OPAM configuration at the top of the RV-Predict directory, instead of using the user's configuration in ~/.opam/.  Add a script that sets that up, opam-setup.sh.  Update doc/BUILDING to suit.  Make git ignore the top-level .opam/ directory.
6880020 Added `try...catch...` for sessionStorage
2eedd8d Shorten more paths.  Fix indentation of `- locked` lines.
b73f6c0 Process *every* data race the backend produces, not just the first one.
82788d2 Refactor code
53dea82 Fixed string secape error
79c3599 Removed .load(ajax) call. Generate javascript instead of html for sourcecode
eb69372 Revert "Removed jquery load function (Removed ajax call). Now http-server is not required anymore"
640cd3e Removed jquery load function (Removed ajax call). Now http-server is not required anymore
cf500ca Changed layout
e69545c Fixed layout
28c8878 Merge branch 'master' of https://github.com/runtimeverification/rv-predict into rv-predict-html-report
80b474a Resolve conflict
72e61dc Pull rv-error subtree.
9baa8f6 Always add an empty line between the stack traces.
0807946 Fix `depend` target for errors/bin/, errors/lib/.
55d97e7 Setjmp (#527)
b76f623 Support for asprintf, vasprintf. (#524)
d05b5e2 html report improvement 1 (#521)
1f5c419 fix rv-error to not throw exception on empty string on stdin
7bfcefb Make git ignore a build product, rv-error.
855a802 Add a reachover build for rv-error & rv_error.
d21a773 Updated rv-error doc with info about bootstrapping
e68705d Make rvpsymbolize-json and rvptrimframe work.
b100caf Fix indentation of elided library frame indication.
a2d7eae Make git ignore more build products.
f1a0ed1 Bring the output in line with my design.
09cca5a Merge pull request #800 from runtimeverification/rv-error-subtree
869308d Make the integration testing more stable. (#796)
42ff5fd Fixes for the c installer. (#798)
2d345bc Working version of the C installer. (#795)
7e576da Fix the rv-predict-master build (#797)
13de31d Draft for installing RV-Predict-C from a deb file. (#794)
5ffe8e7 Fix the most obvious rv-predict installer issues. (#792)
e3f0add Merge pull request #791 from virgil-serbanuta/master.finished-threads
c629f0a Fix the computation for threads that end in the current window.
5bd3942 Preserve signal enabling state accross windows. (#786)
ec57cdb Add counters for event types. (#787)
d64c1a0 Merge pull request #784 from virgil-serbanuta/simpler-faster.java-instrumentation
5894483 Renamed variables.
a0632a1 Documentation improvements and variable renaming.
aeb207a Add a test for Scala instrumentation.
f7fb571 Add a test for Scala instrumentation. Scala is special because it initializes fields before the super constructor call.
677ee9c Actually fix the constructor call bug.
0ec05e6 Fix issue #782 by having better checks for self calls.
3ac2cc6 Merge pull request #783 from virgil-serbanuta/simpler-faster.profiler
54e5c68 Fixed review comments.
1f8d523 Check the profiling flag when displaying the profiling results.
b342e25 Add a time profiler.
92c02b3 Merge pull request #781 from virgil-serbanuta/simpler-faster.timeout-bug
f0bf450 Use the solver with the largest timeout as the main solver.
e874cbf Merge pull request #777 from virgil-serbanuta/simpler-faster.atomic-interruptions
fd8a5f5 Merge pull request #779 from runtimeverification/simpler-faster.binary-rvpdump
7e9848f Fix merge errors.
809dc41 Fix a corner case where rv-predict was interrupting atomic events.
d440a62 Merge pull request #780 from virgil-serbanuta/simpler-faster.corner-cases
bdb09be Fix the integration tests.
fe730c1 Merge pull request #772 from virgil-serbanuta/simpler-faster.corner-cases
2de9989 Add support for a binary output format, -t binary, and a limit to the number of trace records emitted, -n #traces.  The limit can be used with any of the output formats.
4e61f14 Merge pull request #778 from runtimeverification/simpler-faster.deep-rvpdump
1906e3e Track up to 15 signals on top of each thread, a depth of 16 in all.
25518b0 Comment out some asserts.
88c0d7b Merge pull request #776 from runtimeverification/simpler-faster.misc-fixes
1cc68fe Mention rvplicense in the Getting Started section.
b9e5ea0 Install rvplicense, a barebones utility for fetching a new license key.
e0a4a58 Add some more detail to the manual page, and specify Linux as the operating system for this program.
2a287e9 Specify Linux as the operating system that he manual page is for.
d1a7980 Fixes for signal corner cases.
9dd419f Make git ignore more vim swap files, .*.sw*.
14efb2d Merge pull request #775 from runtimeverification/simpler-faster.misc-fixes
ea43eb6 Wrap a long line in the message about the missing/invalid license key.
0624596 Ignore build products.  Add share/ to the set of directories that the `clean` target should remove.
6e20929 Belatedly update Makefile for change of filename, manual -> manual.md.
910d363 Build all of the C++ examples.
7ad9e2c Define the feature macro that dprintf(3) and getopt(3) require, so that kcc doesn't gripe.
1e1b5d2 Avoid wasting resources: don't leave a tail(1) process hanging around in the background when deb-release.sh quits.
431b424 Merge pull request #773 from runtimeverification/simpler-faster.man-pages
184058c Fix the bug Virgil found: move the words following .Nm in the DESCRIPTION section to a line of their own.
3677f5b Merge pull request #770 from runtimeverification/simpler-faster.quicken-compile
1837adb Workaround mk-configure bugs: use a custom chown(1) that uses fakeroot if FAKEROOT_FIFO is in the environment.  mk-configure uses a "naked" chown call instead of mkc_install or $INSTALL to create compressed manual pages with the proper permissions.  I set CHOWNPROG to the original chown, to avoid recursion through `fakeroot -s $INSTALL` (fakeroot doesn't like it) and then I add rv-predict/bin/ to the PATH to get my custom chown.
e17a87a Appease lintian(1) by stripping everything, compressing manual pages, and embedding no timestamps in compressed manual pages.
aa28c66 Mention rvpc++ in the rvpc manual page, and link them during installation.
9cbcfca Quiet complaint about incorrect permissions on DEBIAN/*.
e26f1ac Set the proper base directory and ownership for manual pages.  Compress them if we're installing with a fakeroot.
f7cbb5c Delete empty lines because they make lintian(1) gripe.
8399354 Add manual pages for rvpa, rvpc, rvpdump, rvpsymbolize, and rvpx.
c27e14d Flesh out usage information.
2e339ff Only when -M or -E are passed should we skip normal compilation. This fixes the ITC benchmark build.
2c413ee Flesh out the usage information.  Exit with a distinct return value on every condition.
2e300a0 Flesh out the usage information.
a149f4f Ignore build product manual.rst.
59c0134 Rename manual -> manual.md.  Add a target for a reStructuredText manual, manual.rst.  Fix the journal-article citations in the manual.
1833b1c Merge pull request #764 from virgil-serbanuta/simpler-faster.davids-trace
f966a05 Merge pull request #768 from runtimeverification/simpler-faster.rvsyms-paths
35b8ce1 Merge pull request #766 from virgil-serbanuta/simpler-faster.maven-sanity
cffda07 When the -p option is on the command line, precede the name of the file where a symbol is defined with the compilation path for that file.
18320f1 Don't strip the RV-Predict/C runtime.  I'm not sure why my copy of mk-configure 0.29.1 does not strip, and Dwight's copy does, but that's what happens.  We mustn't strip it because we need some symbols from it---e.g., __rvpredict_thread_wrapper, in order to trim the stack traces properly.
63a0a69 Make some changes designed to speed up compilation: don't build TSAN unless BUILD_TSAN is set to "yes".  Don't build elftoolchain components that we don't need.
410d014 Make this more nearly compilable.  I thought that I was going to re-use this code just now, but I was wrong, so I will leave it in this state.
90b34f3 Change the old simplereader.c comment to one that applies specifically to rvsyms.c
b49e57d Make sure that $(.CURDIR) is on the C #include path so that strstk.h can be found.
d995372 Handle signals that do not start in the current window.
b357a93 Merge pull request #765 from runtimeverification/better-release
3505ef8 Add proper citations.
ccbceae Per Dwight's recommendation, get the classpath for the .jar from rv-predict-source/ instead of from rv-predict-jar/, because Maven is weird.  Delete my hackish addition of rv-licensing as a dependency of rv-predict-jar, since it should not be necessary any more.
fa76588 Remove another duplicate --, s/----no-symbol/--no-symbol/.
868a4fc Fix doubled -- in usage().
25bd7c5 Update documentation per Virgil's reminder.
9a69d36 Add 'set -u' to every script so that it gripes and quits if an undefined variable is used.  This will help us catch bugs in the future.
678c609 Add some scripts for evaluating TSAN versus RV-Predict on the Stolz queue.
a910b1c Add an unfinished Makefile for building a 32-bit runtime.
0cdd9f1 Add some comments per Virgil's comment.
75ab358 Add an experiment with raise(3) to verify that when the signal it raises is masked, the handler doesn't run immediately.
d76d2f0 Print the signals that are in the default mask.
377bc04 Do not use an uninitialized variable (!) to set the interrupts-enabled mask.  Just block the signals that we use for synthetic interrupts in __rvpredict_intr_disable(), and unblock them in __rvpredict_intr_enable(). Delete __rvpredict_intr_init(), it was never used.
410be93 simple ocaml program to symbolize raw stack error json
c45be4f Fix all of the problems that Brandon and Virgil mentioned.
cbe617b Fix the placement of square brackets in the rvpa/rvpx/rvpsymbolize usage. Add an option `--filter no-shorten` that turns off the path shortening. Fix the path-shortening bug that I found, today.
69e8cd9 Add draft manual.
afe2884 Per Virgil's suggestion, use `|` to separate alternates on the command-line instead of `,`, since `|` is more conventional.
131dd8e Write some explanation about postrm in comments.
fc70a6a Refine the license query a bit.
4ca6eca Remove commented-out lines.
5d28084 Make all of the POM files depend on a version of rv-licensing between 1.1-SNAPSHOT and 1.4, exclusive.
c0caa9d Make rvpa and rvpx pass --prompt-for-license to the Java backend.
800acae Use the count as a count, again, instead of flipping its sign back and forth.  We still find the races.
70acee2 Delete some scripts that RV-Predict/C doesn't use any more.
82d27a4 Make deb-release.sh executable like release.sh.
b4d146f Generate DEBIAN/control in deb-release.sh.
55c306f Flesh out the manual some.  Still need to finish up my description of the report format.
cf9ddf7 Use fakeroot(1) to avoid constructing the Debian binary package as root.
75818d2 Bail on unchecked errors.
991dc57 Now that I'm building only static libraries for libdwarf and libelf, there's no need to statically link rvsyms in order to force the elftoolchain versions to be used.
f42e58b Apparently, you cannot exit a shell script twice: when my exit_hook trapped EXIT and re-exited, cleanup_hook was not called like I was expecting.  So call it directly, instead.
7a8e95f Fix some lint found by lintian.
491ae50 Add to rvpa, rvpx, and rvpsymbolize a --filter option that tells a keyword list of filters to disable: no-symbol, no-system, no-trim, no-signal. Implement no-symbol, no-trim, and no-signal.
e1975ac Add an rvp_ prefix to symbols in the interrupts simulation so that it's easier to filter those symbols out of race reports.
a0f302c Nevermind, I cannot really skip the Maven step for the `install` target after all.
644ab08 Make git ignore *.deb.
59412a5 Move DEVELOPERS under doc/.
4086864 Make the Maven build quiet unless NOISY!=no is set.  I set NOISY=yes in the rv-predict-c-release build on Jenkins.
d410eae So that Maven brings releases up-to-date, run mvn with -U option.  Don't use the -q option, that may be too quiet for the Jenkins log.
f38ce59 Don't run the analysis twice.  The trap handler for rvpx was running it a second time after rvpx ran it at the end of the script.
ec60ed6 Call Maven with -Dobfuscate to obfuscate the Java classes.
033b1e4 Explicitly set a top-level PROJECTNAME so that it isn't derived from the current directory, which is different in Jenkins than anywhere else.
3b1a2e5 Make release.sh executable.
ecdd0a8 Make the release script agree with Jenkins' expectations: add an argument for a version number, and produce a file called rv-predict-c-${version}.tar.gz.
6e19050 Fix rv-predict-source packaging and z3 libraries.
3669688 Merge pull request #762 from virgil-serbanuta/simpler-faster.invalid-signal-races
28e0ffa Performance improvements for soundness and tests.
692fe39 Merge pull request #761 from virgil-serbanuta/simpler-faster.lock-representation
ef0092d Soundness for signal interrupts.
f834d4a Merge pull request #757 from virgil-serbanuta/simpler-faster.signal-start-mask-or
c8b2019 Bracketing for locks.
f41eaf3 Lock formatting in race reports.
82adf28 Compute the signal mask as an OR...
9f0687c Merge pull request #759 from virgil-serbanuta/simpler-faster.get-license
69e821a Change the rv-predict code to match the latest licensing API.
8eeb464 Merge pull request #758 from virgil-serbanuta/simpler-faster.get-license
2ad770b Use the new licensing API.
7270310 Merge pull request #756 from virgil-serbanuta/simpler-faster.fix-licensing-dependencies
549a523 Add an upper limit to the licensing version.
e4127d9 Merge pull request #754 from runtimeverification/simpler-faster.fix-mask-instrumentation
97ff758 Merge branch 'simpler-faster.fix-mask-instrumentation' of github.com:runtimeverification/rv-predict into simpler-faster.fix-mask-instrumentation
3bde701 Instrument sigsuspend(2).  This seems to prevent the backend from getting confused and asserting.
87bb184 Fix a bug that zeroed the top 32 bits of masks that were memoized in the trace: cast the constant 1 to uint64_t before shifting left so that we don't end up shifting a narrower constant outside the range that it can represent.
940a85c These changes are just along for the ride: fix the top-level `tags` target, which was broken in elftoolchain/; delete some whitespace at the end of a line; make my test program, sigcount, a little more useful.
9ccc223 Merge pull request #747 from virgil-serbanuta/simpler-faster.get-license
76afaf7 Merge pull request #752 from virgil-serbanuta/simpler-faster.bug-from-david
5181f8e Fix a bug that zeroed the top 32 bits of masks that were memoized in the trace: cast the constant 1 to uint64_t before shifting left so that we don't end up shifting a narrower constant outside the range that it can represent.
9d1a18c These changes are just along for the ride: fix the top-level `tags` target, which was broken in elftoolchain/; delete some whitespace at the end of a line; make my test program, sigcount, a little more useful.
d804673 Merge remote-tracking branch 'virgil-serbanuta/simpler-faster.bug-from-david' into simpler-faster
652b7e9 Fix the assertion error and one more error which showed up in David's trace.
2768751 Merge pull request #751 from runtimeverification/report-tweaks
07b912d Clean up after rvpsymbolize.  Now there is lots of copy-and-paste code in rvpsymbolize.  I should factor it out.  Maybe put it in a lib/common.subr that each script can source at its top?
148f235 Clean Maven build products more thoroughly.
4f34997 Update the trace specification per my conversation with Virgil, today.
72be954 Fix the report appearance when locks are held during an interrupt: put the newline *after* the held-locks report, not before.
e69c4b3 Add an option, -l, for protecting the main thread with locks.
b67ba5f Add more build dependencies (the ones Virgil found today) and sort.
dec509c Extract rvpa, a program that analyzes an rvpredict.trace file, from rvpx.  Now the user can easily analyze an rvpredict.trace that's left in the current directory when they run an RV-Predict/C-instrumented program without using rvpx: they just run `rvpa program`.
579ad27 Change RV-Predict[C] to RV-Predict/C throughout.
da9de28 Add a command-line flag, -g, that makes rvpdump print the generation number for each line of 'plain' or 'symbol-friendly' output.  In the course of implementing that, I extracted a subroutine preamble_string() that prints tid <m>.<n> and optionally prints tid <m>.<n> gen <o>. That helped to shorten the code a bit.
0083ebe Warn, but don't exit, if pthread_mutex_init() is passed attributes.
16dc2ca Rename getRaceLocationSig() to getRaceDataSig() throughout.
3f0a983 Start to flesh out the manual.
504e6e7 Make git ignore vim's .*.swp throughout the tree.
4c04b65 Ignore .*.swp everywhere.  Add some rudimentary notes about dependencies to the (highly incomplete) BUILDING document.
a351c07 Refactor the SMT model to extract the constraint building part. (#749)
6c363bd Change a = to += so that Makefile isn't omitted from the FILES variable. (#748)
59423be Merge pull request #746 from runtimeverification/simpler-faster.installer-and-release-prep
c064f25 Merge branch 'simpler-faster.installer-and-release-prep' into simpler-faster
2cef02b Merge pull request #740 from runtimeverification/simpler-faster.enterfn-with-callsite-2
1e1777c Simplify using wildcards ** and *.
911d84e Remove call stack events from the to fix failing tests (they were added in the current pull request).
b72c3b7 This is what I put on a VM for DENSO last night.
181de1d Make the rv-predict tool prompt for a license user name and password when needed and when asked to do so.
3e901fd Attempted to fix the build.
460190b Ignore a bunch of test products.  What are those files doing there, anyway?  Does nothing clean them up, not even 'mvn clean'?
4b7f37e Go ahead and compile and link if -MD is on the command line.  Continue to skip compilation & linking of -M<anything else> is on the command line.
54d1cc1 Merge branch 'simpler-faster.enterfn-with-callsite-2' of github.com:runtimeverification/rv-predict into simpler-faster.enterfn-with-callsite-2
ee2e975 Merge branch 'simpler-faster' into simpler-faster.enterfn-with-callsite-2
d01aff2 Fix some compile errors.
5fde389 Get rid of experimental 'ranIt' stuff.
310c620 Only create the Z3 library directory *once*.
cd9c5f1 Merge pull request #743 from runtimeverification/simpler-faster.examples
f90a537 Merge branch 'simpler-faster.do-not-share-libz3java.so' into simpler-faster.examples
88c68e6 Only create the Z3 library directory *once*.
95b4216 Merge pull request #744 from runtimeverification/simpler-faster.jenkins-build
71bac7d Protect against a user stepping on another's toes: extract libz3java.so in a private temporary directory, not in /tmp/.  This should make Jenkins more reliable, among other things.
c7d5510 Use the log dir for unpacking the z3 library.
f47c6c0 Merge branch 'simpler-faster.do-not-share-libz3java.so' into simpler-faster.examples
9199557 Merge branch 'simpler-faster.do-not-share-libz3java.so' into simpler-faster.jenkins-build
2a807d7 Protect against a user stepping on another's toes: extract libz3java.so in a private temporary directory, not in /tmp/.  This should make Jenkins more reliable, among other things.
2748298 Merge remote-tracking branch 'origin/simpler-faster.enterfn-with-callsite-2' into simpler-faster.enterfn-with-callsite-2
1521a9e Use the call site address for stack traces.
e70fd00 Add the C11/C++11 examples from rv-predict-c.  By default, building examples/ installs them under $PREFIX/share/examples/rv-predict-c/. If MKBIN=yes, however, the examples are built in-situ, which might be preferred by developers.  Otherwise, a developer can cd $PREFIX/share/examples/rv-predict-c/ and build there.
4e55088 Don't build ar and elfcopy, we don't use them, and they want to link with libarchive, which is not installed on the Jenkins box right now.
b53b071 Make git ignore a bunch of .po files that were build products on the Ubuntu 14.04 Jenkins box for some reason.
44e8818 Explicitly filter out some mk-configure targets (uninstall, etc) that make mk-configure gripe if we replicate them.  Pass MKPIC=no to the elftoolchain build so that it doesn't try to run 'cc -soname', because that doesn't work with the default cc on our Jenkins box (Ubuntu 14.04).
fbd0101 Be more compatible with Ubuntu 14.04 and its version of cmake, 2.8.12.2.
7692a4b Fix some bugs that clang 3.8.1 finds but gcc or clang 3.8.0 does not?  I'm not sure what the difference between rvwork-1 and rv-server-1 is in this instance, but it's fixed, now.
43f3827 Install rvpc from the right directory, and set a PATH that will find it there, too.
7cdf9b0 Install the native-z3 stuff so that a developer's RV-Predict/C .jar can find it.  This adds five seconds to the build time, ugh, but it's necessary for a replicable build.
a8b6d29 Use the call site address for stack traces.
18df1c7 Add the callsite to 'enterfn' events.  Update the documentation. Update rvpdump.  Increase the version number to 0.0.0.3.  This breaks the analysis backend.  Funny thing is, the backend doesn't quit immediately when it reads version number 0.0.0.3.
f5f05e3 Merge pull request #741 from runtimeverification/simpler-faster.add-elftoolchain
7426ff8 Merge pull request #742 from virgil-serbanuta/fix-broken-test
3f0486b Fix a broken test.
f8cbf6d Add a reachover build for elftoolchain.  On Linux, build and link against elftoolchain instead of whatever is installed.
1047737 Ignore a bunch of build products.
aeda72c Create external/bsd/ for BSD-licensed, 3rd-party sources.  Put elftoolchain release 0.7 in there with all of its Subversion metadata, for ease of updating.
5138fc2 Merge pull request #737 from runtimeverification/simpler-faster.improve-race-reports
9260367 Improve the debug output by only displaying the events involved in the race and doing fewer thread switches. (#735)
c6fe804 Bug fixes an a small decrease in the SMT formula size. (#734)
b23442c Removing the whitespace at the end of a data race-report line broke a bunch of tests.  Fix them.
590f094 Repair indentation.
2080f06 Add a comment about the meaning of exit codes 126 and 127.
d9ff46e Merge pull request #736 from runtimeverification/simpler-faster.installer-and-release-prep
8c39e9e Put race reports on local variables into a format that rvpsymbolize can symbolize.  Refactor a bit: move getRaceLocationSig() from Race to MetadataInterface.  In the CompactMetadata class, make getRaceLocationSig put the instruction pointer and CFA of all of the relevant frames inside of the square brackets.
6644022 Run `mkcmake depend install` to install the C instrumentation & runtime under ../target/release/rv-predict/.
176392e Exclude from the installation under lib/ all files under native/. Those seem to have something to do with Windows, where RV-Predict/C definitely does not run.
9be3282 If there is not a valid, current license key installed, don't ask the user for one on stdout.  Instead, print an error and some instructions to stderr, and exit with a non-zero exit code.
7f399aa Don't build the rv-predict.jar if MKJAR=no.  If MKJAR=yes, or if it is unset, go ahead and build the .jar.  The Maven build for the RV-Predict/C installer will invoke the top-level make with MKJAR=no to prevent infinitely re-entering the Maven build.
0fc790b Merge remote-tracking branch 'refs/remotes/origin/simpler-faster' into simpler-faster
6eb8131 If the command is not found (exit code 127) or if it is found, but not executable (exit code 126), don't try to perform prediction.
a216716 Fix the performance issues caused by signals. (#731)
7a46468 Make git ignore only rv-predict.jar.copy instead of *.copy.
21e1abf Don't increase the stack limit.  That was necessary for the Java instrumentation, which adds stack frames on top of the application's stack frames.  That's not a concern for RV-Predict/C.
0a1c464 Merge pull request #733 from runtimeverification/simpler-faster.misc-build-changes
f04c6c1 Merge branch 'simpler-faster' into simpler-faster.misc-build-changes
ae99f07 Merge pull request #732 from virgil-serbanuta/simpler-faster.rename-data-methods
4cdeaf8 Merge pull request #727 from virgil-serbanuta/simpler-faster.signals-enabled-by-mask
3b24ad2 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster.misc-build-changes
15ff8e2 Make git ignore a bunch of build products.
361179b Rename the methods againg to match what they are doing.
ba701ea Fix small bug
34b44c0 getDataAddress renaming
0537b60 Bracket racy addresses with CFAs from the racy threads. (#729)
4dedc40 Symbolize UNIX signals in a way that's appropriate for Linux/x86. (#726)
1979623 Analyze interrupts by default. (#730)
52d3bca Remove unneeded diff.
4052fb8 Also add a test for races.
99c6cca Race reports with bracketing.
8dc4866 Fix broken test.
c75739c Code cleanup.
83bab6c Fix a sigset ordering error and add a test.
58546d3 Signals interrupt signals when the sigset mask allows it.
8632188 Fix races involving atomic events. (#721)
f6b33fd Merge pull request #723 from virgil-serbanuta/simpler-faster.fix-commented-regression-tests
2bc158a Merge pull request #722 from virgil-serbanuta/simpler-faster.thread-start-information
2aa3d5c Merge pull request #719 from virgil-serbanuta/simpler-faster.signals-on-signals-implicit-enabling.2
d33d134 Merge pull request #724 from virgil-serbanuta/simpler-faster.fix-thread-formatting
61b31d1 Fix event type comparisons
29c48aa Make the interrupted thread/signal formatting consistent with the main thread formatting.
6fef360 Remove a test without data and add a comment explaining why the last commented one does not work.
7339bd8 Fix the stack test.
8c29b23 Fix the offline ftpserver.jar test.
036a81f Merge pull request #717 from virgil-serbanuta/simpler-faster.fix-regression-tests
6b8ee99 Stop reading thread start information metadata from trace dumps since it is added on-the-fly to the metadata.
9fee0f1 Fix more tests.
89ec0b1 Added a TODO to fix a test.
4acfbc3 Guessing the last non-working test.
67c0647 Comment out some failing tests.
00ec51d Add a test for the test helper.
7553189 Fix off-by-1 error.
79a86e5 First attempt to fix the tests.
a47ee6b Allow signals to interrupt other signals when implicitly enabled.
3956c08 Merge pull request #715 from virgil-serbanuta/simpler-faster.signals-on-signals-when-explicitly-enabled
c056790 Merge branch 'simpler-faster.signals-on-signals-when-explicitly-enabled' of github.com:virgil-serbanuta/rv-predict into simpler-faster.signals-on-signals-when-explicitly-enabled
52b54fc Allow signals to interrupt signals when explicitly enabled.
b2725b4 Merge pull request #711 from virgil-serbanuta/simpler-faster.signals-on-signals
fb24b4b Merge pull request #712 from virgil-serbanuta/simpler-faster.variable-address-for-symbolization
9bee2ea Fix the Z3Filter.
43f0faa Allow signals to interrupt signals when explicitly enabled.
017cb73 Stop reading location metadata for compact traces.
4fb7587 Merge remote-tracking branch 'fork/simpler-faster.signals-on-signals' into simpler-faster.signals-on-signals
0a2ae19 Stack traces for interrupted threads.
9405f34 Add square brackets around variables.
0311b8d Merge pull request #710 from virgil-serbanuta/simpler-faster.frame-address.fix-npe
e269505 Merge branch 'simpler-faster.frame-address.fix-npe' of github.com:virgil-serbanuta/rv-predict into simpler-faster.frame-address.fix-npe
02e4847 Fix review comments.
75217bd Rename dictionary -> jargon.
539e656 Start a jargon file, beginning with DWARF CFA.
1e43228 Stack traces for interrupted threads.
e35e8db Merge branch 'simpler-faster' of github.com:/runtimeverification/rv-predict into simpler-faster
02476f8 Add a basic manual for installing and using RV-Predict.
3cf2218 Build the Java parts more reliably, I hope.
8e22f5f Remove merge brokeness
edc40d4 Add some tests that I forgot
276e3d3 Optimized the rv-predict code.
0e1767a Recurrent pattern tests.
b71e344 Fixed thread IDs starting at 0 bug.
3357132 Fix recurrent event handling.
ab10f6d Remove TODO.
670de00 Debugging changes.
5a7ae5e Undo DataAddress for optimization purposes.
c3f0526 Fix the broken Java analysis.
e95eba2 Lots of bug fixes.
966b59e small fixes.
b37d443 Code cleanup.
06661a9 Bug fixes and read/write signal masks.
ce6a012 Fixed David's example.
eed9fda Start/join signal restricts.
18bfa94 Started to restrict signals to the thread runtime.
3ca98b7 Fix trace reading issues.
2c39bbd Detect signals racing with the interrupted thread.
7e1ffa9 Race detection between non-interrupted signals and other threads.
c216500 Updated the context tests to check signal depth handling.
a9b70a8 Make the thread type available in loaded traces.
03536ce Some tests and a small fix for TraceCaches that start with a signal exit event.
4652d2f Some files I forgot
25dcc4b Lots of bug fixes.
f107031 Change the enter function reader to read CFAs.
2f4288c Removed signal mask addresses.
3fb5e0b small fixes.
d49f95f Code cleanup.
1917336 Test for set/getset.
e6dc595 Bug fixes and read/write signal masks.
6b2ed21 Fixed David's example.
62993b5 Start/join signal restricts.
de7d47b Started to restrict signals to the thread runtime.
48efdee Fix trace reading issues.
dc5f66f Fixed tests and one small bug.
32dcb70 Add a test for the maximal causal model.
521e2e3 Detect signals racing with the interrupted thread.
6257d7b Race detection between non-interrupted signals and other threads.
55cc48d Signal documentation update.
eb29d68 Updated the context tests to check signal depth handling.
e9d9579 Make the thread type available in loaded traces.
6a833fb Add some tests that I forgot
9799dc2 Optimized the rv-predict code.
2389f76 Recurrent pattern tests.
6812a0d Fixed thread IDs starting at 0 bug.
4420a37 Fix recurrent event handling.
8f35700 Remove TODO.
1961e7e Debugging changes.
1bc7b44 Merge branch 'simpler-faster.frame-address.fix-npe' of github.com:virgil-serbanuta/rv-predict into simpler-faster.frame-address.fix-npe
6f57ca1 Undo DataAddress for optimization purposes.
991883e Fix the broken Java analysis.
9e9479b Straggler from last: slightly modify program counter output to suit rvpsymbolize.
ed56f76 Make rvpsymbolize compatible both with 'symbol-friendly' rvpdump output and output from the RV-Predict analysis backend.
27bffc5 Delete a commented-out line.  No functional change intended.
6199697 Make git ignore .*.swp.
990f0ce Make rvpsymbolize use rvsyms -r.  Make a couple of regexes select a wider range of hexadecimal numbers.
847fb1f Remember a subprogram DIE's instruction pointer range on the stack, and use it to filter descendant variable DIEs.  Now I get just one result instead of a handful of results when I query a local variable belonging to main() in rv-predict-c/examples/demo/lpcq.  Reset the CFA offset when popping the DIE stack.
987e25a Merge branch 'simpler-faster.frame-address.fix-npe' of github.com:virgil-serbanuta/rv-predict into simpler-faster.frame-address.fix-npe
2b818fc Some files I forgot
fec35ff Lots of bug fixes.
af1255e Change the enter function reader to read CFAs.
18ec12f Removed signal mask addresses.
785f670 small fixes.
de68344 Code cleanup.
0aa35f9 Test for set/getset.
9be8d1a Bug fixes and read/write signal masks.
77603fd Fixed David's example.
946f9ba Start/join signal restricts.
2fed595 Started to restrict signals to the thread runtime.
b3854e5 Fix trace reading issues.
ea5de6c Fixed tests and one small bug.
967dfd3 Add a test for the maximal causal model.
1d98880 Detect signals racing with the interrupted thread.
3098904 Race detection between non-interrupted signals and other threads.
ac64a18 Signal documentation update.
81a4852 Updated the context tests to check signal depth handling.
b5492de Make the thread type available in loaded traces.
af57769 Wrap lines.
e84df19 Reduce window to 2000 to match what Virgil uses.
df5de78 Add an option flag, -r, that prints addresses as regular expressions, which is useful symbolizing traces and data-race reports.
ac5531b Log function entry/exit using a program counter in the function we entered instead of a program counter in the caller.  This helps with symbolizing stack variables.
af635a6 Some tests and a small fix for TraceCaches that start with a signal exit event.
29c2383 Some files I forgot
e5f150c Lots of bug fixes.
05e381e Merge branch 'simpler-faster' into simpler-faster.frame-address
bd7b93c When -t symbol-friendly is given, write out program counters in {} for rvsyms to parse.
64ad265 Make mkcmake(1) descend into ouat/test/.  Make Git ignore a bunch of build products in ouat/test/basic/.
f616fbd Add a new output type, 'symbol-friendly', that prints the program counter & DWARF Canonical Frame Address (CFA) for 0, 1, or 2 frames that an address may belong to.
2757248 Change the enter function reader to read CFAs.
d96c8dc Look for nbcompat.h in include/.
6286e64 Look for nbcompat.h in include/.
54bd255 Do not ascribe data members to *pointers* to structs.
1360908 Quiet unused variables warnings.
0c2ac35 Get started on a basic test of the symbolization.
41accb1 Removed signal mask addresses.
f7ef159 small fixes.
6700bfa Merge branch 'simpler-faster.signals-modelling-restricts-1' of github.com:virgil-serbanuta/rv-predict into simpler-faster.signals-modelling-restricts-1
a1ff4ff Code cleanup.
71cc846 Test for set/getset.
a202636 Bug fixes and read/write signal masks.
ccf60cc Fixed David's example.
b390abb Start/join signal restricts.
46f4606 Started to restrict signals to the thread runtime.
089a074 Fix trace reading issues.
7237f0c Fixed tests and one small bug.
b2adff7 Add a test for the maximal causal model.
811e498 Detect signals racing with the interrupted thread.
c2bf7d2 Race detection between non-interrupted signals and other threads.
57dbe18 Signal documentation update.
6af4a97 Updated the context tests to check signal depth handling.
09b53d0 Make the thread type available in loaded traces.
e48d93f Wrap lines at 80 columns.  No functional change intended.
d712cb8 Run the Maven build dead last.
3465692 Re-enable optimization (-O3).
6171e69 Make git ignore tags-related build products.
8f90947 Make git ignore `tags`.
2e6d21f Quiet warnings about non-void-* arguments to %p.
24f9a6a Quiet warnings about unused parameters and the backslash escape I used in those sscanf formats---why did that seem necessary?
8b3fdc3 Ignore tags-related build products.
b2f9e62 I'm moving "CPPFLAGS+=-Wuninitialized -Wunused-parameter -pedantic" to my mk-c.conf.
d094711 Quiet unused-arguments warnings.
7cc463c Use __unused on purposefully unused arguments.
ba846c6 Where I intended not to use an argument, quiet warnings with the __unused attribute.
f71c232 Reactivate optimization (-O3) and turn on aggressive warnings that I will suppress in a subsequent commit.
1374c49 Commit straggler: I forgot to bump the version number to 0.0.0.2.
f4d3179 Bump the version number to 0.0.0.2.
8c5d457 Describe the DWARF Canonical Frame Address that's passed in the latest trace format.
0febf7e Flesh out the atomic-instructions instrumentation.  Add some new stubs, too.
2aec00c Symbolize array indicies within struct members.
7b93130 Analyze the trace even if the program was cancelled with an error. TBD tell the user that they can signal again to cancel the analysis.
c71ba1c Update the type signatures of some atomic instrumentation.
2ee176f Move the RV-Predict scripts to their own directory and add the nascent runtime tests.
7c8dbff Make the runtime and rvpdump write and read more atomic-load and -store events.
3b360fb Remove an extraneous space from the held-locks report in the data-race report.
6a480bb Start to bring the format of data-race reports into line with previous proposals.
4fbc3da Add the address of the signal handler to the `enter-signal` event. Change the specification of the version number from a 32-bit integer to 4 bytes telling major, minor, teeny, and tiny.  Increase the version number from 0.0.0.0 to 0.0.0.1 to poison trace readers who don't understand the new format of the `enter-signal` event.
49b288a Make make(1) descend into ouat/.
5c2b9b3 Fix a couple of typos.
0e469a0 In rvpx, quiet the `ls` invocation that looks for (possibly absent) core files.
2450a45 Make mkcmake(1) descend into test/.
072adb5 Commit a straggler: provide type definitions for read-modify-write events.
63e6638 Make Git ignore `tags`.
a5739be Make Git ignore a file called `core`.
de1570c Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
e2e2efb Add a flag '-a' that makes rvsyms print the program counter / data address that had looked for.  This is useful for joining symbols with other data in scripts.
f488602 Add to rvpdump enough understanding of read-modify-write events to avoid exiting with an error when they're encountered.
e6d6a37 Use the right idiom for creating a symlink.
1c02db2 When -M* is on the command line, don't pass -L/-l options to clang, it will complain.
77aea39 Merge pull request #705 from virgil-serbanuta/simpler-faster.signals-documentation
dbc262b Small clarifications.
6ec3ae1 Merge pull request #701 from virgil-serbanuta/simpler-faster.set-ips
948c8e8 Merge pull request #704 from virgil-serbanuta/simpler-faster.fix-tests
d65d0e2 Fixed small problems in the documentation.
d5b761c Explain why we may need to run the same signal multiple times.
6491cc9 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
e4da89c Make git ignore *.d and .depend.
96fc84a Merge branch 'simpler-faster' into simpler-faster.signals-documentation
4187acb Merge pull request #703 from virgil-serbanuta/simpler-faster.signals
8f47db3 Rewrote a small part of the doc.
6674822 Add strstack_depth() that returns the current depth of a string stack.
01ad4d6 Don't install walker, it's just for my DWARF development & experimentation.
838e2ad Don't install stackstruct, it's just a program to test rvsyms against.
0d0952b Make git ignore *.d, .depend, and *.ll.
c15f9c8 Make git ignore *.d and .depend.
20164f7 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
c7b6321 Break lines.
7bb8ae3 Fixed small issues fordocumenting signal race detection.
5b68348 Documenting the signal race detection, basic idea.
e3d03b1 Fixed one more test.
8319141 Small test comments and fixes.
f06ccb6 Fixed the llvm.demo.example2 test.
d2a2d86 Fix inconsistencies.
a934d35 Added signal events.
db397c9 Debugging changes.
51587c1 Merge pull request #702 from virgil-serbanuta/simpler-faster.fix-decorator
67b04f8 Decorator fix.
2e63249 Rollback unrelated changes
8a1970d Actually add the tests.
921a314 Fixed some minor issues for invalid PCs in compact events and added a test.
4ddc44b Merge pull request #700 from virgil-serbanuta/simpler-faster
21a43e1 Fixed the native z3 version for the rv-predict-source pom.
ce92eed Merge pull request #698 from virgil-serbanuta/simpler-faster.turn-on-compact-trace
0983031 Fix one test.
f694d25 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
a07cba5 Merge pull request #699 from virgil-serbanuta/simpler-faster.fix-issue-263
5c2a6e2 Fix issue #263 and maybe also #262.
ea2fbfd Removed unneeded diffs in TraceCache.
96b46a7 Removed unneeded diffs in TraceCache.
67eb216 Removed unneeded diffs in TraceCache + fixed indentation.
7c6eb33 DeltaAndEventType test
5ddd4b8 Test exceptions for the CompactEventReader.
4a96a35 Assert exception refactoring
95201ed Fixes for merging + Compact event reader eof exception
f968a04 Merge branch 'simpler-faster' into simpler-faster.turn-on-compact-trace
fc67d88 Merge pull request #697 from virgil-serbanuta/simpler-faster.update-signals
7213ff5 Update the sig_depth comment to match the c++ one.
6804c03 Compact event reader test.
4f132e8 Actually read event headers.
b807541 Make the trace cache read compact events.
c4b4539 Allow the trace cache to read compact events.
a3c95bc Fixed the new reader tests to check factory method invocations.
808619f Formatting fix for the GetSetSignalMaskReaderTest.
aa0ab34 Add a test for BlockSignalsReader.
be07730 Add a test for GetSetSigtalMaskReader.
39fc9ab GetSignalMaskReaderTest fix.
a3f9a09 Remove unneeded variable in the UnblockSignalsReaderTest.
c6ab8b5 Test for the GetSignalMaskReader.
23be26e Test for the UnblockSignalsReader.
8e30868 GetSignalMask
9e38194 GetSetSignalMasks
8b3a040 Remove remnants of the prototype for `rvsyms`, `walker`.  Move state from global variables to the dwarf_walk_t so that reusing this code as a library will be easier.
7f64979 Add a multidimensional array that I can test rvsyms against.
edbe9bc Unblocking signals.
ad21ff8 Blocking signals.
72bead6 Blocking signals.
4953213 Renamed the SignalOutstandingDepth and MaskSigs events.
f1bba1a Merge pull request #696 from virgil-serbanuta/simpler-faster.merge-events
c8d32bf Extract a subroutine, rvp_change_sigmask(), for both sigprocmask and pthread_sigmask to use.
99e502c Make git ignore `tags`.
f7b18e6 s/ninstr_outst/idepth/ and make several parallel changes, s/sigoutst/sigdepth/,
ed4ccad Use a less unwieldy name for the depth of signal/interrupt handlers on the current thread, s/_nintr_outst/_idepth/.  Make some parallel changes such as s/noutst/idepth/, s/sigoutst/sigdepth/.
90a62e5 Fix a bug where I was not assigning a signal to each statically-established interrupt.
41e0c35 Oops, straggler to last.
eaeb4bb Try to report an error when an interrupt annotation is malformed.  Alas, instead of reporting, our pass crashes.  Looks like there may be an LLVM bug, fixed in versions later than 3.8.1, that causes the crashes.
7876e3c Update trace specification.
63e22d5 Use clang only if CC is not already set to something else.  Don't strip binaries when installing them.  Use COPTS instead of DBG, since DBG isn't really understood by mk-configure.
3e5a65b Made the compact event extend the ReadonlyEvent.
87c9f1d Extracted a ReadonlyEvent class that can be used both as an old event and as a CompactEvent.
b8f7516 Delete unneeded comment.
ae51361 Merged event types
f9e4366 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
01667de Merge pull request #692 from virgil-serbanuta/read-compact-trace-simplified-context
cc64daf Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
0b22383 Merge pull request #693 from virgil-serbanuta/fix-jenkins
080adb9 Get arrays to symbolize.
a73f14f Add a local array for me to symbolize with rvsyms.  Print the address of `cfa`.
851dc7c Reset the signal depth when switching threads.
7a4665a Undo unneeded diffs.
5bef4a1 Add an argument to rv-predict.
27e39d0 Undo unneeded diffs.
a5051ae Closer to working tests.
684b7eb Fixed bash if branches.
78ed566 Fix the bin and lib paths for Jenkins tests.
ac77b15 Merge branch 'simpler-faster' into read-compact-trace-simplified-context
db65ae4 Add some code for naming struct members.
1d41765 Add some nested structs to my stackstruct program so that I have some nested struct members for `rvsyms` to find.
9f23030 Fix the trace specification.  I'm not sure what I was thinking: a reader shouldn't push or pop anything.
289a00b Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
f1c2cfe Remove unneeded class.
ee7d533 Finished tests.
ae1ec3e More tests for the context
f1c2083 The implementation is almost done, also some tests.
23ffbe3 Merge pull request #690 from virgil-serbanuta/read-compact-trace-factory
24f3340 Temp changes.
674cd77 In the runtime, when a thread begins, and when a signal is entered, set its ring's last PC to the central deltop, (0, 'begin'), so that the runtime is forced to emit a 'jump'.
141e6ab Make rvpc run clang++ instead of clang when it is invoked as rvpc++. Install a link from rvpc++ to rvpc.
eef8d54 Add #definitions for __printflike and __scanflike from NetBSD.
30316d0 Derive, from `walker`, `rvsyms`, a program that takes a data address and optional frame and instruction pointers to a symbol name.
262012a Empty line at the end of the file.
a5dd632 Added a test for the CompactEventFactory.
11d6a58 Merge branch 'simpler-faster' into read-compact-trace-factory
00e37ad Merge pull request #687 from virgil-serbanuta/fix-classpath (#689)
575aa24 Merge pull request #688 from virgil-serbanuta/read-compact-trace-readers
d81884d Use __builtin_dwarf_cfa() instead of __builtin_frame_address().
31d76bf Make this really simple, and use __builtin_dwarf_cfa() instead of __builtin_frame_address().
97c20a7 If CC is not already set, set it to clang.
de11289 Improve walker's comprehension of Canonical Frame Addresses (CFAs).
a562234 Implemented the compact event factory.
906545f Split the CompactEventReader, extracting an event factory.
3b1a84c Improved comment.
3f8d8b0 Merge pull request #686 from virgil-serbanuta/read-compact-trace-readers
c16bbdd Removed some lint errors.
a54fd56 Refactored all readers.
7c39f47 Test refactoring.
38525a7 Add a test for ThreadSyncReader
ff1f96d Add a test for ThreadBeginReader
8f510c7 Add a test for SignalOutstandingDepthReader
8f075e8 Add a test for SignalMaskReader.
b362510 Add a test for SignalMaskMemoizationReader
0107384 Add a test for SignalEstablishReader
a88d8be Add a test for SignalEnterReader
732ec06 Add a test for SignalDisestablishReader
2c2cc55 Add a test for NoDataReader
71c9d50 Add a test for the LockManipulationReader.
548c7ae Add a LazyInitializer test.
05baf95 Add a DataManipulationReader test.
4c5bfee Test for the AtomicReadModifyWriteReader. Readability improvements for the ChangeOfGenerationReaderTest.
34a9b1e Fix the ChangeOfGenerationReaderTest imports.
cd6b03d Moved the ChangeOfGenerationReaderTest to the right package.
df8c373 Change of generation test.
681109c Change of generation test.
18e6b08 Fixed compile errors with stub methods.
8a3a89e Some of the files needed for the readers.
626acb4 The readers, still missing some files.
f0f204b Merge pull request #685 from virgil-serbanuta/read-compact-trace-data-types
5804edc Added the base data types and their tests.
fb80d31 Initial data types, without the classes they need.
43852cc Fix two documentation bugs that Virgil detected.
535bfa7 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
52495b9 Take a snapshot of my work in progress: add to `walker` options for filtering by data pointer (-d ptr), instruction pointer (-i ptr), and stack frame base address (-f ptr).  Make `stackstruct` a little bit more useful as an example to run `walker` on.  Make git ignore more files in walker/.
f4f30fd Merge pull request #683 from virgil-serbanuta/simpler-faster-cp
d2d002a Merge pull request #682 from virgil-serbanuta/no-recursive-logging
901de23 Merge pull request #681 from virgil-serbanuta/claim-gid-deadlock
b4133e7 Fix a deadlock in VolatileLoggingEngine.claimGID
d1ee33a Copy the directory containing my ELF and DWARF experiments, ouat/ (short for (o)nce (u)pon (a) (t)ime), from branch integration-springboard to branch simpler-faster.
1ded237 Bring this up to date with the code.
a684f1c Flesh out the trace specification a bit.
e54a079 Start to update the trace specification.
7c01b5f Bug fix: set exitcode to $? not $!, because $? is the last pipeline's exit code and $! is the PID of the last background process started.
ee382ba rvpsymbolize --pc <program> converts program counters (PCs) on <program>, and rvpsymbolize --ptr <program> converts data pointers.
74f6572 Make git ignore build products, *.copy.
c9dfe17 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
93dad51 Emit the right 64-bit ID to help *slightly* improve symbolization of data addresses.  Now the backend will emit [0x......] (right: a hexadecimal address) instead of something silly about an "array element #...".
bcba830 Add a top-level makefile that builds everything we need for RV-Predict[C], including the .jar file.
d8fe0ad Look in $RV_ROOT (or /usr/local if RV_ROOT is not set) for bin/checkJava and lib/rv-predict.jar.
8ead1d4 Make git ignore _mkc_* files from mk-configure.
316a8c8 Produce a recursive build for all of the RV-Predict[C]: utilities, instrumentation pass and runtime.
5a6eca9 Look for annotations that mark interrupt handlers and produce calls from the module constructor that establish the handlers.
5bf7721 Look for RV-Predict libraries & binaries in RV_ROOT or, if it's not set, /usr/local/.
7b95200 Replace an anonymous number with __arraycount(...).
f5433bd Add and install intr_exports.h, which defines __rvpredict_intr_enable() and other symbols used by the DENSO interrupt simulation.  For consistent definitions, #include "intr_exports.h" in intr.c.
76fa70c Install *.sh as rvpc, rvpx, rvpsymbolize in $PREFIX/bin/.
a3febd3 Fix a minor typo.
e1fddff Merge branch 'simpler-faster-model' into simpler-faster
67d4508 Merge pull request #678 from virgil-serbanuta/simpler-faster
6bbf7ab Write information about static interrupts to stderr only if RVP_INTR_DEBUG is set to 'yes'.
74dd862 Don't delete a temporary directory if it contains core files, because usually a developer will want to look at those.
8f0265d Fix symbolization for the case where symbols contain whitespace. Sometimes C++ symbols contain whitespace.
168b218 Remove unneeded diffs
52a2da9 Merge branch 'simpler-faster' into simpler-faster-model
4988257 Remove unneeded changes.
f8ec8f5 Remove unneeded changes.
b7ee923 Remove unneeded changes.
aefeedf Make git ignore *.d and _mkc_*.
7781456 Make the compact trace reader understand RVP_OP__STORE2.
a26c1bc Link with librt for timer_create() et cetera, which is needed by the "static interrupts" hack for DENSO.
80203eb First draft of the runtime for "static interrupts".  These are interrupt handlers, indicated by the system under test using a function annotation, __attribute__((annotation(...))), that the RV-Predict runtime establishes as signal handlers.
7944a1f Make git ignroe the _mkc_* files the make(1) macro set I use, mk-configure, is stashing ... something.
d963834 Add a tasks list.  I need to add new tasks, including tasks I listed yesterday for Virgil.  Probably should move these tasks to Trello.
f935a64 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster-model
2e7fd7d Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
ec8752a MaximalCausalModel refactoring
26ae71d Wrap lines.  No functional change intended.
86ffe91 Make git ignore *.d.
9991aed Merge remote-tracking branch 'refs/remotes/fork/simpler-faster' into simpler-faster-model
c6d53b6 Add a comment that describes how/why I increase the global generation counter (ggen).
ba2148a Commit changes that hold down the size of an event generation.  This should help with the NullPointerException that Virgil gets because of an oversized window.
eb271d5 Event ordering demo.
a81fd30 Remove unneeded diff.
3cd8605 Merge remote-tracking branch 'origin/simpler-faster' into simpler-faster
ab82d4d Update the declarations for atomic read-modify-write routines, __rvpredict_atomic_{add,and,nand,or,xor,exchange,...}{1,2,4,8,16}, to match the LLVM instrumentation pass.  Thanks to Virgil for pointing out the discrepancy.
aad70a3 Fix unneeded diff.
b4d9113 Fix some type issues that crash my LLVM.
8f4dbfb Add `rvpc`, my new wrapper for compiling with RV-Predict instrumentation.
32e2aa0 Respect the generation numbers assigned by the new instrumentation.
21d1a32 When rv-predict is run with the --debug option, also tell the GIDs involved in a mismatched method entry/exit.
2ba6b22 Add a missing semicolon.  How is it that I haven't compiled this recently?
f4780c8 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
d03d877 Use rvp_addr_t instead of uintptr_t.  This may help me to build both 32- and 64-bit versions of rvpdump and the instrumentation for the same 64-bit target.
38cde0e Delete some irrelevant #if 0'd debug code and shorten the surrounding code.
2c4e829 Use mk-configure macro files.  Lower WARNS to 4 for mk-configure.
fd37b4d Use mk-configure macro files.  Compile with clang.  Lower WARNS for mk-configure, which supports up to 4.  Add a ${.CURDIR} for OBJDIR support.
4e8728d Mark usage() __dead.
8f06707 Don't symbolize my example program, lpcq, every time!  That's just silly. Instead, symbolize the first argument on the rvpx / rvpsymbolize command line.
6ba4b3d Print the generation number for a signal-entry event.
51088df Condition debug `println`s on Configuration.debug.
1b83281 Add rvpx, a wrapper for programs with RV-Predict instrumentation that runs them and performs the analysis.  It's like rv-predict-execute.
09de4b3 Update for compatibility with new traces.  Improve support for signals/interrupts.
310dd69 If a command-line argument is given, read a trace from the file it names instead of from stdin.
be397b6 Ignore build product `tracedump`.
1bb3f29 If a command-line argument is given, read metadata from the file it names instead of from stdin.
2fdf877 Signals track the generation number independent of the threads they interrupt: take care to get that right, especially by logging the current generation number in an 'enter-signal' event.
8b62cee Cosmetic: delete whitespace at EOL.
83f8e26 To request ring service in a signal handler, don't signal a condition variable,, that's not allowed.  Instead, send a signal to the relay.
3b1b1d0 Don't sched_yield(2) in a signal handler, it's not allowed.
86cd16d that do not return.
d5abe91 Application signals had better not run in the relay thread, it isn't instrumented.  Block all signals in the relay thread.
6bb7556 Merge branch 'simpler-faster' of github.com:runtimeverification/rv-predict into simpler-faster
dbd7343 Add some AtomicOrdering:: qualification, and #include the right header for AtomicOrdering.  Not sure why this isn't a problem on Linux, but it is on NetBSD.
29cfd4b Quiet complaint about redundant typedef.  Quiet comlaints about comparing signed w/ unsigned.
92db875 Make the compatibility #definitions conditional on !defined(__NetBSD__). Is __NetBSD__ the right #define, though?
89787ac Mark not_implemented() __dead.
1db0eef Don't try to build a manual page on NetBSD.
6a1d72f Quiet compiler complaints that a typedef is duplicated. Quiet complaints about comparisons of signed and unsigned.
2c149ec Mark usage() __dead for NetBSD.
8e7b260 Ignore more build products.
5f97317 Ignore some build products that appear on NetBSD.
54daece Flesh out signals/interrupts support and fix a bunch of bugs. Improve the compact trace -> legacy trace conversion.
b230a36 Add a program for printing the legacy traces.
6104e90 Accommodate GIDs that are not compact, like the GIDs generated by compact -> legacy trace conversion.  These changes should be compatible with the legacy instrumentation for C, but I need to check.
3ba55fb Add a utility program, metadatadump, that prints a metadata file from a legacy trace.
8bdc4cc Make git ignore some build products.
5edc586 Add instrumentation for establishing, disestablishing, masking, entering, and exiting signal handlers.
ad8c7fd Add some test programs for UNIX signals behavior.  Really I should run these on a few POSIX systems and compare.  Also, I should move these to a different directory, but here they are....
0c9be4c Rename signal.[ch] to rvpsignal.[ch].  Interpose __rvpredict_sigaction() for sigaction(2).
73ea1f9 Make rvpdump understand signal entry/exit.
23fc297 In sigeqset(), skip over leading invalid signal numbers before starting to compare members of `l` and `r`.
5c2bc2f Take a snapshot of my work in progress.  This snapshot will probably not compile, sorry.
cec2ace Log the same program counter for function entry and for function exit, since the analysis backend expects that symmetry.
ae545c3 Optionally re-emit as "legacy" trace.  This is a work in progress.
fbbc5ba Update the legacy operations.
1190fa0 Define the operations used by the "legacy" LLVM instrumentation.
be7094a Join a line.  No functional change intended.
1f37d91 Log change-of-generation (COG) events.
6e3649a Turn up optimization level from -O0 to -O3.
aa5e436 Stragglers from last commit: use the dynamic linker to interpose our pthread(3) stubs, __rvpredict_pthread_*.
2bc80f3 Use the dynamic linker to interpose our pthread(3) stubs, __rvpredict_pthread_*.
d091f5a Fix indentation of a comment.  No functional change intended.
d29a473 Group the pthread-wrapping routines at the end of thread.c.
452afdf Extract subroutine rvp_ring_put_buf() and reuse.
f87c909 Advance the ring-buffer producer pointer over an entire trace at once, don't dribble them in.  As expected, this seems to fix the problem with 'switch' traces.
70b6855 Share some trace typedefs between ngrt and rvpdump.  I thought that ngrt would use the typedefs, but probably not.
43e21ac Make git ignore .depend.
cb8a82c Use __builtin_return_address(0) everywhere that I used __builtin_return_address(1), before, since the former is what I meant.
abb9490 Look for the pass and runtime at $RV_ROOT/rv-predict-legacy/ instead of $RV_ROOT/rv-predict/.
79ad3ca Call __rvpredict_ stubs for pthread_exit, pthread_mutex_{lock,trylock,unlock}.
cea222c Increase WARNS to 5.  Not sure that increases make any difference after 4, I sure didn't see any.
8ef0a0a Remove a duplicate definition for the 'atomic-store' op.
abe0ccd Fix synchronization between rvp_wake_transmitter() and serialize(). Previously, serialize() prematurely stopped emptying ring buffers, so some rings would block forever.
113b6a9 Make git ignore .*.swp.
526dcc5 Add my work in progress on the simpler, faster runtime to llvm/ngrt/. Adapt the instrumentation pass in llvm/pass/ to suit.  In doc/, add the trace format specification and some RV-Predict[C] discussions.
0ee8312 Mention ngrt/, the simpler, faster runtime.
4764ce5 Here is a branch for the slightly delayed DENSO deliverable of 16 Dec 2016, with the RV-Predict backend of March 2016 and the LLVM frontend (instrumentation pass + runtime) of 16 Dec 2016.
f1b5670 Ignore library symbols belonging to objects in /usr/bin/../lib/.  That's an alias for /usr/lib/ that appeared in the path to the GNU C++ standard library was showing up.
c3db484 Make rv-predict-execute run "$@" instead of $1 so that I can pass parameters to a program run under RV-Predict analysis.
02f6f8e Addressed comments
733106a Removed EventType extra import
f0e9c88 Another small rollback
5df39e1 Small rollbacks
4fe9b49 Refactored and improved precision.
59d04ce Repatching Issue #656
52a34e3 Merge pull request #658 from edgar-pek/master
231d86f Merge branch 'master' of https://github.com/edgar-pek/rv-predict
8d71db8 minor fixes and renamings
ebe20ca minor fixes and renamings
2166d2d Merge pull request #657 from runtimeverification/issue-653
e1abf04 Added a TODO about llvmThreadCreationEvents
68ecfff Merge pull request #654 from runtimeverification/issue-653
d57fcc2 Addressed comments and added test.
b04516e Patch for Issues #655 and #656
f8dfdb7 mproved thread and lock reports.
bc0bed8 Patch for Issue #653
473366b Merge pull request #651 from edgar-pek/master
7ccab97 made the name more intuitive
1b32c1d Merge pull request #650 from runtimeverification/tracking-fork
95cc8f1 Added FORK event. No handling yet.
b5467f8 Merge pull request #648 from runtimeverification/max-vars
c644917 Bumped max # of vars to 1024*1024
6de9b20 Merge pull request #645 from runtimeverification/brief-stacks
2ca71aa Reporting library locks at user level.
95a6262 Properly reporting atomic lock/unlock. simplify
c44959b Simplified file paths and updated tests.
59fbe13 Added JavaDoc
9b4b4dc Refactorings.
a77ca47 Merge branch 'master' into brief-stacks
057da42 Merge pull request #644 from runtimeverification/fix
c61a4ec Fix when exceeding number of variables.
504ecd9 Merge pull request #643 from ericpts/master
549d5b4 Updated race processing to reflect LLVM changes
2d0df4d Merge pull request #642 from ericpts/master
f4d8269 Updated the llvm script
594cfa6 Merge pull request #634 from ericpts/master
a78c843 Merge pull request #641 from runtimeverification/atomics_prelock_fix
8c0d1fc Fix for lock events not generating prelocks.
b500eb2 Merge pull request #640 from runtimeverification/deadlock-predetection
1227bd6 Added TODO for moving PRE_LOCK with sync events.
68030e9 Merge pull request #639 from runtimeverification/deadlock-predetection
7ffd304 Added documentation for the PRE_LOCK event.
d059cba Merge pull request #638 from runtimeverification/deadlock-predetection
fae91d3 Disabling deadlock prediction for Java for now.
38f2f73 Deadlock pre-detection, backend part.
3c0e0da Merge pull request #635 from edgar-pek/master
bc193c0 handling the case when calling unlock on an non-existing lock
b7d4fc1 Fixed bug when handling C files
b836b51 Merge pull request #633 from ericpts/master
efe285a Added compile script
9c318ed Merge pull request #621 from edgar-pek/master
58aa792 Merge branch 'master' of https://github.com/edgar-pek/rv-predict
d6a4d51 Merge pull request #2 from runtimeverification/master
943c6a1 Merge branch 'master' of https://github.com/runtimeverification/rv-predict
f1ec899 fixed the reversed order of traversal returned from the SCC computation inside the deadlock detection
483792c Merge pull request #626 from ericpts/master
cad47d4 Merge pull request #1 from runtimeverification/master
fcb68a2 Merge branch 'master' of https://github.com/runtimeverification/rv-predict
91c49c1 Fix for C programs not returning 0
6be1add Merge pull request #624 from runtimeverification/deadlocks
ceb74a9 Updated deadlock output and test.
5846c54 Refactorings
e4b3460 Almost working (modulo tests).
9fff716 changed line endings to make it readable in Notepad
049b7a8 Added deadlock example to integration tests
4111acb Reorganized code and added test
c117f27 Mimiquing TSan output.
93c89b0 Fixed initialization
4456a4c First attempt at deadlock detection.
1f48108 Merge pull request #581 from runtimeverification/newLicensing
8430c63 README.md updated to reflect changes in the directory structure
77e4380 refactor examples/examples to examples/demo
4da3532 Added test for detailed stack frame
6481cf2 Started patch for rv-predict-c
9012e52 Merged two executions
e400c64 Merge pull request #619 from edgar-pek/master
9e2e6a5 remove PATH note in the uninstall instructions
06b26ea Using correct Agent resource path
71c7c26 Fixing proguard warnings
14ec3f8 minor modification to the uninstall note
a21504e add uninstall note
c07a525 Merge pull request #612 from yilongli/hotfix
13e8eeb Merge branch 'master' into hotfix
47367ee Merge branch 'master' into newLicensing
18913ed Merge pull request #618 from runtimeverification/merging-sources
e6650e8 Addressing @yilongli's comments
a18378b Merge branch 'merging-sources' into newLicensing
2c446e0 Merged agent and logging into rv-predict-source.
a7e5121 Merge branch 'master' into newLicensing
0fdd016 implemented a naive pretty printer for metadata.bin
460ea23 extracted lz4 related code to a separate utility class and compressed metadata
6b9c65d added option --log-dirname and revised the documentation
cd1fb8e Merge pull request #611 from ericpts/master
1b5fe7c Modified rv-predict-llvm script to reflect changes
b02f9c2 change installer size for usability
6a35fef upgrade to rv-install 1.1
8e59dc7 move license info printing to end of version, help, and don't print when errors occur
3a94eeb (auto)update license, update license path to new predict jar path, increase height for offline text in installation panel
84d21a5 Merge pull request #610 from yilongli/fix-DumpLogFile
2e11df5 a little bit defensive check to avoid potential ArrayOutOfBoundException…
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants