kframework / c-semantics Goto Github PK

View Code? Open in Web Editor NEW

302.0 302.0 39.0 20.71 MB

Semantics of C in K

License: Other

Perl 4.89% C 74.19% C++ 6.92% Makefile 1.91% OCaml 10.63% Shell 1.21% CMake 0.12% Dockerfile 0.11%

c-semantics's People

Contributors

Stargazers

Watchers

c-semantics's Issues

Error codes should be made uniform

@msaxena2 , as we discussed, the error codes of the C semantics should be made uniform. For, they should all start with a capital letter. Can you please go ahead and do this change as soon as you get a chance?

test-build failing

The test-build target fails trying to run the test program because - is apparently no longer supported as the name of the input file:

make[1]: Leaving directory '/home/brandon/code/k/c-semantics/semantics'
Testing kcc...
printf "#include <stdio.h>\nint main(void) {printf(\"x\"); return 42;}\n" | dist/kcc - -o dist/testProgram.compiled
Unsupported option - at dist/kcc line 333.
Makefile:65: recipe for target 'test-build' failed
make: *** [test-build] Error 255

semantics of *scanf?

I could not find a semantics of *scanf functions. Are there some fundamental reasons why those are currently not supported?
I am asking because it would be cool if the semantics could handle examples below
https://sourceware.org/bugzilla/show_bug.cgi?id=12437
https://sourceware.org/bugzilla/show_bug.cgi?id=12701

Applications of K in systems lacking the ability to run K.

C often finds usages on systems that lack the ability to run anything else. Running K on such systems is often not an option. There can be many reasons behind this: for instance, lack of a compatible JVM, or just lack of resources to run a rather large application like K (I haven't tried running K on a small system like the Raspberry Pi, but it'll be interesting to see what the performance is like). C code running on such systems is often available though, and it'll be interesting to see whether we can run the code on K running on a completely separate system. Since the code would not be executing on the machine itself, we'd mostly be lacking the ability to perform any sort of concrete execution. However, symbolic execution of the code may be possible. @andreistefanescu and I were able to verify several programs withing the SV-COMP testbench by performing symbolic execution. The programs in the testbench however, were much simpler than the kind we'd encounter on embedded systems. Furthermore, the code, apart from having C, may have assembly as well. The purpose of opening this issue to spur a discussion on this topic.

kcc error about missing class

On Ubuntu 16.04 (64bit), I get the following message:

fhussain@machine1:~/repos/research/fpcsmith/fpbugshome/bug1$ kcc -d -I${CSMITH_HOME}/runtime wrong1.c
'/home/fhussain/repos/research/c-semantics/dist/x86-gcc-limited-libc/pp' '-I' '/home/fhussain/repos/research/fpcsmith/runtime' '-pedantic' 'wrong1.c' '-o' 'tmp-kcc-mJ9kxLC'
/home/fhussain/repos/research/c-semantics/dist/cparser tmp-kcc-mJ9kxLC --trueName 'wrong1.c' > tmp-kcc-wDXoODW
'krun' '--output' 'binary' '--output-file' 'tmp-kcc-oHO79iI' '-d' '/home/fhussain/repos/research/c-semantics/dist/x86-gcc-limited-libc/c11-translation-kompiled' '-w' 'none' '--smt' 'none' '--debug' '--interpret' '-cOPTIONS=_Set_(SetItem(NoLink(.KList)), .Set(.KList)) ' '-pOPTIONS=printf %s' '-pOBJS=printf %s' '-cOBJS=.K' '--parser' 'cat' 'tmp-kcc-wDXoODW'
File: /home/fhussain/repos/research/fpcsmith/runtime/safe_math.h
Line: 301
Error: UB-CEB12
Description: Potential negative zero produced via bitwise operations (this could be a false positive).
Type: Undefined behavior.
See also: C11 sec. 6.2.6.2:4, J.2:1 item 14
Error: Could not find or load main class org.kframework.main.BinaryToText
Translation failed (config dumped). Refer to last command run for details.

Did I miss a classpath somewhere? I do have the class file:

fhussain@machine1:~/repos/research/k$ find . -name "BinaryToText*"
./kernel/target/classes/org/kframework/main/BinaryToText.class
./kernel/src/main/java/org/kframework/main/BinaryToText.java

Thanks.

Unspecified vs Implementation Defined Behaviors

kcc often lists implementation defined behavior as unspecified. The difference between the two is documented in C11 sec. 3.4.1 and 3.4.4.

Even though it may not be technically wrong to list implementation defined behavior as unspecified, kcc should be able to distinguish between the two, just as the standard does.

Consider for instance error code "CCV1", that has message "signed overflow". kcc categorizes this as unspecified behavior. C11, on the other hand, in section 6.3.1.3:3 mentions that the error is implementation defined. Moreover, sec. J.1:1 (a list of unspecified behaviors encountered in the standard), does not have the error in its original form.

