Semantics of C in K
C OCaml Perl C++ Shell Makefile Other
Latest commit 794f017 Mar 24, 2017 @dwightguth dwightguth committed on GitHub Enums + Enumerators (#413)
* Squashed 'c-semantics/' changes from f8e7068..46628b2

46628b2 Small patch for #fun compilation (#407)
2ecd8fe More restrict check tweaks. (#404)
c95b335 various minor fixes for classes (#406)
80b1724 Unions 2 (#405)
584fa6f add rudimentary error reporting back to open source semantics (#403)
bd15701 Enumprep2 (#401)
7de6ef2 Restrict refactoring. (#358)
cf8be6e Revert "Revert "overloading operators + default constructor + misc fi… (#400)
d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix kframework/c-semantics#269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge kframework/c-semantics#266 (#387)
d989a4f Merge kframework/c-semantics#265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes kframework/c-semantics#264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: 46628b2

* Squashed 'c-semantics/' changes from 46628b2..8b1ddf2

8b1ddf2 Merge remote-tracking branch 'c-semantics/master' into HEAD
0e30e73 Minor fix
2ff8bc8 Forgotten rule
99d1031 Remove ite
adb2fca Fixes
4af078c Enums: various fixes
f68697d UNSPEC
ffbcca9 getAsocNs for enum
1e2724e Enumerator lookup.
cc93394 Check value of enumerators with fixed underlying type.
135aeff Enumerators
ee6cbfd Enums: conversions and promotions
9052eff Enums.

git-subtree-dir: c-semantics
git-subtree-split: 8b1ddf2db4d83c8e91317df5bb60606562ab2931

README.md

See INSTALL.md for installation instructions and LICENSE for licensing information.

If this readme isn't enough, consider checking out these papers to better understand this project:

Quick overview

  • kcc is meant to act a lot like gcc. You use it and run programs the same way. If your system provides a command kcc already (of which there are several possible), we also provide the synonym kclang.
  • The programs kcc generates act like normal programs. Both the output to stdout (e.g., printf), as well as the return value of the program should be what you expect. In terms of operational behavior, a correct program compiled with kcc should act the same as one compiled with gcc.
  • Take a look at kcc -h for some compile-time options. For most programs, you only need to run kcc program.c and everything will work.
  • After compiling a program and generating an output file a.out, the resulting program is a native executable and can be run on any platform provided it has access to the runtime libraries required by the dynamic linker.
  • If you try to run a program that is undefined (or one for which we are missing semantics), the program will get stuck. The message should tell you where it got stuck and may give a hint as to why. If you want help deciphering the output, or help understanding why the program is undefined, please send your final configuration to us. If you are using default settings, this configuration is located in the file config in the current directory if the program got stuck while executing, or can be generated using kcc -d in case of compile-time errors.

Runtime features

Once kcc has been run on C source files, it should produce an executable script (a.out by default).

Testing the semantics

The tests directory includes many of the tests we've used to build confidence in the correctness of our semantics. To run the basic set of tests, run make check from the top-level directory. For performance reasons, you may first wish to run kserver in the background, and pass a -j flag to make to get the desired level of parallelism.

A note on libraries

KCC comes by default with relatively limited support for the C library. If you are compiling and linking a program that makes use of many library functions, you may likely run into CV-CID1 and UB-TDR2 errors, signifying respectively that the function you are calling was not declared in the appropriate header file, or that it was declared, but no definition exists currently in the semantics.

We recommend if you wish to execute such programs that you contact Runtime Verification, Inc, which licenses a tool RV-Match based on this semantics which is capable of executing such programs by linking against the native code provided on your system for these libraries. For more information, contact https://runtimeverification.com/support.

Project structure

Directories:

  • examples: some simple example programs for demonstrating the undefinedness that we can catch.

  • x86-gcc-limited-libc: library headers and some library sources for functions that aren't defined directly in the semantics itself.

  • parser: the lightly modified OCaml CIL C parser.

  • scripts: e.g., the kcc script and program-runner, the script that becomes a.out.

  • semantics: the K C semantics.

  • tests: undefinedness, gcc-torture, juliet, llvm, etc.

  • dist: created during the build process, this is where the final products go. For convenience, consider adding this directory to your $PATH.

During the build process, three versions of the semantics are built using kompile with different flags: a "deterministic" version, a version for supporting non-deterministic expression sequencing, and another with non-deterministic thread-interleaving. These all get copied to dist/ along with the contents of x86-gcc-limited-libc/include and the scripts/kcc script. Finally, make runs kcc -s -shared on all the libc source files in x86-gcc-limited-libc/src.

The kcc script is the primary interface to our semantics. Invoking kcc myprogram.c results in the contents of the parameter C source file being piped through, consecutively:

  1. the GNU C preprocessor, resulting in the C program with all preprocessor macros expanded;
  2. the CIL C parser (cparser), resulting in a KAST term;

The root of this AST is a single TranslationUnit term, which is then interpreted by our "translation" semantics.

See semantics/c11/README.md for more details.