About c11.k

Where is the c11.k ? I can't find it.

kcc and gcc disagree on well-defined program (packed offsetof)

The following program is well-defined according to kcc, yet they show different outputs.

$ gcc 3-array-in-struct.c
$ ./a.out ; echo $?
offsetof: 31
5
$ kcc 3-array-in-struct.c
$ ./a.out ; echo $?
offsetof: 32
5
$

Here is the program:

#include <stddef.h>
#include <stdio.h>

struct foo {
  char buffer[31];
  int secret __attribute__ ((packed));
};

int idx = 0;

void setIdx() {
  idx = 31;
}

int main() {
  setIdx();
  struct foo x = {0};
  printf("offsetof: %lu\n", offsetof(struct foo, secret));;
  x.secret = 5;
  char* d = (char*)(&x);
  d += offsetof(struct foo, secret);
  int * e = (int *)d;
  return *e;
}

@diekmann thinks: I specified the struct with the attribute packed, so the offset must be 31. kcc reports undefined behavior if I remove the offsetof and replace it with 31.

Build errors in c-semantics on 'make -j4'

I get these llvm/clang related build errors when 'make'ing, although I did follow all the install instructions. I will appreciate if you can have a look and tell me what I'm doing wrong.

merrors.20sep2016.txt

Build fails after c95b33500c49836f0f1b277c226d5f136beaf179

After c95b335, I am not able to build the semantics. However, building with 2ecd8fe and 46628b2 without c95b335 works fine.

However, log does not seem to contain anything interesting:

kdep -d "x86-gcc-limited-libc/c11-nd-thread-kompiled" -I /path/to/c-semantics/x86-gcc-limited-libc/semantics -I /path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics -- c11-cpp14.k > .depend-nd-thread-tmp
mv .depend-nd-thread-tmp .depend-nd-thread
kdep -d "x86-gcc-limited-libc/c11-nd-kompiled" -I /path/to/c-semantics/x86-gcc-limited-libc/semantics -I /path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics -- c11-cpp14.k > .depend-nd-tmp
mv .depend-nd-tmp .depend-nd
kdep  -d "x86-gcc-limited-libc/c11-cpp14-kompiled" -I /path/to/c-semantics/x86-gcc-limited-libc/semantics -I /path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics -- c11-cpp14.k > .depend-execution-tmp
mv .depend-execution-tmp .depend-execution
kdep  -d "x86-gcc-limited-libc/cpp14-translation-kompiled" -I /path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics -I /path/to/c-semantics/x86-gcc-limited-libc/semantics -- cpp14/cpp14-translation.k > .depend-cpp-tmp
mv .depend-cpp-tmp .depend-cpp
kdep  -d "x86-gcc-limited-libc/c11-translation-kompiled" -I /path/to/c-semantics/x86-gcc-limited-libc/semantics -- c11/c11-translation.k > .depend-translation-tmp
mv .depend-translation-tmp .depend-translation
Kompiling the static C++ semantics...
kompile -O2 --backend ocaml --non-strict --exit-code "<result-value> _:Int </result-value>" -w2e --opaque-klabels c11/c11-translation.k --smt none cpp14/cpp14-translation.k -d "x86-gcc-limited-libc/cpp14-translation-kompiled" --no-prelude -w all -v --debug -I /path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics -I /path/to/c-semantics/x86-gcc-limited-libc/semantics
Parse command line options                                   =    49
Importing: Source(/path/to/c-semantics/semantics/./cpp14/cpp14-translation.k)
Importing: Source(/path/to//runtimeverification/k/k-distribution/target/release/k/include/builtin/kast.k)
Importing: Source(/path/to//runtimeverification/k/k-distribution/target/release/k/include/builtin/domains.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/translation.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/conversion.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/elaborator.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/env.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/error.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/init.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/io.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/name.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/operators.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/overloading.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/process-label.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/promotion.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/syntax.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/template-deduction.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/value-category.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/configuration.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/class.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/declarator.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/enum.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/initializer.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/linkage.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/namespace.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/template.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/decl/typedef.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/additive.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/alignof.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/assignment.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/bitwise.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/cast.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/comma.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/conditional.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/function-call.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/eval.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/inc-and-dec.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/literal.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/logical.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/members.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/multiplicative.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/new.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/reference.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/relational.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/sizeof.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/expr/unary.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/block.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/canonicalization.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/expr.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/goto.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/if.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/labeled.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/loop.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/return.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/stmt/try.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/typing/canonicalization.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/typing/dependent.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/typing/expr.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics/cpp-extensions-translation.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/common.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/alignment.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/bitsize.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/builtin.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/class.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/conversion.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/dynamic.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/error.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/promotion-context.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/reference.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/settings.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/symloc.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/syntax.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/typing.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/additive.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/bitwise.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/cast.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/eval.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/multiplicative.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/members.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/relational.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/expr/unary.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/memory/alloc.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/memory/reading.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/memory/writing.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/common/stmt/expr.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics/cpp-extensions-common.k)
Importing: Source(/path/to/c-semantics/semantics/linking/linking.k)
Importing: Source(/path/to/c-semantics/semantics/common/common.k)
Importing: Source(/path/to/c-semantics/semantics/common/alignment.k)
Importing: Source(/path/to/c-semantics/semantics/common/bits.k)
Importing: Source(/path/to/c-semantics/semantics/common/builtin.k)
Importing: Source(/path/to/c-semantics/semantics/common/compat.k)
Importing: Source(/path/to/c-semantics/semantics/common/configuration.k)
Importing: Source(/path/to/c-semantics/semantics/common/error.k)
Importing: Source(/path/to/c-semantics/semantics/common/init.k)
Importing: Source(/path/to/c-semantics/semantics/common/memory.k)
Importing: Source(/path/to/c-semantics/semantics/common/resolution.k)
Importing: Source(/path/to/c-semantics/semantics/common/settings.k)
Importing: Source(/path/to/c-semantics/semantics/common/symloc.k)
Importing: Source(/path/to/c-semantics/semantics/common/syntax.k)
Importing: Source(/path/to/c-semantics/semantics/linking/error.k)
Importing: Source(/path/to/c-semantics/semantics/linking/init.k)
Importing: Source(/path/to/c-semantics/semantics/linking/resolution.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/alignment.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/promotion.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing/common.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing/compatibility.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/settings.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/semantics/c-settings.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/linking/resolution.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics/cpp-settings.k)
/tmp/tmp-kompile-3920466660543057499.l:2451: warning, rule cannot be matched
/tmp/tmp-kompile-433125670004862106.l:18225: warning, rule cannot be matched
/tmp/tmp-kompile-7121154872073150187.l:48464: warning, rule cannot be matched
Parse definition [3121/3146 rules]                           = 133776
Apply compile pipeline                                       = 12911
/tmp/tmp-kompile-726289431847268140.l:58177: warning, rule cannot be matched
/tmp/tmp-kompile-8999958745240912615.l:58177: warning, rule cannot be matched
Importing: Source(/path/to/c-semantics/semantics/./c11/c11-translation.k)
Importing: Source(/path/to/c-semantics/semantics/c11/c11-translation.k)
Importing: Source(/path/to//runtimeverification/k/k-distribution/target/release/k/include/builtin/kast.k)
Importing: Source(/path/to//runtimeverification/k/k-distribution/target/release/k/include/builtin/domains.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/translation.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/syntax.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/annotation.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/compound-literal.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/configuration.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/elaborator.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/env.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/error.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/function-def.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/init.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/io-direct.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/literal.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/process-label.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/promotion.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/decl/definition.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/decl/global.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/decl/initializer.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/decl/local.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/decl/resolution.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/decl/tagged.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/decl/typedef.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/additive.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/alignof.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/assignment.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/bitwise.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/cast.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/conditional.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/eval.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/function-call.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/identifier.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/inc-and-dec.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/logical.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/members.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/multiplicative.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/offsetof.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/reference.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/relational.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/sequencing.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/sizeof.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/expr/unary.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/block.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/break.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/goto.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/if-then.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/labeled.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/loop.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/return.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/static-assert.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/stmt/switch.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/typing/canonicalization.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/typing/interpretation.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/translation/typing/expr.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/semantics/c-extensions-translation.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/common.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/alignment.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/binding.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/bitsize.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/bits.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/conversion.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/dynamic.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/error.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/os-settings.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/promotion-context.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/promotion.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/settings.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/symloc.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/syntax.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/type-builder.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/additive.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/assignment.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/bitwise.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/cast.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/eval.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/members.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/multiplicative.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/reference.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/relational.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/expr/unary.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/memory/alloc.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/memory/reading.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/memory/writing.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing/common.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing/compatibility.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing/misc.k)
Importing: Source(/path/to/c-semantics/semantics/c11/language/common/typing/predicates.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/semantics/c-extensions-common.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/semantics/os-settings.k)
Importing: Source(/path/to/c-semantics/semantics/c11/library/init.k)
Importing: Source(/path/to/c-semantics/semantics/linking/linking.k)
Importing: Source(/path/to/c-semantics/semantics/common/common.k)
Importing: Source(/path/to/c-semantics/semantics/common/alignment.k)
Importing: Source(/path/to/c-semantics/semantics/common/bits.k)
Importing: Source(/path/to/c-semantics/semantics/common/builtin.k)
Importing: Source(/path/to/c-semantics/semantics/common/compat.k)
Importing: Source(/path/to/c-semantics/semantics/common/configuration.k)
Importing: Source(/path/to/c-semantics/semantics/common/error.k)
Importing: Source(/path/to/c-semantics/semantics/common/init.k)
Importing: Source(/path/to/c-semantics/semantics/common/memory.k)
Importing: Source(/path/to/c-semantics/semantics/common/resolution.k)
Importing: Source(/path/to/c-semantics/semantics/common/settings.k)
Importing: Source(/path/to/c-semantics/semantics/common/symloc.k)
Importing: Source(/path/to/c-semantics/semantics/common/syntax.k)
Importing: Source(/path/to/c-semantics/semantics/linking/error.k)
Importing: Source(/path/to/c-semantics/semantics/linking/init.k)
Importing: Source(/path/to/c-semantics/semantics/linking/resolution.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/semantics/c-settings.k)
org.kframework.utils.errorsystem.KEMException: [Warning] Compiler: missing entry for hook C_SEMANTICS.error
	at org.kframework.utils.errorsystem.KExceptionManager.registerInternal(KExceptionManager.java:188)
	at org.kframework.utils.errorsystem.KExceptionManager.register(KExceptionManager.java:175)
	at org.kframework.utils.errorsystem.KExceptionManager.registerCompilerWarning(KExceptionManager.java:109)
	at org.kframework.backend.ocaml.DefinitionToOcaml.definition(DefinitionToOcaml.java:1232)
	at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:53)
	at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
	at org.kframework.main.Main.runApplication(Main.java:113)
	at org.kframework.main.Main.runApplication(Main.java:103)
	at org.kframework.main.Main.main(Main.java:52)
[Warning] Compiler: missing entry for hook C_SEMANTICS.error

I have seen the warning

[Warning] Compiler: missing entry for hook C_SEMANTICS.error

many times and it was never a problem.

take more advantage of local rewriting

Much of the C semantics was written long ago, when the K framework did not support many of its current features and was buggy. Now we should be able to replace rules of the form

rule compositeFunctionType(T:Type, Mods:Set, .K, P:List, .List, _)
  => compositeFunctionType(T, Mods, .K, .List, .List, P)
requires P =/=K .List

with

rule compositeFunctionType(T:Type, Mods:Set, .K, `P:List => .List`, .List, `_ => P`)
requires P =/=K .List

This is more compact and potentially faster and more concurrent.

This is not urgent, but it may be worth beautifying a bit the C semantics at some later point. Maybe have some intern or someone interested in learning the C semantics do it? Any volunteer?

expression in sizeof is evaluated if it is a constant expression

int main() {
  size_t x = sizeof(*((char *)0));
  return 0;
}

This program should succeed. However, we report a false positive of a null pointer read because we are evaluating the constant expression associated with dereferencing a null pointer. Something needs to be done so that we can compute the type of sizeof expressions without requiring that the expression is evaluated for possible undefined behaviors.

Error while compiling libc: builtintypes.c[6:0-0] : syntax error

Since 966b06c I encounter following error while trying to compile libc:

Translating the standard library... (/path/to/c-semantics/x86-gcc-limited-libc)
cd /path/to/c-semantics/x86-gcc-limited-libc/src && /path/to/c-semantics/dist/kcc -nodefaultlibs -Xbuiltins -shared -o /path/to/c-semantics/dist/x86-gcc-limited-libc/lib/libc.so *.c  -I .
Can't exec "rv-ifdefclear": No such file or directory at /path/to/c-semantics/dist/kcc line 906.
builtintypes.c[6:0-0] : syntax error
Translation failed (config dumped). Run kcc -d -nodefaultlibs -Xbuiltins -shared -o /path/to/c-semantics/dist/x86-gcc-limited-libc/lib/libc.so builtintypes.c ctype.c math.c stdlib.c string.c -I . to see commands run.

The output of running kcc -d is following:

'/path/to/c-semantics/dist/x86-gcc-limited-libc/pp' '-I' '.' '-pedantic' 'builtintypes.c' '-o' 'tmp-kcc-mmmVwXv'
Can't exec "rv-ifdefclear": No such file or directory at /path/to/c-semantics//dist/kcc line 906.
/path/to/c-semantics/dist/cparser tmp-kcc-mmmVwXv --trueName 'builtintypes.c' > tmp-kcc-P66oKAV
builtintypes.c[6:0-0] : syntax error
Translation failed (config dumped). Refer to last command run for details

The file tmp-kcc-P66oKAV then contains only 'Parsing error'. The preprocessed file (tmp-kcc-mmmVwXv) looks good. I think that missing rv-ifdefclear is not the problem, because I have already encountered it before.

kcc on structs with no named members

Consider the program:
struct a{
int : 5
};

int main() {
printf("Execution");
}
Compiling this file with kcc, and then running it works fine, and "Execution" is printed to the screen. However, according C11 sec 6.7.2.1, "A structure or union is defined as containing no named members" is undefined. Shouldn't kcc also be reporting undefined behavior here?

For loop line information is wrong

If you have time for this after fixing the issue with the effective types, this is the second highest priority bug to fix. The issue is that line information is wrong for undefinedness that occurs as part of the clauses of a for loop. For example:

int buf[5] = {0};
for (int i = 0; buf[i] == 0; i++) {
  printf("%d", i);
}

This should output a buffer overflow on the line with buf[i] == 0. However, the error reported refers to the following line. I believe this involves how we rewrite for loops. But it would be good if we could fix this.

README.md is missing from the examples directory

If that is by design, then the link at top-level README.md should be updated.

Edgar

composite type of vla with size not evaluated

consider:

#include<stddef.h>
int main() {
  int x = 5;
  int y[x];
  sizeof(0 ? (int (*) [x]) NULL : NULL);
  return 0;
}

This should be undefined because the type of the conditional expression is the composite type of its two branches, and the type of the first branch is a vla type whose size specifier is not evaluated. Composite types are not allowed in this case. I think this might have worked before we went back to the old type strictness, but it seems broken now. There needs to be some case to handle this added to typing/expr.k

does the C semantics require gcc?

=-=- Installing compiler 4.03.0+trunk -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[default.comp] https://github.com/ocaml/ocaml/tarball/trunk downloaded
Now compiling OCaml. This may take a while, please bear with us...
[ERROR] Compiler build failed at "./configure -prefix /Users/cos/.opam/4.03.0+trunk -with-debug-runtime":
        # opam-version 1.2.2
        # os           darwin
        # command      ./configure -prefix /Users/cos/.opam/4.03.0+trunk -with-debug-runtime
        # path         /Users/cos/.opam/4.03.0+trunk/build/ocaml
        # exit-code    2
        # env-file     /Users/cos/.opam/log/log-21577-6d07ae.env
        # stdout-file  /Users/cos/.opam/log/log-21577-6d07ae.out
        # stderr-file  /Users/cos/.opam/log/log-21577-6d07ae.err
        ### stdout ###
        # Configuring OCaml version 4.03.0+dev11-2015-10-19
        # Configuring for host x86_64-apple-darwin15.0.0 ...
        # Configuring for target x86_64-apple-darwin15.0.0 ...
        # Using compiler gcc.
        # Compiler family and version: .
        # [ERROR!] Unable to compile the test program.
        #  Make sure the C compiler gcc  is properly installed.
        ### stderr ###
        # ./runtest: line 21: 21647 Segmentation fault: 11  $cc -o tst $* $cclibs 2> /dev/null

Testing errors

Hello,

I've installed the C semantics following the given instructions and I'm getting these errors at the end of make -j4:

Testing kcc...
printf "#include <stdio.h>\nint main(void) {printf(\"x\"); return 42;}\n" | dist/kcc - -o dist/testProgram.compiled
dist/testProgram.compiled 2> /dev/null > dist/testProgram.out; test $? -eq 42
grep x dist/testProgram.out > /dev/null
Done.
Cleaning up...
Done.
make[1]: Entering directory '/home/fmse/c-semantics/k/c-semantics/semantics'
kdep -d "x86-gcc-limited-libc/c11-nd-thread-kompiled" -I /home/fmse/c-semantics/k/c-semantics/x86-gcc-limited-libc/semantics -- c11.k > .depend-nd-thread-tmp
mv .depend-nd-thread-tmp .depend-nd-thread
kdep -d "x86-gcc-limited-libc/c11-nd-kompiled" -I /home/fmse/c-semantics/k/c-semantics/x86-gcc-limited-libc/semantics -- c11.k > .depend-nd-tmp
mv .depend-nd-tmp .depend-nd
kdep  -d "x86-gcc-limited-libc/c11-kompiled" -I /home/fmse/c-semantics/k/c-semantics/x86-gcc-limited-libc/semantics -- c11.k > .depend-execution-tmp
mv .depend-execution-tmp .depend-execution
kdep  -d "x86-gcc-limited-libc/c11-translation-kompiled" -I /home/fmse/c-semantics/k/c-semantics/x86-gcc-limited-libc/semantics -- c11-translation.k > .depend-translation-tmp
mv .depend-translation-tmp .depend-translation
Kompiling the dynamic C semantics with expression sequencing non-determinism...
kompile -O2 --backend ocaml --non-strict --exit-code "<result-value> _:Int </result-value>" --smt none c11.k -d "x86-gcc-limited-libc/c11-nd-kompiled" --no-prelude --transition "observable ndtrans" --superheat "ndheat" --supercool "ndlocal" -I /home/fmse/c-semantics/k/c-semantics/x86-gcc-limited-libc/semantics
[Error] Critical: Unknown option: --superheat
Makefile:29: recipe for target 'x86-gcc-limited-libc/c11-nd-kompiled/c11-nd-kompiled/timestamp' failed
make[1]: *** [x86-gcc-limited-libc/c11-nd-kompiled/c11-nd-kompiled/timestamp] Error 1
make[1]: Leaving directory '/home/fmse/c-semantics/k/c-semantics/semantics'
Makefile:89: recipe for target 'semantics' failed
make: *** [semantics] Error 2

It looks like the tests fail because the --superheat option is not known by kompile. This is weird because I'm using exactly the K tool suggested in INSTALL.md and I have done this on a newly installed Ubuntu with no K installed before.

The dist directory seems to be created and the helloworld.c example (suggested at the end of INSTALL.md) works. Can trust the compiled semantics if the tests fail?

Diamond in subsorting

Is there any reason to have the production

syntax KItem ::= Type [avoid]

in cil-exp.k? The definition kompiles without it.

It would be nice if the CIL semantics works with the Coq backend, and to help that I'd like to label the injections into TypeOrExp, but doing it without removing that KItem production produces parsing ambiguities (maybe a bug, I opened runtimeverification/k#589).

OCaml compiler patches

I think it would be possible to provide an opam compiler description file that applies Dwight's compilation speed patches:

https://opam.ocaml.org/doc/manual/dev-manual.html#sec24

on dealing with libraries

@dwightguth: I'm posting this issue only because I want to make sure I don't forget it to check it with you and make sure that we converge on this, so we tell our users/customers the same story.

Regarding adding execution support for libraries to the C semantics, I believe that the clean approach is to do it through the support for builtins that the framework currently supports. That is, to add a new builtin function, say int foo(int x, int* y), we would probably want to do something like this:

  syntax Id ::= "foo"  [hook(myFooImplementation)]

or something like this

  syntax Exp ::= foo(Decl, Decl)  [hook(myFooImplementation)]

This way we can smoothly switch between builtin vs user-defined vs C-code semantics of libraries, and, moreover, there is a chance that other semantics can also make use of the same hooks/builtins, e.g., LLVM. Let me know if you disagree, or you believe that we should do it differently.

Syncing Examples and Error Codes

Currently, the Error Codes CSV is modified manually when any change to the semantics is made. This process is error prone, and may lead to the CSV being out of sync with the examples, and the semantics. We need some way of automatically generating the CSV from the semantics, and then checking if all the error codes have corresponding examples in the examples directory. Additionally we may want to then run the examples, check if they produce the required error, and update the output files.

Minor mistake in INSTALL.md

opam switch 4.03+trunk should be opam switch 4.03.0+trunk

Edgar.

spell-check error messages

See, for example, "Implementiation" in the error message below:

Error: IMPL-CCV2
Description: conversion to signed integer outside the range that can be represented.
Type: Implementiation defined behavior.
See also: C11 sec. 6.3.1.3:3, J.3.5:1 item 4
  at main(6-int-overflow.c:5)
  at <file-scope>(<unknown>)

illegal quoting in errors file

https://github.com/kframework/c-semantics/blob/master/examples/error-codes/Error_Codes.csv#L102

How comes we have this error, and how comes everything works with it?

remove OLD_LICENSE

What's the point of keeping two licenses?

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

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?

Redeclaring the same identifier within a block not resulting in an error

This following program,

int main() {
  int a;
  int a;
}

produces no error with kcc. Also executes without error.

Shouldn't an error like, "redeclaration of identifier with no linkage" be thrown here?

inline definitions

It would appear the C semantics does not correctly handle inline definitions, but instead treats them as if they are external definitions, which they are not. It would be good for us to fix this case. Cf C11 section 6.7.4.

For example, this program:

inline int foo() { return 6; }

int main() {
  return foo();
}

Should fail to compile because an inline definition was created for the function foo with external linkage, and the identifier was referenced, but it was not given an external definition in another translation unit. However, kcc compiles it successfully.

Similarly, if the following file is compiled into the same program as the previous file:

int foo() { return 6; }

It should then compile successfully because the external definition was used. However, instead, it fails because it believes there are multiple external definitions for foo, even though one is actually an inline definition and therefore not an external definition.

Capitalize all error messages, both in the error_codes table and in the code

https://github.com/kframework/c-semantics/blob/master/examples/error-codes/Error_Codes.csv#L170-L171

make issue

I want to install it on my mac. After typing "make -j4", there is error: 'clang/AST/ASTConsumer.h' file not found
#include "clang/AST/ASTConsumer.h"

Any one can solve that problem?

Issue with K version 3.6 and Ocaml 4.03.0+k and oasis package

@ellisonch @cos

Hi Chucky and Cosmin,

I am trying to install the c-semantics but keep having an issue when I do the k-configure-opam-dev.

It's trying to install the oasis package but I got the following error:

The following dependencies couldn't be met:

mlgmp -> oasis
Your request can't be satisfied:
oasis is not available because your system doesn't comply with ocaml-version >= "3.11.2" & ocaml-version < "4.03.0".

Am I doing something wrong ?

Thanks for the reply !

and congrats for the work behind K ! its truly awesome !!!

unable to run the CIL semantics following the instructions

I am trying to follow the instructions at:
https://github.com/kframework/c-semantics/tree/java_rewrite_engine/cil-semantics#how-to-use-and-test-the-cil-semantics
to run the CIL semantics.

kcil, kcil-pp & kompile are all in my PATH. And I have successfully kompiled cil.k.

yilongli@ubuntu:~/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics$ which kcil
/home/yilongli/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics/kcil
yilongli@ubuntu:~/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics$ which kcil-pp
/home/yilongli/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics/kcil-pp
yilongli@ubuntu:~/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics$ which kompile 
/home/yilongli/Eclipse-Workspaces/sbtg-workspace/k/bin/kompile

However, I couldn't even run the simplest program, test.cil.c in the directory. Here is the error message.

yilongli@ubuntu:~/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics$ kcil test.cil.c
Error running KCIL preprocessor:
Could not open /home/yilongli/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics/test.cil.c.cil for reading: No such file or directory
Died at /home/yilongli/Eclipse-Workspaces/sbtg-workspace/c-semantics/cil-semantics/kcil line 214.

This is very frustrating. Can someone help me out? Thanks!

Excessive depth in document: use XML_PARSE_HUGE

From a user:

Error compiling program:
Entity: line 32: parser error : Excessive depth in document: 256 use
XML_PARSE_HUGE option

ons>
<StmtCons

^
Died at /home/pwilke/csemantics/c-semantics/dist/kcc line 432.

I think this is caused by the XML AST representation of function bodies as a tree of nested cells instead of a list of cells at equal depth. It looks like it would effect functions over a certain number of lines (256?). The solution seems to be to flatten this tree into a list in the parser, before printing the AST as XML.

Don't seem to process declarations in old-style functions

Consider the following function:

struct foo;
void bar(x)
  struct foo x;
{
  //do stuff
}

This should generate an error because x has no linkage and is incomplete, but it doesn't seem to be processed.

build fails on MacOS

Makefile checks for clang version 3.5, not 3.5 or newer. This causes the build to fail on the latest MacOS, which has clang 3.6.

NPE in SymbolicRewriter.rewrite

It looks to me like if you pass a bound of zero to SymbolicRewriter.rewrite, you end up returning null from the method. In this case it should return the value passed into the function instead.

Handling floating point

1.0f translates to Float(#"1e+00") instead of Float(#"1e+00f")
Generally, account for both float and double constants.

Return semantics deletes pending ```exitRestrictScope``` operations.

The rule in semantics/language/execution/stmt/return.k:42 deletes the remaining of the k cell which may contain pending exitRestrictScope operations.

Fix Robby's program

This program should be undefined:

 #include <stdio.h>

 unsigned long f() {
  double d = -0.5;
  return d * (1 << 30);
 }
 int main() {
  printf("0x%lx\n",f());
 }

kcc on empty structs

Consider the program:
struct a{
};

int main() {
printf("Execution");
}

kcc, when run on this file, reports undefined behavior, with error code "CDT1" and the error message being "structs cannot be empty". C11 6.2.5:20 mentions that a struct is a "non empty set of member objects". Doesn't this actually define the behavior? Shouldn't kcc not report this as undefined behavior?

Test failure with newest K

Testing b7099f5 against runtimeverification/k@425f4a4 fails one test in unit-fail, j087a.c

$ cat j087a.out
Error: CEE2
Description: Referring to an object outside of its lifetime.
Type: Undefined behavior.
See also: C11 sec. 6.2.4
  at __va_inc(j087a.c:6)
  at f(j087a.c:6)
  at main(j087a.c:11)
  at <file-scope>(<unknown>)
$ cat j087a.ref
Error: EIO10
Description: Type of lvalue not compatible with the effective type of the object being accessed.
Type: Undefined behavior.
See also: C11 sec. 6.5:7
  at f(j087a.c:6)
  at main(j087a.c:11)
  at <file-scope>(<unknown>

Linkage check for block-scope functions

Valid aggregate initialization results in error

Consider this example:

static char *x[] = {"foo"};

Compiling it with kcc results in

File: test.c
Line: 1
Error: UB-CDI3
Description: Invalid initializer for aggregate type.
Type: Undefined behavior.
See also: C11 sec. 6.7.9:16, J.2:1 item 83

a.out uses an option that is no longer supported by krun

I tried running ./a.out of a program compiled with kcc, but it failed with the following error:

VERBOSE=1 ./a.out
krun --output-mode raw --load-cfg tmp-kcc-in-vWl9u9gdx3O.c11 --io on -d /home/mikida2/kframework/c-semantics/dist/c11-kompiled --parser cat -cARGC=1 --output tmp-kcc-out-vbltIAtx7zB.txt --verbose -cARGV=""./a.out"",,.KList
Error while parsing commandline:Unrecognized option: --load-cfg

This is probably because of a recent overhaul to the options provided by all tools.

Effective type check for structs/union is backwards

So if you look at the C11 standard section 6.5 paragraphs 6 and 7, it says that an object with effective type E can be accessed by an lvalue with type L if (among other conditions) L is an aggregate or union type and one of its members has type L' which is type for which an lvalue in allowed to access an object with effective type E.

However, currently this check is backwards, we are checking that E is an aggregate type and one of its members E' is a type which, were it the effective type of an object, could be accessed via an lvalue of type L.

I tried to fix this but it turned out to be more complicated than I expected because simply reversing the order of the check generated a lot of false positives. They seem to arise in the case where getTypeAtOffset accepts an offset of 0 and therefore returns the aggregate type itself. This aggregate type is then used as the effective type of a write to a subobject of the struct with a different type, which causes an error to be raised. I'm not entirely sure what the correct solution is here, because strictly assigning the struct type as the effective type of an object of allocated duration that has been written to through an lvalue of struct type, would seem to mean that if I subsequently write to any member of that struct, it is undefined according to the aliasing rules. It's pretty clear that the interactions between aggregate/union types and effective type was not completely worked out properly by the standard, but I don't have the time to work out something reasonable for us to do in this case. I think what I would propose is to make the effective type of subobjects be the corresponding member type of the effective type of the parent object. So if I have a declared object of aggregate or union type, the effective type when accessing an entire aggregate or union would be the declared type, and when accessing a member would be the inner type of the member. And if I have a malloced object that has been given an effective type of an aggregate or union type, then when I read or write one of its members, we treat the effective type as the type of the member actually stored at that offset.

That way, when we call #effectivelyCompat, the effective type we pass it will never be an aggregate or union except in cases when the lvalue is also an aggregate or union.

This seems kind of tricky to handle though so I'm creating an issue for this and assigning it to @chathhorn . Chris, when you read this, if you want to discuss the issue or propose an alternate solution, let me know.

Result of relational operators does not have type 'bool'

In semantics/cpp14/language/translation/expr/relational.k, there are some rules like this one:

     rule R1:PRVal == R2:PRVal
          => pre(stripHold(R1) == stripHold(R2), combine(...), type(R1))

I suppose there should be type(bool) on rhs. For example, the following program

int x = 1;
if (true == (x == 2))
    ;

fails in runtime. I can create pull request if you agree this is a bug.

Function Parameter with storage class other than register

Consider the following:

void fnc(static int a) {
  a = 4;
}
int main()
{
  fnc(2);
}

Running the program above results in Translation failed. Run kcc -d static.c to see commands run. The expected error in this case should have codeCV-TDG5 and description function parameter appears with storage class other than register.

kcc fails without error if _GNU_SOURCE is enabled for fcntl.h

Hi,

I tested kcc with the following "simple" program:

#define _GNU_SOURCE

#include <stdio.h>
#include <fcntl.h>

int main(int argc, char **argv){
        printf("Hello World\n");
        return 0;
}

It fails with the following (not very helpful) error:

Error: Could not find or load main class org.kframework.main.BinaryToText
Translation failed (config dumped). Run kcc -d tests/gnusource.c to see commands run.

It fails with the same error if I enable kserver. If I remove the #define _GNU_SOURCE, everything works fine. Something in the fcntl.h must cause the error.

Tested on vanilla Ubuntu 16.04 with a fresh installation of k and c-semantics as of today.

About my setup:
k 1b84d683339e39c7268f2496544fafcdd81fbc8f Dec 13 2016
c-semantics 66b31eb Dec 15 2016
Installed according to the guide.
Ubuntu 16.04.1 LTS

Edit: kcc -Wsystem-headers reports an error. It would be incredibly helpful for starters if kcc would hint that this parameter exists. The current output is quite misleading.
Ultimately, the fix is to get the binary rv-match distribution which hopefully can process this header?

kframework / c-semantics Goto Github PK

c-semantics's People

Contributors

Stargazers

Watchers

Forkers

c-semantics's Issues

Recommend Projects

Recommend Topics

Recommend Org