From 4a083ff8bd7ebb08d63d0a90aaa110f14e2e9079 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 28 Jun 2019 00:12:31 +0000 Subject: [PATCH 01/84] LLVM backend: kcc/runner scripts. --- Makefile | 2 +- scripts/kcc | 98 +++++++++++++++---------------- scripts/program-runner | 77 +++++++----------------- semantics/Makefile | 4 +- semantics/linking/configuration.k | 2 +- 5 files changed, 72 insertions(+), 111 deletions(-) diff --git a/Makefile b/Makefile index 9b28f6b69..38a808f41 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ export KOMPILE := $(K_BIN)/kompile export KDEP := $(K_BIN)/kdep # Appending to whatever the environment provided. -K_OPTS += -Xmx8g +K_OPTS += -Xmx16g K_OPTS += -Xss32m export K_OPTS diff --git a/scripts/kcc b/scripts/kcc index 3867ab23d..27d09d3aa 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -37,6 +37,8 @@ use constant KRUN => do { my $ext = IS_CYGWIN? '.bat' : ''; $path . $ext; }; + +use constant LLVM_KRUN => kBinDir('llvm-krun'); use constant PRINTF => IS_CYGWIN? 'printf %%s' : 'printf %s'; use constant QUOTE_INT => IS_CYGWIN? printable("\"Int\"") : "\"Int\""; use constant QUOTE_STRING => IS_CYGWIN? printable("\"String\"") : "\"String\""; @@ -127,7 +129,7 @@ sub main { close(FILE); my $profDir = profileDir(); - my $krun = KRUN; + my $krun = LLVM_KRUN; $template =~ s?__EXTERN_SCRIPTS_DIR__?$profDir?g; $template =~ s?__EXTERN_HEAP_SIZE__?$heapSize?g; $template =~ s?__EXTERN_KRUN__?$krun?g; @@ -292,15 +294,15 @@ sub makeOptions { my @options = (); if (arg('-fno-native-compilation')) { - push(@options, "`NoNativeFallback`(.KList)"); + push(@options, "LblNoNativeFallback{}()"); } if (arg('-frecover-all-errors')) { - push(@options, "`RecoverAll`(.KList)"); + push(@options, "LblRecoverAll{}()"); } if (arg('-fuse-native-std-lib')) { - push(@options, "`UseNativeStdLib`(.KList)"); + push(@options, "LblUseNativeStdLib{})"); } if (arg('-flint') || arg('-Wlint')) { @@ -334,23 +336,23 @@ sub makeOptions { $stackSize = printable($stackSize); } my $int = QUOTE_INT; - push(@options, "`Lint`(.KList)"); - push(@options, "`Heap`(#token($heapSize, $int))"); - push(@options, "`Stack`(#token($stackSize, $int))"); + push(@options, "LblLint{}()"); + push(@options, "LblHeap{}(\\dv{SortInt{}}($heapSize))"); + push(@options, "LblStack{}(\\dv{SortInt{}}($stackSize))"); } if (arg('-e')) { my $entry = quote(printable(quote(arg('-e')))); my $string = QUOTE_STRING; - push(@options, "`EntryPoint`(#token($entry, $string))"); + push(@options, "LblEntryPoint{}(\\dv{SortString{}}($entry))"); } if (arg('-finteractive-fail')) { - push(@options, "`InteractiveFail`(.KList)"); + push(@options, "LblInteractiveFail{}()"); } if (arg('-Wfatal-errors')) { - push(@options, "`FatalErrors`(.KList)"); + push(@options, "LblFatalErrors{}()"); } for (breakpoints()) { @@ -358,22 +360,22 @@ sub makeOptions { $file = quote(printable(quote(rel2abs($file)))); $line = quote(printable($line)); my ($string, $int) = (QUOTE_STRING, QUOTE_INT); - push(@options, "`Breakpoint`(#token($file, $string), #token($line, $int))"); + push(@options, "LblBreakpoint{}(\\dv{SortString{}}($file), \\dv{SortInt{}}($line))"); } if ($link) { - push(@options, "`Link`(.KList)"); + push(@options, "LblLink{}()"); } - return makeSet(@options); + return makeOptionSet(@options); } sub addArg { - my ($name, $value, $category, @krunArgs) = @_; + my ($name, $value, $sort, $category, @krunArgs) = @_; if (useInterpreter()) { - push(@krunArgs, '-c', $name, $value, $category); + push(@krunArgs, '-c', $name, $value, $sort, $category); } else { push(@krunArgs, "-c$name=$value"); if ($category eq 'text' or $category eq 'binary') { @@ -414,7 +416,7 @@ sub linkAll { } sub getKRunCommand { - my ($output, $symbols, $sem) = @_; + my ($output, $sem) = @_; my $def = profileDir($sem); @@ -422,9 +424,9 @@ sub getKRunCommand { if (useInterpreter()) { my $dir = catfile($def, $sem); @krun = - ( catfile($dir, 'interpreter') - , catfile($dir, 'realdef.cma') - , $symbols + ( LLVM_KRUN + , '-d' + , $dir , '--output-file', $output ); } else { @@ -435,7 +437,6 @@ sub getKRunCommand { , '-d', $def , '-w', 'none' , '--smt', 'none' - , '--argv', $symbols ); if (arg('-d')) { @@ -451,7 +452,7 @@ sub getLinkingCommand { my @objs = objFiles(); - my @krun = getKRunCommand($output, $symbols, 'c-cpp-linking-kompiled'); + my @krun = getKRunCommand($output, 'c-cpp-linking-kompiled'); if (arg('-flinking-depth=')) { push(@krun, '--depth'); @@ -459,15 +460,15 @@ sub getLinkingCommand { } my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING); - my $json = "#token($rvErrorJson, $string)"; + my $json = "\\dv{SortString{}}($rvErrorJson)"; - @krun = addArg("OPTIONS", makeOptions($link), 'text', @krun); - @krun = addArg("JSON", $json, 'text', @krun); + @krun = addArg("OPTIONS", makeOptions($link), 'Set', 'kore', @krun); + @krun = addArg("JSON", $json, 'String', 'kore', @krun); my $uuid = create_uuid_as_string(); my $encodedUuid = quote(printable(quote($uuid))); - my $uuidOpt = "#token($encodedUuid, $string)"; - @krun = addArg("UUID", $uuidOpt, 'text', @krun); + my $uuidOpt = "\\dv{SortString{}}($encodedUuid)"; + @krun = addArg("UUID", $uuidOpt, 'String', 'kore', @krun); if (scalar @objs) { my $allObjsFile = tempFile('all-objs'); @@ -483,29 +484,24 @@ sub getLinkingCommand { }; } if (length $thisObj) { - # push(@objTexts, "`unwrapObj`($thisObj)"); - $thisObj = substr($thisObj, 8, -1); # wrap $thisObj with `unwrapObj`() - push(@objTexts, "$thisObj\x02\x00\x00\x00\x00\x00\x00\x00\x09\x00u\x00n\x00w\x00r\x00a\x00p\x00O\x00b\x00j\x00\x00\x00\x00\x01"); + push(@objTexts, "LblunwrapObj{}($thisObj)"); } } - my $objText = join('', @objTexts); - my $one = chr((scalar @objTexts >> 24) & 0xff); - my $two = chr((scalar @objTexts >> 16) & 0xff); - my $three = chr((scalar @objTexts >> 8) & 0xff); - my $four = chr((scalar @objTexts >> 0) & 0xff); - $objText = MAGIC . "\x04\x00\x01$objText\x03$one$two$three$four\x07"; + my $objText = 'dotk{}()'; + foreach my $obj (@objTexts) { + $objText = 'kseq{}(' . $obj . ', ' . $objText . ')'; + } + $objText = "Lblload{}($objText)"; open(my $file, '>', "$allObjsFile"); print $file $objText; close $file; - @krun = addArg("OBJS", $allObjsFile, 'binaryfile', @krun); + @krun = addArg("OBJS", $allObjsFile, 'KItem', 'korefile', @krun); } else { - @krun = addArg("OBJS", ".K", 'text', @krun); + @krun = addArg("OBJS", "Lblload{}(dotk{}())", 'KItem', 'text', @krun); } - @krun = addArg("PGM", ".K", 'text', @krun); - setShellDebugFile($output, 1); return @krun; } @@ -516,7 +512,7 @@ sub getTranslationCommand { my $cTransDef = profileDir("c-translation-kompiled"); my $cppTransDef = profileDir("cpp-translation-kompiled"); - my @krun = getKRunCommand($output, 'dummy', + my @krun = getKRunCommand($output, $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled'); if (arg('-ftranslation-depth=')) { @@ -525,17 +521,17 @@ sub getTranslationCommand { } my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING); - my $json = "#token($rvErrorJson, $string)"; + my $json = "\\dv{SortString{}}($rvErrorJson)"; - @krun = addArg("OPTIONS", makeOptions(0), 'text', @krun); - @krun = addArg("JSON", $json, 'text', @krun); + @krun = addArg("OPTIONS", makeOptions(0), 'Set', 'kore', @krun); + @krun = addArg("JSON", $json, 'String', 'kore', @krun); my $encodedUuid = quote(printable(quote($uuid))); - my $uuidOpt = "#token($encodedUuid, $string)"; - @krun = addArg("UUID", $uuidOpt, 'text', @krun); + my $uuidOpt = "\\dv{SortString{}}($encodedUuid)"; + @krun = addArg("UUID", $uuidOpt, 'String', 'kore', @krun); my $kast = parse($src, $lang, $trampolines); - @krun = addArg("PGM", $kast, 'textfile', @krun); + @krun = addArg("PGM", $kast, 'KItem', 'korefile', @krun); setShellDebugFile($output, 1); return @krun; @@ -612,7 +608,7 @@ sub parse { return $kast; } my $cparser = distDir('cparser'); - shell($cparser, $ppResult, '--trueName', $inputFile)->verbose()->stdout($kast)->run(); + shell($cparser, $ppResult, '--kore', '--trueName', $inputFile)->verbose()->stdout($kast)->run(); return $kast; } @@ -641,16 +637,16 @@ sub getStd { return "-std=$std"; } -sub makeSet { - my $set = '`.Set`(.KList)'; +sub makeOptionSet { + my $set = "Lbl'Stop'Set{}()"; foreach my $el (@_) { - $set = "`_Set_`(`SetItem`($el), $set)"; + $set = "Lbl'Unds'Set'Unds'{}(LblSetItem{}(inj{SortOpt{}, SortKItem{}}($el)), $set)"; } return $set; } sub useInterpreter { - -e profileDir('cpp-translation-kompiled', 'cpp-translation-kompiled', 'interpreter'); + return 1; } sub getRVErrorJson { diff --git a/scripts/program-runner b/scripts/program-runner index f9dff59b3..63cf81856 100755 --- a/scripts/program-runner +++ b/scripts/program-runner @@ -8,6 +8,7 @@ use File::Temp; use File::Copy; use MIME::Base64; use String::Escape qw(quote backslash); +use String::ShellQuote qw(shell_quote_best_effort); setpgrp; @@ -31,9 +32,9 @@ my $SCRIPTS_DIR = '__EXTERN_SCRIPTS_DIR__'; my $KRUN = '__EXTERN_KRUN__'; -my $EXEC_DEF = catfile($SCRIPTS_DIR, "c-cpp-kompiled"); -my $EXEC_ND_DEF = catfile($SCRIPTS_DIR, "c-nd-kompiled"); -my $EXEC_ND_THREAD_DEF = catfile($SCRIPTS_DIR, "c-nd-thread-kompiled"); +my $EXEC_DEF = catfile(catfile($SCRIPTS_DIR, "c-cpp-kompiled"), "c-cpp-kompiled"); +my $EXEC_ND_DEF = catfile(catfile($SCRIPTS_DIR, "c-nd-kompiled"), "c-nd-kompiled"); +my $EXEC_ND_THREAD_DEF = catfile(catfile($SCRIPTS_DIR, "c-nd-thread-kompiled"), "c-nd-thread-kompiled"); my @temporaryFiles = (); @@ -64,10 +65,9 @@ sub main { $objInput = ''; } - my $argv = reduce { our ($a, $b); "`_List_`($a,$b)" } (map {qq|`ListItem`(#token($_, "String"))|} (map {quote(backslash(quote(backslash($_))))} ($0, @ARGV))); + my $argv = reduce { our ($a, $b); "Lbl'Unds'List'Unds'{}($a,$b)" } (map {qq|LblListItem{}(inj{SortString{}, SortKItem{}}(\\dv{SortString{}}($_)))|} (map {quote(backslash($_))} ($0, @ARGV))); - my @cmd = ('--output', 'kast', '--no-sort-collections', '--no-alpha-renaming', '-d', $EXEC_DEF, "-cARGV=$argv", '-pARGV=printf %s', '-w', 'none', '--parser', - 'cat', $fileInput); + my @cmd = ('-d', $EXEC_DEF, "-c", "ARGV", $argv, "List", "kore", "-c", "PGM", $fileInput, "GeneratedTopCell", "korefile"); my $options = getOptions(); if (defined $ENV{HELP}) { @@ -84,73 +84,40 @@ sub main { return 1; } - if (defined $ENV{TRACE}) { - push @cmd, '--trace'; - } - if (defined $ENV{DEBUG}) { push @cmd, '--debug'; } - if (defined $ENV{VERBOSE}) { - push @cmd, '--verbose'; - } - - push @cmd, '--native-libraries'; - my $libs = nativeLibraries(); + #push @cmd, '--native-libraries'; + #my $libs = nativeLibraries(); # kcc may have been run as k++ so this is necessary - push @cmd, "-lstdc++ $libs $objInput"; + #push @cmd, "-lstdc++ $libs $objInput"; if (defined $ENV{DEPTH}) { push @cmd, '--depth'; push @cmd, $ENV{DEPTH}; } - if (defined $ENV{PROVE}) { - push @cmd, '--prove'; - push @cmd, $ENV{PROVE}; - push @cmd, '--smt_prelude'; - push @cmd, $ENV{SMT_PRELUDE}; - } else { - push @cmd, '--smt'; - push @cmd, 'none'; - push @cmd, '--output-file'; - push @cmd, $fileOutput; - } - - if (defined $ENV{SEARCH}) { - push @cmd, '--search-final'; - $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)"; - push @cmd, '-d'; - push @cmd, $EXEC_ND_DEF; - print 'Searching reachable states... '; - print "(with non-deterministic expression sequencing)\n"; - } - - if (defined $ENV{THREADSEARCH}) { - push @cmd, '--search-final'; - $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)"; - push @cmd, '-d'; - push @cmd, $EXEC_ND_THREAD_DEF; - print 'Searching reachable states... '; - print "(with non-deterministic thread interleaving)\n"; - } + push @cmd, '--output-file'; + push @cmd, $fileOutput; my $encodedJson = getJson(); - push @cmd, "-cOPTIONS=$options"; - push @cmd, '-pOPTIONS=printf %s'; - push @cmd, '-cJSON=#token(' . $encodedJson . ', "String")'; - push @cmd, '-pJSON=printf %s'; + push @cmd, "-c"; + push @cmd, "OPTIONS"; + push @cmd, $options; + push @cmd, "Set"; + push @cmd, "kore"; + push @cmd, "-c"; + push @cmd, "JSON"; + push @cmd, "\\dv{SortString{}}($encodedJson)"; + push @cmd, "String"; + push @cmd, "kore"; # Execute krun with the arguments in @cmd - print("'krun' '" . join("' '", @cmd) . "'\n") if defined $ENV{VERBOSE}; + print(join(' ', ($KRUN, map {shell_quote_best_effort($_)} @cmd)) . "\n") if defined $ENV{VERBOSE}; my $ret = system($KRUN, @cmd) >> 8; - if (defined $ENV{LTLMC} | defined $ENV{PROVE}) { - return 0; - } - return processResult($fileOutput, $ret, defined $ENV{VERBOSE}); } diff --git a/semantics/Makefile b/semantics/Makefile index e79ca7e21..1143222d4 100644 --- a/semantics/Makefile +++ b/semantics/Makefile @@ -8,9 +8,7 @@ OUTPUT_DIR := $(abspath $(BUILD_DIR)) PROFILE_DIR := $(realpath $(CURDIR)/../profiles/x86-gcc-limited-libc) # Appending to whatever the environment provided. -KOMPILE_FLAGS += --backend ocaml -KOMPILE_FLAGS += --non-strict -KOMPILE_FLAGS += --smt none +KOMPILE_FLAGS += --backend llvm # Generate a makefile list from a colon-separated one. # K_INCLUDE_PATH comes from the environment. diff --git a/semantics/linking/configuration.k b/semantics/linking/configuration.k index 339871e99..c8df194ea 100644 --- a/semantics/linking/configuration.k +++ b/semantics/linking/configuration.k @@ -17,7 +17,7 @@ module C-CONFIGURATION - load($OBJS:K) + $OBJS:KItem ~> linkProgram(getEntryPoint($OPTIONS:Set)) ~> cleanup From a8061d4d02f6e089cc2331b97d77b3ae41b4ed92 Mon Sep 17 00:00:00 2001 From: chathhorn Date: Wed, 28 Aug 2019 17:38:49 -0500 Subject: [PATCH 02/84] Dockerfile: build LLVM backend. --- Dockerfile | 42 ++++++++++++++++++++++++++++-------------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/Dockerfile b/Dockerfile index 7d9cb9584..f60fe2d0e 100644 --- a/Dockerfile +++ b/Dockerfile @@ -4,12 +4,25 @@ FROM runtimeverificationinc/kframework:ubuntu-bionic # Install packages. # ##################### -RUN apt-get update -q \ - && apt install --yes \ - libstdc++6 \ - llvm-6.0 \ - clang++-6.0 \ - clang-6.0 +RUN apt-get update -q \ + && apt-get install --yes \ + libstdc++6 \ + llvm-6.0 \ + clang++-6.0 \ + clang-6.0 \ + clang-8 \ + libclang-8-dev \ + llvm-8-tools \ + lld-8 \ + zlib1g-dev \ + bison \ + flex \ + libboost-test-dev \ + libgmp-dev \ + libmpfr-dev \ + libyaml-dev \ + libjemalloc-dev \ + pkg-config RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.7 \ && cd z3 \ @@ -41,20 +54,21 @@ COPY --from=runtimeverificationinc/ocaml:ubuntu-bionic \ /home/user/.opam \ /home/user/.opam - -# This is where the rest of the dependencies go. -ENV DEPS_DIR="/home/user/c-semantics-deps" - ############ # Build K. # ############ +# This is where the rest of the dependencies go. +ENV DEPS_DIR="/home/user/c-semantics-deps" +ENV PATH="${DEPS_DIR}/k/llvm-backend/src/main/native/llvm-backend/build/bin:${PATH}" +ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin" + COPY --chown=user:user ./.build/k/ ${DEPS_DIR}/k RUN cd ${DEPS_DIR}/k \ - && mvn package -q -U \ + && mvn package -e -q -U \ -DskipTests -DskipKTest \ - -Dhaskell.backend.skip -Dllvm.backend.skip \ - -Dcheckstyle.skip + -Dhaskell.backend.skip \ + -Dcheckstyle.skip \ + -Dproject.build.type=FastBuild -ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin" From b9cd90aca6bf43e3d5493b684d5c0f54623e981c Mon Sep 17 00:00:00 2001 From: chathhorn Date: Thu, 29 Aug 2019 19:05:36 -0500 Subject: [PATCH 03/84] Jenkinsfile: disable rule parse profiling. --- Jenkinsfile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index 97d6576d9..bd36c62d9 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -34,13 +34,13 @@ pipeline { eval $(opam config env) eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib) export KOMPILE_FLAGS=-O2 - make -j4 profile-rule-parsing --output-sync=line + make -j4 --output-sync=line ''' } } } - post { success { - archiveArtifacts 'dist/timelogs.d/timelogs.csv' - } } + // post { success { + // archiveArtifacts 'dist/timelogs.d/timelogs.csv' + // } } } stage ( 'Re-compile w/ timeout' ) { steps { timeout(time: 8, unit: 'SECONDS' ) { From 2200763af2b12a5f1b86bb0e58a7e5de18a79367 Mon Sep 17 00:00:00 2001 From: chathhorn Date: Thu, 19 Sep 2019 11:38:41 -0500 Subject: [PATCH 04/84] Jenkinsfile: remove parse profiling. --- Jenkinsfile | 3 --- 1 file changed, 3 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index bd36c62d9..4aa386f85 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -38,9 +38,6 @@ pipeline { ''' } } } - // post { success { - // archiveArtifacts 'dist/timelogs.d/timelogs.csv' - // } } } stage ( 'Re-compile w/ timeout' ) { steps { timeout(time: 8, unit: 'SECONDS' ) { From afb5e1255d55929cd6b8c697711ae612731bafcf Mon Sep 17 00:00:00 2001 From: chathhorn Date: Tue, 22 Oct 2019 15:55:08 -0500 Subject: [PATCH 05/84] Enable kore output for C++ parser. --- scripts/kcc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/kcc b/scripts/kcc index 27d09d3aa..f083888d3 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -603,7 +603,7 @@ sub parse { push(@cppParserArgs, '-fno-diagnostics-color'); } - shell($cppParser, $ppResult, '--', @cppParserArgs)->verbose()->stdout($kast)->run(); + shell($cppParser, $ppResult, '--kore', '--', @cppParserArgs)->verbose()->stdout($kast)->run(); return $kast; } From 5b609e4543314209281a0d136bc3556f626125c0 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 6 Feb 2020 16:22:11 +0100 Subject: [PATCH 06/84] generate readable dumps --- scripts/RV_Kcc/Shell.pm | 32 ++++++++++++++++++++++++-------- scripts/kcc | 7 ++++--- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/scripts/RV_Kcc/Shell.pm b/scripts/RV_Kcc/Shell.pm index 2590be447..67fc5bcfd 100644 --- a/scripts/RV_Kcc/Shell.pm +++ b/scripts/RV_Kcc/Shell.pm @@ -11,12 +11,12 @@ use File::Spec::Functions qw(catfile); use String::ShellQuote qw(shell_quote_best_effort); use Exporter; -use RV_Kcc::Files qw(tempFile kBinDir IS_CYGWIN); +use RV_Kcc::Files qw(profileDir tempFile kBinDir IS_CYGWIN); use constant NULL => '/dev/null'; -use constant KBIN2TEXT => do { - my $path = kBinDir('k-bin-to-text'); +use constant KAST => do { + my $path = kBinDir('kast'); my $ext = IS_CYGWIN? '.bat' : ''; $path . $ext; }; @@ -30,6 +30,7 @@ our @EXPORT_OK = qw( enableDebugging saveArgv setShellDebugFile + setLanguageDefinition shell debug ); @@ -48,18 +49,24 @@ sub debug { } } -sub shell { - my ($cmd, @args) = @_; +sub shell_ex { + my ($out, $err, $cmd, @args) = @_; my $self = { CMD => $cmd , ARGS => \@args - , STDOUT => NULL - , STDERR => NULL + , STDOUT => $out + , STDERR => $err , TMP => '' }; return (bless $self); } +sub shell { + my ($cmd, @args) = @_; + return shell_ex(NULL, NULL, $cmd, @args) + +} + sub verbose { my ($self) = @_; $self->{STDOUT} = ''; @@ -167,11 +174,20 @@ sub commandName { ($debugFile, $isBinary) = @_; } + my $languageDefinition; + sub setLanguageDefinition { + ($languageDefinition) = @_; + } + sub checkError { my ($retval) = @_; if ($retval) { if ($debugFile && $isBinary) { - shell(KBIN2TEXT, $debugFile, 'kcc_config')->result(); + shell_ex('kcc_config', NULL, KAST, + '-i', 'kore', + '-o', 'pretty', + '-d', $languageDefinition, + $debugFile)->result(); } elsif ($debugFile) { copy($debugFile, 'kcc_config'); } diff --git a/scripts/kcc b/scripts/kcc index f083888d3..b8be378fc 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -20,7 +20,7 @@ use RV_Kcc::Opts qw( cppArgs suppressions ifdefs ldArgs nativeObjFiles srcFiles objFiles trampolineFiles breakpoints RVMAIN BASE_LIBS MAGIC ); -use RV_Kcc::Shell qw(shell checkError setShellDebugFile saveArgv debug); +use RV_Kcc::Shell qw(shell checkError setShellDebugFile setLanguageDefinition saveArgv debug); # Here we trap control-c (and others) so we can clean up when that happens. $SIG{'ABRT'} = 'interruptHandler'; @@ -512,8 +512,8 @@ sub getTranslationCommand { my $cTransDef = profileDir("c-translation-kompiled"); my $cppTransDef = profileDir("cpp-translation-kompiled"); - my @krun = getKRunCommand($output, - $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled'); + my $def = $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled'; + my @krun = getKRunCommand($output, $def); if (arg('-ftranslation-depth=')) { push(@krun, '--depth'); @@ -533,6 +533,7 @@ sub getTranslationCommand { my $kast = parse($src, $lang, $trampolines); @krun = addArg("PGM", $kast, 'KItem', 'korefile', @krun); + setLanguageDefinition(profileDir($def)); setShellDebugFile($output, 1); return @krun; } From 03fc20461e72a3ead8d45948bf1c6fbbd1110abd Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 6 Feb 2020 16:43:01 +0100 Subject: [PATCH 07/84] llvm-krun -save-temps --- scripts/kcc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/kcc b/scripts/kcc index b8be378fc..d17ddef6e 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -429,6 +429,9 @@ sub getKRunCommand { , $dir , '--output-file', $output ); + if (arg('-d')) { + push(@krun, '-save-temps'); + } } else { @krun = ( KRUN From 2d91b87ff84012cc07c6a5f07bc69bb7684c681b Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 2 Mar 2020 13:03:39 +0100 Subject: [PATCH 08/84] kcc -fdebug-translation --- scripts/RV_Kcc/Opts.pm | 1 + scripts/kcc | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/scripts/RV_Kcc/Opts.pm b/scripts/RV_Kcc/Opts.pm index 30f4e3fce..67f047445 100644 --- a/scripts/RV_Kcc/Opts.pm +++ b/scripts/RV_Kcc/Opts.pm @@ -447,6 +447,7 @@ sub parseOpts { for GCC. { RV_Kcc::Opts::pushArg('cppArgs', "-d$chars"); } -ftranslation-depth= Compile program up to a given depth. [undocumented] + -fdebug-translation Run translation semantics with GDB. [undocumented] -flinking-depth= Link program up to a given depth. [undocumented] -fmessage-length=0 Write all error messages on a single line. -frunner-script Compile program to perl script with analysis tool options. [undocumented] diff --git a/scripts/kcc b/scripts/kcc index d17ddef6e..759ad4bd6 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -523,6 +523,10 @@ sub getTranslationCommand { push(@krun, arg('-ftranslation-depth=')); } + if (arg('-fdebug-translation')) { + push(@krun, '--debug'); + } + my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING); my $json = "\\dv{SortString{}}($rvErrorJson)"; From 3861e0285d754c8bab4849a6cd46f3ae23466fb0 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 5 Mar 2020 11:39:18 +0100 Subject: [PATCH 09/84] append sorts to symbols --- clang-tools/ClangKast/GetKastVisitor.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index a20f52e45..f4aab809c 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -266,7 +266,7 @@ class GetKastVisitor bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) { if (!info) { if (decl == 0) { - Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME)); + Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME)); } else { Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING})); VisitUnsigned((unsigned long long)decl); @@ -1503,7 +1503,7 @@ class GetKastVisitor switch (Kind) { #define OVERLOADED_OPERATOR(Name,Spelling,Token,Unary,Binary,MemberOnly) \ case OO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; #include "clang/Basic/OperatorKinds.def" default: @@ -1515,7 +1515,7 @@ class GetKastVisitor switch (Kind) { #define UNARY_OP(Name, Spelling) \ case UO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; UNARY_OP(PostInc, "_++") UNARY_OP(PostDec, "_--") @@ -1548,7 +1548,7 @@ class GetKastVisitor switch (Kind) { #define BINARY_OP(Name, Spelling) \ case BO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; BINARY_OP(PtrMemD, ".*") BINARY_OP(PtrMemI, "->*") @@ -2250,7 +2250,7 @@ class GetKastVisitor VisitUnsigned(presumed.getColumn()); VisitBool(mgr.isInSystemHeader(loc)); } else { - Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC)); + Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC)); } } From e55a48724ebbe35a202d0ac528e809658074e01a Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 5 Mar 2020 14:20:59 +0100 Subject: [PATCH 10/84] fix lookupEnumerator --- .build/k | 2 +- semantics/cpp/language/translation/name.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.build/k b/.build/k index 748a6d579..739907788 160000 --- a/.build/k +++ b/.build/k @@ -1 +1 @@ -Subproject commit 748a6d57943317c0470eb8a136c205fd4da3029f +Subproject commit 739907788e2aa66cf90ea5ef008d9455dd91682f diff --git a/semantics/cpp/language/translation/name.k b/semantics/cpp/language/translation/name.k index 5cf49244c..e6ce9d522 100644 --- a/semantics/cpp/language/translation/name.k +++ b/semantics/cpp/language/translation/name.k @@ -261,7 +261,7 @@ module CPP-TRANSLATION-NAME ... X |-> V::PRVal requires variable in Mask - rule lookupEnumerator(X::CId, E::Enum, Mask::Set, C:K) => #if C ==K .K #then prv(V, Tr, ET) #else classSet(prv(V, Tr, ET), {C}:>Class :: X, SetItem({C}:>Class)) #fi ... + rule lookupEnumerator(X::CId, E::Enum, Mask::Set, C:K) => #if C ==K .K #then {prv(V, Tr, ET)}:>KItem #else {classSet(prv(V, Tr, ET), {C}:>Class :: X, SetItem({C}:>Class))}:>KItem #fi ... Sc::Scope E ET::CPPType From 05422b760bff1c14af9c006b0fced679f800de3c Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 5 Mar 2020 11:39:29 +0100 Subject: [PATCH 11/84] fix --- semantics/cpp/language/common/dynamic.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index 5568d60d8..efcaad533 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -273,8 +273,8 @@ module CPP-QUALID-SYNTAX imports CPP-QUALID-SORTS // self imports CPP-SORTS // CId, Name - syntax NNS ::= NoNNS() - | NNS "::" NNSSpecifier [klabel(NestedName)] + syntax NNS ::= NoNNS() [symbol] + | NNS "::" NNSSpecifier [klabel(NestedName), symbol] syntax NNSSpecifier ::= NNS(CId) | TemplateNNS(CId) From ed473827a94c4ea5082eff4824d9b099308c59fb Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 13 Mar 2020 11:04:13 +0100 Subject: [PATCH 12/84] rename isNoInit => hasInit --- semantics/cpp/language/translation/decl/initializer.k | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k index 502e4e6b6..bb5b8583b 100644 --- a/semantics/cpp/language/translation/decl/initializer.k +++ b/semantics/cpp/language/translation/decl/initializer.k @@ -326,13 +326,13 @@ module CPP-TRANSLATION-DECL-INITIALIZER syntax Bool ::= hasInit(CId, Map) [function] - rule hasInit(X:CId, X |-> M::Map _) => notBool isNoInit(M) + rule hasInit(X:CId, X |-> M::Map _) => notBool hasNoInit(M) - syntax Bool ::= isNoInit(Map) [function] + syntax Bool ::= hasNoInit(Map) [function] - rule isNoInit(_ |-> (_, NoInit())) => true + rule hasNoInit(_ |-> (_, NoInit())) => true - rule isNoInit(_ |-> _) => false [owise] + rule hasNoInit(_ |-> _) => false [owise] syntax Expr ::= classAggInit(base: LVal, fields: List, initList: List, initializers: Map, class: Class, initExp: K, ctype: ConstructorType, duration: Duration) From b291263ad8b273333d721827aa57a2dd6ba18dda Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 13 Mar 2020 14:10:23 +0100 Subject: [PATCH 13/84] Revert "append sorts to symbols" This reverts commit bb1a33f03aa2d6c4b0992c78e4cc84e59825732a. --- clang-tools/ClangKast/GetKastVisitor.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index f4aab809c..a20f52e45 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -266,7 +266,7 @@ class GetKastVisitor bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) { if (!info) { if (decl == 0) { - Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME)); + Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME)); } else { Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING})); VisitUnsigned((unsigned long long)decl); @@ -1503,7 +1503,7 @@ class GetKastVisitor switch (Kind) { #define OVERLOADED_OPERATOR(Name,Spelling,Token,Unary,Binary,MemberOnly) \ case OO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ break; #include "clang/Basic/OperatorKinds.def" default: @@ -1515,7 +1515,7 @@ class GetKastVisitor switch (Kind) { #define UNARY_OP(Name, Spelling) \ case UO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ break; UNARY_OP(PostInc, "_++") UNARY_OP(PostDec, "_--") @@ -1548,7 +1548,7 @@ class GetKastVisitor switch (Kind) { #define BINARY_OP(Name, Spelling) \ case BO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ break; BINARY_OP(PtrMemD, ".*") BINARY_OP(PtrMemI, "->*") @@ -2250,7 +2250,7 @@ class GetKastVisitor VisitUnsigned(presumed.getColumn()); VisitBool(mgr.isInSystemHeader(loc)); } else { - Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC)); + Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC)); } } From 18f40a9dc1c94686a3c0c1868a888be40038ec5a Mon Sep 17 00:00:00 2001 From: chathhorn Date: Tue, 22 Oct 2019 17:52:32 -0500 Subject: [PATCH 14/84] C++ semantics [symbol] tags. --- semantics/cpp/language/translation/syntax.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index e59c97ec8..8e386dd4c 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -191,7 +191,7 @@ module CPP-ABSTRACT-SYNTAX | ForTStmt(Stmt, Decl, Stmt, Stmt) | ForTStmt(Expr, Stmt, Stmt) | TemplateDefinitionStmt(K) [symbol] // synthetic statement created by the body of a function template definition when it's evaluted before instantiation - | TReturnOp(init: Expr, obj: K) + | TReturnOp(init: Expr, obj: K) [symbol] syntax AStmt ::= NoStatement() [symbol] | CompoundAStmt(List) [symbol] From ee06607e138ec8417cb4b7f805f1261a8f68b608 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 27 Mar 2020 11:37:52 +0100 Subject: [PATCH 15/84] update K --- .build/k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.build/k b/.build/k index 739907788..51686b228 160000 --- a/.build/k +++ b/.build/k @@ -1 +1 @@ -Subproject commit 739907788e2aa66cf90ea5ef008d9455dd91682f +Subproject commit 51686b228230341d0fb851767734ed44d88ecfcb From b8e640b14cea6dd2cf66b80af23226c30479cac0 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 27 Mar 2020 11:39:18 +0100 Subject: [PATCH 16/84] llvm debug --- semantics/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/semantics/Makefile b/semantics/Makefile index 1143222d4..3ebc11bd2 100644 --- a/semantics/Makefile +++ b/semantics/Makefile @@ -27,6 +27,7 @@ KOMPILE_FLAGS += --no-prelude KOMPILE_FLAGS += -w all KOMPILE_FLAGS += -v KOMPILE_FLAGS += --debug +KOMPILE_FLAGS += -ccopt -g # Used specifically in the timestamp_of rules. From a718f5e1eb0b8ee6347cb37101d09a5806af3926 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 25 Mar 2020 11:27:19 +0100 Subject: [PATCH 17/84] UnknownCabsLoc --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index a20f52e45..3f2b4bf50 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -2250,7 +2250,7 @@ class GetKastVisitor VisitUnsigned(presumed.getColumn()); VisitBool(mgr.isInSystemHeader(loc)); } else { - Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC)); + Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC)); } } From d6af82b50039cbdf33e4ac5f61678929780f29a4 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 1 Apr 2020 11:50:04 +0200 Subject: [PATCH 18/84] workaround for K bug https://github.com/kframework/k/issues/1193 --- semantics/common/configuration.k | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/semantics/common/configuration.k b/semantics/common/configuration.k index 7ecccd4be..a482f4cc5 100644 --- a/semantics/common/configuration.k +++ b/semantics/common/configuration.k @@ -6,6 +6,9 @@ module COMMON-CONFIGURATION imports STRING-SYNTAX imports COMMON-SYNTAX + syntax Enum ::= DummyEnum() + syntax Class ::= DummyClass() + configuration .Map @@ -101,7 +104,7 @@ module COMMON-CONFIGURATION - .K + DummyClass() .K true .List @@ -127,7 +130,7 @@ module COMMON-CONFIGURATION - .K + DummyEnum() .K false .Map From 28cb90a4c3d7a6a32d7b64a53cef36e882e80d6f Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 1 Apr 2020 17:58:42 +0200 Subject: [PATCH 19/84] C++ parser: toplevel sort is KItem --- clang-tools/ClangKast/ClangKast.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/ClangKast.cc b/clang-tools/ClangKast/ClangKast.cc index bed0c41aa..99ecb3cb7 100644 --- a/clang-tools/ClangKast/ClangKast.cc +++ b/clang-tools/ClangKast/ClangKast.cc @@ -330,7 +330,7 @@ void Kast::add(const T & node) { Kast::Nodes.push_back(make_unique(node)); } -void Kast::print() { print(Sort::K, 0); } +void Kast::print() { print(Sort::KITEM, 0); } int Kast::print(Sort parentSort, int idx) { if (!Nodes[idx]) throw logic_error("parse error"); From 1a8cdb4d1ab8f1b2b8bd37f8b100ea94cbaa5ad1 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 2 Apr 2020 11:38:48 +0200 Subject: [PATCH 20/84] C++ parser #NoName --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 3f2b4bf50..866ec352f 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -266,7 +266,7 @@ class GetKastVisitor bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) { if (!info) { if (decl == 0) { - Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME)); + Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME)); } else { Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING})); VisitUnsigned((unsigned long long)decl); From aad43ba665fabe4fff759c5599ba208d075739dc Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Tue, 7 Apr 2020 12:58:58 +0200 Subject: [PATCH 21/84] [symbol] --- semantics/cpp/language/common/syntax.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/common/syntax.k b/semantics/cpp/language/common/syntax.k index df833af66..8e12b0bbe 100644 --- a/semantics/cpp/language/common/syntax.k +++ b/semantics/cpp/language/common/syntax.k @@ -103,7 +103,7 @@ module CPP-SYNTAX syntax AccessSpecifier ::= Public() [symbol] | Private() [symbol] | Protected() [symbol] | NoAccessSpec() - syntax RefQualifier ::= RefLValue() | RefRValue() | RefNone() + syntax RefQualifier ::= RefLValue() [symbol] | RefRValue() [symbol] | RefNone() [symbol] syntax TemplateKeyword ::= "template" | "no-template" @@ -205,7 +205,7 @@ module CPP-SYNTAX syntax Decl syntax Stmt ::= LabelStmt(CId, List) - | GotoStmt(CId) + | GotoStmt(CId) [symbol] | ExpressionStmt(Expr) [strict(c)] | PRValExpressionStmt(Expr) [strict(c)] | BreakStmt() From df184b41de3690f674a37bb4ba3d4d87d63caa2d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Tue, 7 Apr 2020 11:34:19 +0200 Subject: [PATCH 22/84] remove overloaded ExprLoc so that the parser to Kore does not need to choose the right overload --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- semantics/cpp/language/common/dynamic.k | 10 +++++++ semantics/cpp/language/common/syntax.k | 6 ++-- .../cpp/language/execution/expr/expr-loc.k | 2 +- .../language/translation/decl/declarator.k | 10 +++---- .../language/translation/decl/initializer.k | 29 +++++++++++-------- .../language/translation/expr/conditional.k | 4 +-- semantics/cpp/language/translation/init.k | 2 +- semantics/cpp/language/translation/name.k | 4 +-- semantics/cpp/language/translation/syntax.k | 14 ++++++--- .../cpp/language/translation/typing/expr.k | 5 ++-- .../cpp/language/translation/value-category.k | 5 ++-- 12 files changed, 57 insertions(+), 36 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 866ec352f..76bd2cb87 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -62,7 +62,7 @@ class GetKastVisitor if (Expr *E = dyn_cast(S)) { if (!dyn_cast(S)) { - Kast::add(Kast::KApply("ExprLoc", Sort::EXPRLOC, {Sort::CABSLOC, Sort::EXPR})); + Kast::add(Kast::KApply("ExprLoc", Sort::EXPRLOC, {Sort::CABSLOC, Sort::KITEM})); CabsLoc(E->getExprLoc()); } } diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index efcaad533..ec813aaf6 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -575,6 +575,8 @@ module CPP-DYNAMIC-OTHER-SYNTAX syntax KItem ::= seqstrict(StrictList) [klabel(seqstrictcpp)] + syntax Bool ::= isSpuriousExpr(KItem) [function] + endmodule // CPP-DYNAMIC-OTHER-SYNTAX module CPP-DYNAMIC-OTHER @@ -1076,6 +1078,14 @@ module CPP-DYNAMIC-OTHER rule idOf(_ :: S::ClassSpecifier) => idOf(S) + rule isSpuriousExpr(ExprLoc(_, X::KItem) => X) + + rule isSpuriousExpr(X::KItem) => true + requires notBool isExpr(X) + + rule isSpuriousExpr(E:Expr) => false + requires ExprLoc(...) :/=K E + endmodule // CPP-DYNAMIC-OTHER // ------------------------------ diff --git a/semantics/cpp/language/common/syntax.k b/semantics/cpp/language/common/syntax.k index 8e12b0bbe..dd11ac12c 100644 --- a/semantics/cpp/language/common/syntax.k +++ b/semantics/cpp/language/common/syntax.k @@ -193,11 +193,9 @@ module CPP-SYNTAX syntax Expr ::= ConvertType(CPPType, Expr) | ExprLoc - syntax ExprLoc ::= ExprLoc(CabsLoc, Expr) + syntax ExprLoc ::= ExprLoc(CabsLoc, KItem) - syntax Init ::= ExprLoc(CabsLoc, Init) - - syntax BraceInit ::= ExprLoc(CabsLoc, BraceInit) + syntax Init ::= ExprLoc syntax Block ::= BlockStmt(List) | BlockStmt(Int, List) diff --git a/semantics/cpp/language/execution/expr/expr-loc.k b/semantics/cpp/language/execution/expr/expr-loc.k index 66b328d3c..b00193190 100644 --- a/semantics/cpp/language/execution/expr/expr-loc.k +++ b/semantics/cpp/language/execution/expr/expr-loc.k @@ -10,7 +10,7 @@ module CPP-EXECUTION-EXPR-EXPRLOC imports C-CONFIGURATION imports CPP-DYNAMIC-SYNTAX // Execution() - rule ExprLoc(L::CabsLoc, E::Expr) => #ExecExprLoc(L, E) ... + rule ExprLoc(L::CabsLoc, E:Expr) => #ExecExprLoc(L, E) ... _ => L requires Execution() diff --git a/semantics/cpp/language/translation/decl/declarator.k b/semantics/cpp/language/translation/decl/declarator.k index f426159ae..6cbc1c2f6 100644 --- a/semantics/cpp/language/translation/decl/declarator.k +++ b/semantics/cpp/language/translation/decl/declarator.k @@ -417,7 +417,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR syntax CPPType ::= completeDeclaration(CPPType, Init) [function] - rule completeDeclaration(T::CPPType, (ExprLoc(_, I::Init) => I)) + rule completeDeclaration(T::CPPType, (ExprLoc(_, I:Init) => I)) // @ref n4296 8.5.4:3.2 (char x[] = {"foo"}) rule completeDeclaration(t(Q::Quals, Mods::Set, incompleteArrayType(t(Q'::Quals, Mods'::Set, T:CPPSimpleCharType))), BraceInit(ListItem(StringLiteral(Narrow::CharKind, S::String)))) => t(Q, Mods, arrayType(t(Q', Mods', T), lengthString(S) +Int 1)) @@ -441,11 +441,11 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule completeDeclaration(t(Q::Quals, Mods::Set, incompleteArrayType(T::CPPType)), BraceInit(ListItem(Init::Init) L::List)) => t(Q, Mods, arrayType(T, size(L) +Int 1)) requires (size(L) =/=Int 0 orBool StringLiteral(...) :/=K Init) - andBool (notBool isAggregateType(T) orBool isBraceInit(Init)) + andBool (notBool isAggregateType(T) orBool #isBraceInit(Init)) rule completeDeclaration(t(Q::Quals, Mods::Set, incompleteArrayType(t(... st: classType(...)) #as T::CPPType)), BraceInit((ListItem(Init::Init) _) #as L::List)) => t(Q, Mods, arrayType(T, computeAggArraySize(getClassInfo(T), L))) requires isAggregateType(T) - andBool notBool isBraceInit(Init) + andBool notBool #isBraceInit(Init) rule completeDeclaration(T::CPPType, _) => T [owise] @@ -465,7 +465,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR types: (F |-> (_::CPPType |-> (T::CPPType, _))) _, initList: (ListItem(Init::Expr) => .List) _ ) - requires (notBool isAggregateType(T) orBool isBraceInit(Init)) + requires (notBool isAggregateType(T) orBool #isBraceInit(Init)) rule #computeAggArraySize(... fields: (ListItem(Class.DataMember(F:CId, _)) Fields::List => Class.getNonStaticDataMembers(getClassInfo(T))), @@ -474,7 +474,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR callStack: (.List => ListItem(kpair(Fields, Types))) _ ) requires isAggregateType(T) - andBool notBool isBraceInit(Init) + andBool notBool #isBraceInit(Init) syntax Decl ::= lazyDefineObject(NNSVal, CId, CId, CPPType, Init, DeclarationType, Set, SymBase) diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k index bb5b8583b..bedb547a7 100644 --- a/semantics/cpp/language/translation/decl/initializer.k +++ b/semantics/cpp/language/translation/decl/initializer.k @@ -79,9 +79,11 @@ module CPP-TRANSLATION-DECL-INITIALIZER context defaultInit(HOLE:Expr, _, _) [result(LVal)] - context #figureInit(... srcT: HOLE:TypeExpr => typeof(HOLE)) [result(CPPType)] + context #figureInit(... srcT: HOLE:TypeExpr => typeof(HOLE)) + requires notBool isSpuriousExpr(HOLE) [result(CPPType)] - context #figureInit(... srcCat: HOLE:CatExpr => catof(HOLE)) [result(ValueCategory)] + context #figureInit(... srcCat: HOLE:CatExpr => catof(HOLE)) + requires notBool isSpuriousExpr(HOLE) [result(ValueCategory)] rule #figureInit(Base::Expr, DestT::CPPType, IType::InitType, I::Init, SrcType::CPPType, SrcCat::ValueCategory, @@ -102,7 +104,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER syntax KItem ::= #figureInitHeatBase(destT: CPPType, type: InitType, init: Init, srcT: K, srcCat: K, ConstructorType, Duration) - rule #figureInit(... init: ExprLoc(L::CabsLoc, I::Init) => I) ... + rule #figureInit(... init: ExprLoc(L::CabsLoc, I:Init) => I) ... _ => L // @ref n4296 8.5:6.1 @@ -225,6 +227,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER // @ref n4296 8.5:17.2 (reference destination type) rule #figureInit(Base:LVal, cppRefType #as DestT::CPPType, _, E:Expr, _, _, _, D::Duration) => bindReference(Base, E, D) + requires ExprLoc(...) :/=K E // @ref n4296 8.5:17.3 (string literal) rule #figureInit(Base:LVal, t(... st: _:CPPSimpleArrayType) #as DestT::CPPType, _, StringLiteral(Kind::CharKind, S::String), _, _, _, _) @@ -239,7 +242,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER // @ref n4296 8.5:17.6.1 (direct init or copy init from derived class) rule #figureInit(Base:LVal, t(... st: classType(DestC::Class)) #as DestT::CPPType, Type::InitType, E:Expr, SrcT::CPPType, _, IsConstructor::ConstructorType, _) => constructorInit(Base, Type, DestC, ListItem(E), IsConstructor) - requires Type ==K DirectInit() orBool (isCPPClassType(SrcT) andBool isBaseClassOf(DestT, SrcT)) + requires ExprLoc(...) :/=K E andBool (Type ==K DirectInit() orBool (isCPPClassType(SrcT) andBool isBaseClassOf(DestT, SrcT))) rule #figureInit(Base:LVal, t(... st: classType(DestC::Class)), DirectInit(), ExpressionList(L::List), _, _, IsConstructor::ConstructorType, _) => constructorInit(Base, DirectInit(), DestC, L, IsConstructor) @@ -249,7 +252,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER // expression initializer, non-class type rule #figureInit(Base:LVal, DestT::CPPType, _, E:Expr, SrcT:CPPType, SrcCat:ValueCategory, _, _) => #if canConvertWithStandardConversion(DestT, SrcT, SrcCat) #then le(Base, trace(Base), DestT) :=init E #else ill-formed #fi - requires notBool isCPPRefType(DestT) andBool notBool isCPPArrayType(DestT) andBool notBool isCPPClassType(DestT) andBool notBool isCPPClassType(SrcT) + requires ExprLoc(...) :/=K E andBool notBool isCPPRefType(DestT) andBool notBool isCPPArrayType(DestT) andBool notBool isCPPClassType(DestT) andBool notBool isCPPClassType(SrcT) rule #figureInit(... base: lv(loc(Base::SymBase, _), _, _), init: S:Stmt) => functionDef(Base, S) @@ -368,7 +371,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER initializers: (F |-> (_::CPPType |-> (T::CPPType, _))) _, class: C::Class, duration: D::Duration) - requires (notBool isAggregateType(T) orBool isBraceInit(Init)) + requires (notBool isAggregateType(T) orBool #isBraceInit(Init)) rule (.K => #figureInit0(Base . no-template Name(C, F), T, CopyInit(), BraceInit(L), ConstructorInit(false), D)) @@ -379,7 +382,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER class: C::Class, duration: D::Duration) requires isAggregateType(T) - andBool notBool isBraceInit(Init) + andBool notBool #isBraceInit(Init) rule (classAggInit(... fields: .List, initList: L::List, initExp: E2::MaybeExpr) => .K) ~> classAggInit(... initList: .List => L, initExp: E1::MaybeExpr => compoundInitJoin(E1, E2)) @@ -414,7 +417,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER rule #evalBraceOrEqualInitializer(_, _, NoInit()) => BraceInit(.List) - rule #evalBraceOrEqualInitializer(_, _, ExprLoc(L::CabsLoc, I::Init) => I) + rule #evalBraceOrEqualInitializer(_, _, ExprLoc(L::CabsLoc, I:Init) => I) rule #evalBraceOrEqualInitializer(C::Class, Base::Expr, BraceInit(L::List)) => BraceInit(#evalBraceOrEqualInitializers(C, Base, L)) @@ -467,7 +470,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER current: I::Int, initList: ListItem(Init::Init) _ ) - requires (notBool isAggregateType(T) orBool isBraceInit(Init)) + requires (notBool isAggregateType(T) orBool #isBraceInit(Init)) andBool Size >Int I rule (.K => braceElisionMaybe(Init, T)) ~> @@ -476,7 +479,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER current: I::Int, initList: (ListItem(Init::Init) _) #as L::List ) - requires notBool isBraceInit(Init) + requires notBool #isBraceInit(Init) andBool isAggregateType(T) andBool Size >Int I @@ -489,9 +492,11 @@ module CPP-TRANSLATION-DECL-INITIALIZER // If the initializer is neither BraceInit nor Expr, then this rule may not apply. rule braceElisionMaybe(E:Expr, T::CPPType) => braceElisionMaybe2(E, E, E, T) - context braceElisionMaybe2(... initType: (HOLE:TypeExpr => typeof(HOLE))) [result(CPPDType)] + context braceElisionMaybe2(... initType: (HOLE:TypeExpr => typeof(HOLE))) + requires notBool isSpuriousExpr(HOLE) [result(CPPDType)] - context braceElisionMaybe2(... initCat: (HOLE:CatExpr => catof(HOLE))) [result(ValueCategory)] + context braceElisionMaybe2(... initCat: (HOLE:CatExpr => catof(HOLE))) + requires notBool isSpuriousExpr(HOLE) [result(ValueCategory)] rule braceElisionMaybe2(... init: From::Expr, diff --git a/semantics/cpp/language/translation/expr/conditional.k b/semantics/cpp/language/translation/expr/conditional.k index 897fbc20d..34a394620 100644 --- a/semantics/cpp/language/translation/expr/conditional.k +++ b/semantics/cpp/language/translation/expr/conditional.k @@ -44,9 +44,9 @@ module CPP-TRANSLATION-EXPR-CONDITIONAL syntax KItem ::= typeAndCatOfConditional(Expr, TypeExpr, CatExpr, Expr, TypeExpr, CatExpr) [klabel(typeAndCatOfConditional0)] - rule typeAndCatOfConditional(ExprLoc(_, E::Expr) => E, _) + rule typeAndCatOfConditional(ExprLoc(_, E:Expr) => E, _) - rule typeAndCatOfConditional(_, ExprLoc(_, E::Expr) => E) + rule typeAndCatOfConditional(_, ExprLoc(_, E:Expr) => E) rule typeAndCatOfConditional(E1::Expr, E2::Expr) => typeAndCatOfConditional(E1, E1, E1, E2, E2, E2) [owise] diff --git a/semantics/cpp/language/translation/init.k b/semantics/cpp/language/translation/init.k index c58ef88b6..224456229 100644 --- a/semantics/cpp/language/translation/init.k +++ b/semantics/cpp/language/translation/init.k @@ -76,7 +76,7 @@ module CPP-TRANSLATION-INIT _ => L requires Execution() - rule ExprLoc(L::CabsLoc, E::Expr) => #ExprLoc(L, E) ... + rule ExprLoc(L::CabsLoc, E:Expr) => #ExprLoc(L, E) ... _ => L requires Translation() diff --git a/semantics/cpp/language/translation/name.k b/semantics/cpp/language/translation/name.k index e6ce9d522..4c34b09e1 100644 --- a/semantics/cpp/language/translation/name.k +++ b/semantics/cpp/language/translation/name.k @@ -379,7 +379,7 @@ module CPP-TRANSLATION-NAME rule (.K => argDependentNameLookup(X, Args)) ~> CallExpr(Name(NoNNS(), X::CId), Args::StrictList, krlist(.List)) - rule CallExpr((ExprLoc(L::CabsLoc, E::Expr) => E), Args::StrictList, krlist(.List)) ... + rule CallExpr((ExprLoc(L::CabsLoc, E:Expr) => E), Args::StrictList, krlist(.List)) ... _ => L context CallExpr(Name(HOLE:NNS, _), _, _) @@ -431,7 +431,7 @@ module CPP-TRANSLATION-NAME context & HOLE:Expr requires notBool isName(HOLE) andBool notBool isExprLoc(HOLE) - rule & (ExprLoc(L::CabsLoc, E::Expr) => E) ... + rule & (ExprLoc(L::CabsLoc, E:Expr) => E) ... _ => L rule ElaboratedTypeSpecifier(T::Tag, X::CId, NoNNS()) => resolveElabSpecifier(T, nameLookup(X, T, typeMask)) diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index 8e386dd4c..e390f2eac 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -270,9 +270,7 @@ module CPP-ABSTRACT-SYNTAX | UTF16() [symbol] | UTF32() [symbol] - syntax BraceInit ::= BraceInit(List) [symbol] - - syntax Init ::= BraceInit + syntax Init ::= BraceInit(List) [symbol] syntax ExpressionList ::= ExpressionList(List) [symbol] @@ -292,6 +290,8 @@ module CPP-ABSTRACT-SYNTAX syntax AStmt ::= StmtLoc(CabsLoc, AStmt) [symbol] + syntax Bool ::= "#isBraceInit" "(" KItem ")" [function] + endmodule module CPP-TRANSLATION-ABSTRACT-REWRITING @@ -313,7 +313,7 @@ module CPP-TRANSLATION-ABSTRACT-REWRITING syntax Bool ::= hasAnonymousUnionObject(Expr) [function] - rule hasAnonymousUnionObject(ExprLoc(_, E::Expr) => E) + rule hasAnonymousUnionObject(ExprLoc(_, E:Expr) => E) rule hasAnonymousUnionObject(Name(NoNNS(), #NoName)) => true @@ -344,4 +344,10 @@ module CPP-TRANSLATION-ABSTRACT-REWRITING context IfTStmt((HOLE:Expr => reval(HOLE)), _, _) [result(PRVal)] + rule #isBraceInit(ExprLoc(_, X::KItem) => X) + + rule #isBraceInit(BraceInit(_)) => true + + rule #isBraceInit(_) => false [owise] + endmodule diff --git a/semantics/cpp/language/translation/typing/expr.k b/semantics/cpp/language/translation/typing/expr.k index b49a53bbc..b5f08d812 100644 --- a/semantics/cpp/language/translation/typing/expr.k +++ b/semantics/cpp/language/translation/typing/expr.k @@ -71,13 +71,14 @@ module CPP-TRANSLATION-TYPING-EXPR syntax KResult ::= NoInitType - context (HOLE:TypeExpr => typeof(HOLE)) types:: _ [result(CPPDType)] + context (HOLE:TypeExpr => typeof(HOLE)) types:: _ + requires notBool isSpuriousExpr(HOLE) [result(CPPDType)] context K:KResult types:: HOLE:STypeList // ---------------------------------- - rule typeof(ExprLoc(_, E::Expr) => E) + rule typeof(ExprLoc(_, E:Expr) => E) rule typeof(StringLiteral(Ascii(), S::String) => type(arrayType(const(char), lengthString(S) +Int 1))) diff --git a/semantics/cpp/language/translation/value-category.k b/semantics/cpp/language/translation/value-category.k index 90c420626..689125280 100644 --- a/semantics/cpp/language/translation/value-category.k +++ b/semantics/cpp/language/translation/value-category.k @@ -64,13 +64,14 @@ module CPP-TRANSLATION-VALUE-CATEGORY rule (NoInit() => NoInitCat()) cats:: _ - context (HOLE:CatExpr => catof(HOLE)) cats:: _ [result(ValueCategory)] + context (HOLE:CatExpr => catof(HOLE)) cats:: _ + requires notBool isSpuriousExpr(HOLE) [result(ValueCategory)] context K:KResult cats:: HOLE:SCatList // -------------------------------- - rule catof(ExprLoc(_, E::Expr) => E) + rule catof(ExprLoc(_, E:Expr) => E) rule catof(StringLiteral(_, _) => lvalue) From 01944f2ad1b810436bee554c9c5cf2319f3930c4 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 9 Apr 2020 13:31:01 +0200 Subject: [PATCH 23/84] C++ [symbol] --- clang-tools/ClangKast/GetKastVisitor.h | 9 ++++----- semantics/common/compat.k | 2 +- semantics/common/syntax.k | 2 +- semantics/cpp/language/common/class.k | 2 +- semantics/cpp/language/common/dynamic.k | 4 ++-- semantics/cpp/language/common/syntax.k | 10 +++++----- 6 files changed, 14 insertions(+), 15 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 76bd2cb87..0fe46403d 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -224,22 +224,21 @@ class GetKastVisitor Kast::add(Kast::KApply("NestedName", Sort::NNS, {Sort::NNS, Sort::NNSSPECIFIER})); TRY_TO(TraverseNestedNameSpecifier(NNS->getPrefix())); } - auto nns = Kast::KApply("NNS", Sort::NNSSPECIFIER, {Sort::CID}); switch (NNS->getKind()) { case NestedNameSpecifier::Identifier: - Kast::add(nns); + Kast::add(Kast::KApply("NNSCId", Sort::NNSSPECIFIER, {Sort::CID})); TRY_TO(TraverseIdentifierInfo(NNS->getAsIdentifier())); break; case NestedNameSpecifier::Namespace: - Kast::add(nns); + Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME})); TRY_TO(TraverseDeclarationName(NNS->getAsNamespace()->getDeclName())); break; case NestedNameSpecifier::NamespaceAlias: - Kast::add(nns); + Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME})); TRY_TO(TraverseDeclarationName(NNS->getAsNamespaceAlias()->getDeclName())); break; case NestedNameSpecifier::TypeSpec: - Kast::add(nns); + Kast::add(Kast::KApply("NNSCId", Sort::NNSSPECIFIER, {Sort::CID})); TRY_TO(TraverseType(QualType(NNS->getAsType(), 0))); break; case NestedNameSpecifier::TypeSpecWithTemplate: diff --git a/semantics/common/compat.k b/semantics/common/compat.k index 792c58016..7dcde9d3b 100644 --- a/semantics/common/compat.k +++ b/semantics/common/compat.k @@ -28,7 +28,7 @@ module COMPAT-SYNTAX syntax List ::= removeListItem(List, K) [function] - syntax StrictListResult ::= krlist(List) + syntax StrictListResult ::= krlist(List) [symbol] syntax StrictList ::= StrictListResult syntax KResult ::= StrictListResult diff --git a/semantics/common/syntax.k b/semantics/common/syntax.k index 7e9acf661..b1d24cc20 100644 --- a/semantics/common/syntax.k +++ b/semantics/common/syntax.k @@ -52,7 +52,7 @@ module COMMON-SYNTAX syntax Bool ::= Quals "<=Quals" Quals [function] syntax Bool ::= Quals ">Quals" Quals [function] - syntax Namespace ::= GlobalNamespace() + syntax Namespace ::= GlobalNamespace() [symbol] syntax Scope ::= "none" | FileScope syntax FileScope ::= "fileScope" diff --git a/semantics/cpp/language/common/class.k b/semantics/cpp/language/common/class.k index f7508ac93..0d28e5ff1 100644 --- a/semantics/cpp/language/common/class.k +++ b/semantics/cpp/language/common/class.k @@ -171,7 +171,7 @@ module CPP-CLASS-SYNTAX syntax KItem ::= returnFromBraceOrEqualInitializer(LVal, Scope) - syntax This ::= This() + syntax This ::= This() [symbol] syntax Expr ::= This diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index ec813aaf6..0042a023b 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -276,9 +276,9 @@ module CPP-QUALID-SYNTAX syntax NNS ::= NoNNS() [symbol] | NNS "::" NNSSpecifier [klabel(NestedName), symbol] - syntax NNSSpecifier ::= NNS(CId) + syntax NNSSpecifier ::= NNS(CId) [klabel(NNSCId), symbol] | TemplateNNS(CId) - | NNS(Name) + | NNS(Name) [klabel(NNSName), symbol] syntax QualId ::= NNSVal "::" CId [klabel(QualId)] diff --git a/semantics/cpp/language/common/syntax.k b/semantics/cpp/language/common/syntax.k index dd11ac12c..3233c2ce6 100644 --- a/semantics/cpp/language/common/syntax.k +++ b/semantics/cpp/language/common/syntax.k @@ -117,8 +117,8 @@ module CPP-SYNTAX | Expr "++" [strict(c)] | Expr "--" [strict(c)] | BuiltinCallOp(Expr, Bool, List) - | ReinterpretCast(AType, Expr) [strict(c)] - | ConstCast(AType, Expr) [strict(c)] + | ReinterpretCast(AType, Expr) [strict(c), symbol] + | ConstCast(AType, Expr) [strict(c), symbol] > right: "++" Expr [strict(c)] | "--" Expr [strict(c)] @@ -183,8 +183,8 @@ module CPP-SYNTAX | ThrowOp(Expr) [strict(c)] > left: Comma(Expr, Expr) [strict(c; 1)] - syntax Name ::= Name(NNS, CId) - | Name(NNS, CId, List) + syntax Name ::= Name(NNS, CId) [symbol] + | Name(NNS, CId, List) [klabel(Name3)] syntax ExecName ::= ExecName(NNS, CId) @@ -193,7 +193,7 @@ module CPP-SYNTAX syntax Expr ::= ConvertType(CPPType, Expr) | ExprLoc - syntax ExprLoc ::= ExprLoc(CabsLoc, KItem) + syntax ExprLoc ::= ExprLoc(CabsLoc, KItem) [symbol] syntax Init ::= ExprLoc From f88d3b357e12bbfa280367d7a6fa3925752369b2 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 9 Apr 2020 17:22:08 +0200 Subject: [PATCH 24/84] fix toCPPTypes --- semantics/cpp/language/common/dynamic.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index 0042a023b..aec367f99 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -779,7 +779,7 @@ module CPP-DYNAMIC-OTHER rule toTemplateArgs(.List) => .TemplateArgs - rule toCPPTypes(ListItem(A::CPPType) L::List) => A, toCPPTypes(L) + rule toCPPTypes(ListItem(A::CPPDType) L::List) => A, toCPPTypes(L) rule toCPPTypes(.List) => .CPPTypes From 5ffaa5247e0e2a272d65d40ec4c34f0abeb9a2f4 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 9 Apr 2020 20:32:16 +0200 Subject: [PATCH 25/84] fix sorts --- semantics/cpp/language/translation/decl/declarator.k | 8 ++++---- semantics/cpp/language/translation/syntax.k | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/semantics/cpp/language/translation/decl/declarator.k b/semantics/cpp/language/translation/decl/declarator.k index 6cbc1c2f6..5d3600bd3 100644 --- a/semantics/cpp/language/translation/decl/declarator.k +++ b/semantics/cpp/language/translation/decl/declarator.k @@ -53,13 +53,13 @@ module CPP-TRANSLATION-DECL-DECLARATOR imports CPP-TRANSLATION-CONSTANT-SYNTAX imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR - rule FunctionDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List) + rule FunctionDecl(N::NNS, X::CId, Mangled::CId, T::AType, Params::List) => NormalizedDecl(N, X, Mangled, T, NoInit(), Function(Params)) [anywhere] - rule VarDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Init::Init, IsDirect:Bool) + rule VarDecl(N::NNS, X::CId, Mangled::CId, T::AType, Init::Init, IsDirect:Bool) => NormalizedDecl(N, X, Mangled, T, Init, Var(#if IsDirect #then DirectInit() #else CopyInit() #fi)) [anywhere] - rule FunctionDefinition(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List, Body::Stmt) + rule FunctionDefinition(N::NNS, X::CId, Mangled::CId, T::AType, Params::List, Body::Stmt) => NormalizedDecl(N, X, Mangled, T, Body, Function(Params)) [anywhere] rule DeclStmt(L::List) => listToK(L) @@ -72,7 +72,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule Specifier(Spec::Specifier, DeclaratorAndSpecifiers(D::Declarator, S::Set)) => DeclaratorAndSpecifiers(D, S SetItem(Spec)) [anywhere] - rule NormalizedDecl(N::NNSVal, X::CId, Mangled::CId, T::AType, Init::Init, Type::DeclarationType) + rule NormalizedDecl(N::NNS, X::CId, Mangled::CId, T::AType, Init::Init, Type::DeclarationType) => DeclaratorAndSpecifiers(NormalizedDecl(N, X, Mangled, T, Init, Type), .Set) context DeclaratorAndSpecifiers(NormalizedDecl(... nns: HOLE:NNS), _) diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index e390f2eac..d23d3e3f3 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -49,9 +49,9 @@ module CPP-ABSTRACT-SYNTAX | ConstructorMember(CId, Init) [symbol] | ConstructorDelegating(Init) [symbol] - syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, AStmt) [strict(4), symbol] - | FunctionDecl(NNS, CId, CId, AType, List) [strict(4), symbol] - | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [strict(4), symbol] + syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, AStmt) [symbol] + | FunctionDecl(NNS, CId, CId, AType, List) [symbol] + | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [symbol] | FieldDecl(NNS, CId, AType, Init) [strict(3), symbol] | BitFieldDecl(NNS, CId, AType, Expr) [strict(3), symbol] From da1305948c191244dcb8a7897a24239d479505f0 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 10 Apr 2020 16:06:05 +0200 Subject: [PATCH 26/84] fix NoInit --- clang-tools/ClangKast/ClangKast.cc | 1 + clang-tools/ClangKast/ClangKast.h | 1 + clang-tools/ClangKast/GetKastVisitor.h | 12 ++++++++---- 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/clang-tools/ClangKast/ClangKast.cc b/clang-tools/ClangKast/ClangKast.cc index 99ecb3cb7..9d3ec34b1 100644 --- a/clang-tools/ClangKast/ClangKast.cc +++ b/clang-tools/ClangKast/ClangKast.cc @@ -91,6 +91,7 @@ std::ostream& operator<<(std::ostream & os, const Sort & sort) { case Sort::NAMESPACE: os << "Namespeace"; break; case Sort::NNS: os << "NNS"; break; case Sort::NNSSPECIFIER: os << "NNSSpecifier"; break; + case Sort::NOINIT: os << "NoInit"; break; case Sort::NONAME: os << "NoName"; break; case Sort::OPID: os << "OpId"; break; case Sort::QUALIFIER: os << "Qualifier"; break; diff --git a/clang-tools/ClangKast/ClangKast.h b/clang-tools/ClangKast/ClangKast.h index ec07aa03d..91368ec09 100644 --- a/clang-tools/ClangKast/ClangKast.h +++ b/clang-tools/ClangKast/ClangKast.h @@ -39,6 +39,7 @@ enum class Sort { NAMESPACE, NNS, NNSSPECIFIER, + NOINIT, NONAME, OPID, QUALIFIER, diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 0fe46403d..8cbae5405 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -497,6 +497,10 @@ class GetKastVisitor return TraverseFunctionHelper(D); } + void NoInit() { + Kast::add(Kast::KApply("NoInit", Sort::NOINIT)); + } + bool TraverseVarHelper(VarDecl *D) { StorageClass(D->getStorageClass()); ThreadStorageClass(D->getTSCSpec()); @@ -517,7 +521,7 @@ class GetKastVisitor if (D->getInit()) { TRY_TO(TraverseStmt(D->getInit())); } else { - Kast::add(Kast::KApply("NoInit", Sort::INIT)); + NoInit(); } VisitBool(D->isDirectInit()); return true; @@ -544,7 +548,7 @@ class GetKastVisitor } else if (D->hasInClassInitializer()) { TRY_TO(TraverseStmt(D->getInClassInitializer())); } else { - Kast::add(Kast::KApply("NoInit", Sort::INIT)); + NoInit(); } return true; } @@ -1282,7 +1286,7 @@ class GetKastVisitor bool VisitReturnStmt(ReturnStmt *S) { Kast::add(Kast::KApply("ReturnStmt", Sort::STMT, {Sort::INIT})); if (!S->getRetValue()) { - Kast::add(Kast::KApply("NoInit", Sort::INIT)); + NoInit(); } return false; } @@ -1837,7 +1841,7 @@ class GetKastVisitor if (E->hasInitializer()) { TRY_TO(TraverseStmt(E->getInitializer())); } else { - Kast::add(Kast::KApply("NoInit", Sort::INIT)); + NoInit(); } KSeqList(E->getNumPlacementArgs()); for (unsigned i = 0; i < E->getNumPlacementArgs(); i++) { From b1e20bdbc17c9cff80f1b2ca2ce1e6a7ea7f4db8 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 10 Apr 2020 16:06:17 +0200 Subject: [PATCH 27/84] fix sorts --- .build/k | 2 +- semantics/cpp/language/common/dynamic.k | 4 ++-- semantics/cpp/language/common/typing.k | 2 ++ semantics/cpp/language/translation/decl/initializer.k | 4 ++-- 4 files changed, 7 insertions(+), 5 deletions(-) diff --git a/.build/k b/.build/k index 51686b228..bb0ebdce5 160000 --- a/.build/k +++ b/.build/k @@ -1 +1 @@ -Subproject commit 51686b228230341d0fb851767734ed44d88ecfcb +Subproject commit bb0ebdce5a1f94dfc86baaa5f75b97f8c8248b67 diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index aec367f99..09a6e65b5 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -518,7 +518,7 @@ module CPP-DYNAMIC-OTHER-SYNTAX syntax CPPTypes ::= toCPPTypes(List) [function] | toCPPTypes(TemplateArgs) [function, klabel(TemplateArgsToCPPTypes)] - syntax TemplateArg ::= CPPType + syntax TemplateArg ::= CPPDType syntax String ::= showCPPTypes(CPPTypes) [function] | showCPPType(CPPType) [function] @@ -787,7 +787,7 @@ module CPP-DYNAMIC-OTHER rule CPPTypesSize(Ts::CPPTypes) => size(toList(Ts)) - rule toList(T::CPPType, Ts::CPPTypes) => ListItem(T) toList(Ts) + rule toList(T::CPPDType, Ts::CPPTypes) => ListItem(T) toList(Ts) rule toList(.CPPTypes) => .List diff --git a/semantics/cpp/language/common/typing.k b/semantics/cpp/language/common/typing.k index 953f04b51..90f9cf2d5 100644 --- a/semantics/cpp/language/common/typing.k +++ b/semantics/cpp/language/common/typing.k @@ -779,6 +779,8 @@ module CPP-TYPING rule stripTypes(T::CPPType, Ts::TemplateArgs) => stripType(T), stripTypes(Ts) + rule stripTypes(variadic, Ts::TemplateArgs) => variadic, stripTypes(Ts) + rule stripTypes(.TemplateArgs) => .TemplateArgs rule T1::CPPType ==Type T2::CPPType => stripType(T1) ==K stripType(T2) diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k index bedb547a7..7ce4bc607 100644 --- a/semantics/cpp/language/translation/decl/initializer.k +++ b/semantics/cpp/language/translation/decl/initializer.k @@ -86,7 +86,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER requires notBool isSpuriousExpr(HOLE) [result(ValueCategory)] rule #figureInit(Base::Expr, DestT::CPPType, IType::InitType, - I::Init, SrcType::CPPType, SrcCat::ValueCategory, + I::Init, SrcType::K, SrcCat::K, CT::ConstructorType, D::Duration) => Base ~> #figureInitHeatBase(DestT, IType, I, SrcType, SrcCat, CT, D) @@ -95,7 +95,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER requires notBool isLVal(Base) rule Base:LVal ~> #figureInitHeatBase(DestT::CPPType, IType::InitType, - I::Init, SrcType::CPPType, SrcCat::ValueCategory, + I::Init, SrcType::K, SrcCat::K, CT::ConstructorType, D::Duration) => #figureInit(Base, DestT, IType, I, SrcType, SrcCat, CT, D) From f82292b3ccb94aa7e41248061c97bf5decf6eeef Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 15 Apr 2020 11:31:29 +0200 Subject: [PATCH 28/84] strip traces in linking semantics because the execution semantics does not understand the translation semantics's labels --- semantics/linking/init.k | 2 ++ 1 file changed, 2 insertions(+) diff --git a/semantics/linking/init.k b/semantics/linking/init.k index 7b1d85bff..246db3977 100644 --- a/semantics/linking/init.k +++ b/semantics/linking/init.k @@ -350,4 +350,6 @@ module LINKING-INIT syntax Map ::= getOverridden(Map, Map) [function] rule getOverridden(_, _) => .Map::Map [owise] + rule hasTrace(_) => noTrace [anywhere] + endmodule From 2c5ded1cc6f15292129d5b189d0b2e66ff7cb964 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 15 Apr 2020 13:21:32 +0200 Subject: [PATCH 29/84] fix sort --- semantics/cpp/language/execution/expr/function-call.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/execution/expr/function-call.k b/semantics/cpp/language/execution/expr/function-call.k index 264f90daf..1c46a282f 100644 --- a/semantics/cpp/language/execution/expr/function-call.k +++ b/semantics/cpp/language/execution/expr/function-call.k @@ -131,7 +131,7 @@ module CPP-EXECUTION-EXPR-FUNCTION-CALL ~> K:K => sequencePoint ~> enterRestrictBlock(blockScope(X, Base, 0)) - ~> #if Obj ==K .K #then .K #else setThis(& Obj) #fi + ~> #if Obj ==K .K #then .K #else setThis(& {Obj}:>Expr) #fi ~> bind(Params, getParams(DefT), L) ~> Blk @@ -149,7 +149,7 @@ module CPP-EXECUTION-EXPR-FUNCTION-CALL ) ... ( C::Bag - Obj::Expr + Obj:K _ MDC:K From edcc5110a5289ec657637a424828bb4df5e39e40 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 15 Apr 2020 15:22:55 +0200 Subject: [PATCH 30/84] fix `assertInBounds` and `assert` --- semantics/common/error.k | 4 ++-- semantics/cpp/language/common/io.k | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/semantics/common/error.k b/semantics/common/error.k index 715c669df..6b07b8418 100644 --- a/semantics/common/error.k +++ b/semantics/common/error.k @@ -20,7 +20,7 @@ module ERROR-SYNTAX syntax ErrorResult ::= errorFuncResult(K, K) syntax Error - syntax K ::= assert(Bool, Error) + syntax KItem ::= assert(Bool, Error) syntax KItem ::= "EXT" "-" "UNDEF" "(" String "," String ")" [function, klabel(LinkUndef)] syntax KItem ::= "EXT" "-" "UNDEF" "(" String "," String "," List ")" @@ -47,6 +47,6 @@ module ERROR rule errorFuncResult(K1:K, K2:K) => K1 ~> K2 - rule assert(B::Bool, E::Error) => #if B #then .K #else E #fi [macro] + rule assert(B::Bool, E::Error) => #if B #then .K #else E #fi endmodule diff --git a/semantics/cpp/language/common/io.k b/semantics/cpp/language/common/io.k index 37d8199cb..900149957 100644 --- a/semantics/cpp/language/common/io.k +++ b/semantics/cpp/language/common/io.k @@ -4,7 +4,7 @@ module CPP-COMMON-IO-SYNTAX syntax CPPType - syntax K ::= assertInBounds(Int, Int) [klabel(cppAssertInBounds)] + syntax KItem ::= assertInBounds(Int, Int) [klabel(cppAssertInBounds)] syntax Bits ::= getUninitializedBits(SymLoc, CPPType) [function, klabel(getUninitializedBitsCpp)] @@ -25,7 +25,7 @@ module CPP-COMMON-IO syntax Error ::= "errorReadOutOfBounds" rule assertInBounds(Offset::Int, Len::Int) - => assert(Offset assert(Offset DRAFTING("EIO1", "Reading outside the bounds of an object.")) From 12d1c03c5d3618bdb73af7ba2b52a2a8c40ebcf1 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 16 Apr 2020 09:28:12 +0200 Subject: [PATCH 31/84] do not escape strings twice --- clang-tools/ClangKast/ClangKast.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/ClangKast.cc b/clang-tools/ClangKast/ClangKast.cc index 9d3ec34b1..53020f199 100644 --- a/clang-tools/ClangKast/ClangKast.cc +++ b/clang-tools/ClangKast/ClangKast.cc @@ -224,7 +224,7 @@ void Kast::KApply::print(Sort parentSort, function printChild) cons // *** Kast::KToken *** string Kast::KToken::toKString(const string & s) { - return string(Kore ? escape(s) : "\"" + escape(s) + "\""); + return string(Kore ? s : "\"" + escape(s) + "\""); } string Kast::KToken::toKString(bool b) { From 367ef5e81cb4d48d1ed66af984701bfb99395daa Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 16 Apr 2020 09:28:31 +0200 Subject: [PATCH 32/84] fix sorts --- semantics/cpp/language/execution/stmt/return.k | 2 +- semantics/cpp/language/execution/temporary.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/execution/stmt/return.k b/semantics/cpp/language/execution/stmt/return.k index d0b5f1061..931f05f16 100644 --- a/semantics/cpp/language/execution/stmt/return.k +++ b/semantics/cpp/language/execution/stmt/return.k @@ -81,7 +81,7 @@ module CPP-EXECUTION-STMT-RETURN ( .Set .List - LCE::KItem + LCE::K ... => C) ListItem( diff --git a/semantics/cpp/language/execution/temporary.k b/semantics/cpp/language/execution/temporary.k index 7d24a754a..bc4e19bab 100644 --- a/semantics/cpp/language/execution/temporary.k +++ b/semantics/cpp/language/execution/temporary.k @@ -56,7 +56,7 @@ module CPP-EXECUTION-TEMPORARY rule (.K => destructLocal(IsException, Entry)) ~> destructTemporaries(IsException:Bool) ... - ListItem(Entry::KTuple) => .List ... + ListItem(Entry::KItem) => .List ... rule destructTemporaries(...) => .K ... .List From 5e80cb0dc1870a907c7d0344a8a443464ce4a02b Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 11:42:58 +0200 Subject: [PATCH 33/84] IfAStmtD --- clang-tools/ClangKast/GetKastVisitor.h | 6 ++++-- semantics/cpp/language/translation/syntax.k | 8 ++++---- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 8cbae5405..b9372f8cc 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -1347,10 +1347,11 @@ class GetKastVisitor } bool TraverseIfStmt(IfStmt *S) { - Kast::add(Kast::KApply("IfAStmt", Sort::ASTMT, {Sort::DECL, Sort::ASTMT, Sort::ASTMT})); if (VarDecl *D = S->getConditionVariable()) { + Kast::add(Kast::KApply("IfAStmtD", Sort::ASTMT, {Sort::DECL, Sort::ASTMT, Sort::ASTMT})); TRY_TO(TraverseDecl(D)); } else { + Kast::add(Kast::KApply("IfAStmt", Sort::ASTMT, {Sort::EXPR, Sort::ASTMT, Sort::ASTMT})); TRY_TO(TraverseStmt(S->getCond())); } TRY_TO(TraverseStmt(S->getThen())); @@ -1363,10 +1364,11 @@ class GetKastVisitor } bool TraverseSwitchStmt(SwitchStmt *S) { - Kast::add(Kast::KApply("SwitchAStmt", Sort::ASTMT, {Sort::DECL, Sort::ASTMT})); if (VarDecl *D = S->getConditionVariable()) { + Kast::add(Kast::KApply("SwitchAStmtD", Sort::ASTMT, {Sort::DECL, Sort::ASTMT})); TRY_TO(TraverseDecl(D)); } else { + Kast::add(Kast::KApply("SwitchAStmt", Sort::ASTMT, {Sort::EXPR, Sort::ASTMT})); TRY_TO(TraverseStmt(S->getCond())); } TRY_TO(TraverseStmt(S->getBody())); diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index d23d3e3f3..fbf60c44f 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -201,10 +201,10 @@ module CPP-ABSTRACT-SYNTAX | WhileAStmt(Decl, AStmt) | WhileAStmt(Expr, AStmt) [symbol] | DoWhileAStmt(AStmt, Expr) [symbol] - | IfAStmt(Decl, AStmt, AStmt) [symbol] - | IfAStmt(Expr, AStmt, AStmt) - | SwitchAStmt(Decl, AStmt) [symbol] - | SwitchAStmt(Expr, AStmt) + | IfAStmtD(Decl, AStmt, AStmt) [symbol] + | IfAStmt(Expr, AStmt, AStmt) [symbol] + | SwitchAStmtD(Decl, AStmt) [symbol] + | SwitchAStmt(Expr, AStmt) [symbol] | CaseAStmt(Expr, AStmt) [symbol] | DefaultAStmt(AStmt) [symbol] | TryAStmt(AStmt, List) [symbol] From f6cb33bf8ee8aab30c66c1355e6ae6926dd86394 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 11:43:26 +0200 Subject: [PATCH 34/84] operatorXYZ_CPP-SYNTAX_OpId --- clang-tools/ClangKast/GetKastVisitor.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index b9372f8cc..dfc1a7e65 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -1508,7 +1508,7 @@ class GetKastVisitor switch (Kind) { #define OVERLOADED_OPERATOR(Name,Spelling,Token,Unary,Binary,MemberOnly) \ case OO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; #include "clang/Basic/OperatorKinds.def" default: @@ -1520,7 +1520,7 @@ class GetKastVisitor switch (Kind) { #define UNARY_OP(Name, Spelling) \ case UO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; UNARY_OP(PostInc, "_++") UNARY_OP(PostDec, "_--") @@ -1553,7 +1553,7 @@ class GetKastVisitor switch (Kind) { #define BINARY_OP(Name, Spelling) \ case BO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; BINARY_OP(PtrMemD, ".*") BINARY_OP(PtrMemI, "->*") From 679b821963e50bf42d3e8b14be75686605dff26c Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 11:44:07 +0200 Subject: [PATCH 35/84] fix sorts --- semantics/cpp/language/common/conversion.k | 6 ++---- semantics/cpp/language/execution/stmt/if.k | 4 ++-- semantics/cpp/language/execution/stmt/try.k | 4 ++-- semantics/cpp/language/translation/conversion.k | 2 +- semantics/cpp/language/translation/process-label.k | 12 ++++++------ 5 files changed, 13 insertions(+), 15 deletions(-) diff --git a/semantics/cpp/language/common/conversion.k b/semantics/cpp/language/common/conversion.k index ec4aeb862..c36b6f666 100644 --- a/semantics/cpp/language/common/conversion.k +++ b/semantics/cpp/language/common/conversion.k @@ -6,9 +6,7 @@ module CPP-CONVERSION-SYNTAX syntax Expr ::= instantiate(SymLoc, Trace, CPPType) [klabel(instantiateCpp)] // performs standard type conversions only - syntax PRVal ::= convertType(CPPType, PRVal) [function] - - syntax PRExpr ::= convertType(CPPType, PRExpr) [function] + syntax Expr ::= convertType(CPPType, Expr) [function] syntax Expr ::= convertTypeHold(CPPType, Expr) @@ -216,7 +214,7 @@ module CPP-CONVERSION requires X1 ==Type X2 andBool isSimilar(T1, T2) andBool cvQualificationSignature(T1) <=QualSig cvQualificationSignature(T2) - rule convertType(_::CPPType, _::PRExpr) => cannot-convert [owise] + rule convertType(_::CPPType, _:PRExpr) => cannot-convert [owise] rule isSimilar(t(_, _, pointerType(T1::CPPType)), t(_, _, pointerType(T2::CPPType))) => isSimilar(T1, T2) diff --git a/semantics/cpp/language/execution/stmt/if.k b/semantics/cpp/language/execution/stmt/if.k index e9209242e..f3ef84c45 100644 --- a/semantics/cpp/language/execution/stmt/if.k +++ b/semantics/cpp/language/execution/stmt/if.k @@ -9,8 +9,8 @@ module CPP-EXECUTION-STMT-IF rule IfStmt(prv((unknown(I::Int) => #if I ==Int 0 #then 0 #else 1 #fi), _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), _, _) - rule IfStmt(prv(1, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), S::Stmt, _) => fullExpression ~> S + rule IfStmt(prv(1, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), S::K, _) => fullExpression ~> S - rule IfStmt(prv(0, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), _, S::Stmt) => fullExpression ~> S + rule IfStmt(prv(0, _, t(... st: _:CPPSimpleBoolType) #as T::CPPType), _, S::K) => fullExpression ~> S endmodule diff --git a/semantics/cpp/language/execution/stmt/try.k b/semantics/cpp/language/execution/stmt/try.k index d200bc6c4..66e9acdc3 100644 --- a/semantics/cpp/language/execution/stmt/try.k +++ b/semantics/cpp/language/execution/stmt/try.k @@ -145,10 +145,10 @@ module CPP-EXECUTION-STMT-TRY requires size(S) >Int 0 rule throw(V::LVal) => catchWithHandler(CatchAnyOp(S), V) ... - ListItem(CatchAnyOp(S::Stmt)) ... + ListItem(CatchAnyOp(S::K)) ... rule throw(V::LVal) => catchWithHandler(CatchOp(T, S), V) ... - ListItem(CatchOp(T::CPPType, S::Stmt)) ... + ListItem(CatchOp(T::CPPType, S::K)) ... requires handlerMatches(T, type(V)) rule throw(V::LVal) ... diff --git a/semantics/cpp/language/translation/conversion.k b/semantics/cpp/language/translation/conversion.k index 4e6ad6e7f..1507a6170 100644 --- a/semantics/cpp/language/translation/conversion.k +++ b/semantics/cpp/language/translation/conversion.k @@ -12,7 +12,7 @@ module CPP-TRANSLATION-CONVERSION rule convertType(t(... st: memberPointerType(...)) #as T::CPPType, prv(0, hasTrace(IntegerLiteral(0, T2::CPPType)), _)) => prv(NullMemberPointer, hasTrace(IntegerLiteral(0, T2)), T) - rule convertType(T::CPPType, pre(E::Expr, Tr::Trace, _)) => pre(ConvertType(T, E), Tr, T) + rule convertType(T::CPPType, pre(E:Expr, Tr::Trace, _)) => pre(ConvertType(T, E), Tr, T) rule isNullPointerConstant(prv(_, hasTrace(IntegerLiteral(0, _)), _)) => true diff --git a/semantics/cpp/language/translation/process-label.k b/semantics/cpp/language/translation/process-label.k index 5d46ce5cd..747932b26 100644 --- a/semantics/cpp/language/translation/process-label.k +++ b/semantics/cpp/language/translation/process-label.k @@ -106,7 +106,7 @@ module CPP-TRANSLATION-PROCESS-LABEL rule waitingOnGotoMap ... - (ForStmt(Control:Expr, Post::Stmt, S::Stmt) => .K) + (ForStmt(Control:Expr, Post::Stmt, S::K) => .K) ~> K:K Tail:K @@ -141,7 +141,7 @@ module CPP-TRANSLATION-PROCESS-LABEL rule waitingOnGotoMap ... (.K => S ~> loopMarked) - ~> WhileStmt(_:Expr, S::Stmt) + ~> WhileStmt(_:Expr, S::K) ~> (.K => popLoop) ~> K:K @@ -159,7 +159,7 @@ module CPP-TRANSLATION-PROCESS-LABEL rule waitingOnGotoMap ... - (IfStmt(_:Expr, S1::Block, S2::Block) => .K) ~> K:K + (IfStmt(_:Expr, S1::K, S2::K) => .K) ~> K:K Tail:K B::Bag @@ -182,7 +182,7 @@ module CPP-TRANSLATION-PROCESS-LABEL rule waitingOnGotoMap ... - (TryStmt(S::Block, .List) => .K) ~> K:K + (TryStmt(S::K, .List) => .K) ~> K:K Tail:K B::Bag @@ -196,7 +196,7 @@ module CPP-TRANSLATION-PROCESS-LABEL rule waitingOnGotoMap ... - TryStmt(_, (ListItem(CatchOp(T::CPPType, S::Block)) => .List) L::List) ~> K:K + TryStmt(_, (ListItem(CatchOp(T::CPPType, S::K)) => .List) L::List) ~> K:K Tail:K B::Bag @@ -210,7 +210,7 @@ module CPP-TRANSLATION-PROCESS-LABEL rule waitingOnGotoMap ... - TryStmt(_, (ListItem(CatchAnyOp(S::Block)) => .List) L::List) ~> K:K + TryStmt(_, (ListItem(CatchAnyOp(S::K)) => .List) L::List) ~> K:K Tail:K B::Bag From 280c0f5e1936f5ac7d500ecc2bdc5581e194ddb3 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 14:42:57 +0200 Subject: [PATCH 36/84] fix sorts --- semantics/cpp/language/translation/stmt/canonicalization.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/semantics/cpp/language/translation/stmt/canonicalization.k b/semantics/cpp/language/translation/stmt/canonicalization.k index 731901267..6aa7f4bcb 100644 --- a/semantics/cpp/language/translation/stmt/canonicalization.k +++ b/semantics/cpp/language/translation/stmt/canonicalization.k @@ -44,7 +44,7 @@ module CPP-TRANSLATION-STMT-CANONICALIZATION rule canonicalizeAStmts(ListItem(E:Expr) L::List) => ListItem(TExpressionStmt(E)) canonicalizeAStmts(L) - rule canonicalizeAStmts(ListItem(S::Stmt) L::List) => ListItem(S) canonicalizeAStmts(L) [owise] + rule canonicalizeAStmts(ListItem(S:AStmt) L::List) => ListItem(S) canonicalizeAStmts(L) [owise] rule canonicalizeAStmts(.List) => .List From 42ae7cafe799be5ddde9711e187712cc7597c01d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 14:43:58 +0200 Subject: [PATCH 37/84] isKResult --- semantics/cpp/language/translation/decl/declarator.k | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/semantics/cpp/language/translation/decl/declarator.k b/semantics/cpp/language/translation/decl/declarator.k index 5d3600bd3..de7d7af07 100644 --- a/semantics/cpp/language/translation/decl/declarator.k +++ b/semantics/cpp/language/translation/decl/declarator.k @@ -403,8 +403,9 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule stripAuto => .K ... ... auto |-> _ => .Map ... - rule declareNonStaticObject(ID::CId, T::CPPType, Init:KResult, DT::DeclarationType, DU::Duration, S::Set) + rule declareNonStaticObject(ID::CId, T::CPPType, Init:KItem, DT::DeclarationType, DU::Duration, S::Set) => declareNonStaticObject2(declareNonStaticObjectExec(ID, T, Init, DT, DU, S), Constexpr() in S) + requires isKResult(Init) syntax KItem ::= declareNonStaticObject2(K, Bool) From f2f2798dc16b547addefd6bf2124babc7d9b1d63 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 16:11:52 +0200 Subject: [PATCH 38/84] fix sorts --- semantics/cpp/language/common/dynamic.k | 4 ++-- semantics/cpp/language/execution/stmt/loop.k | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index 09a6e65b5..36f3dfd49 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -565,7 +565,7 @@ module CPP-DYNAMIC-OTHER-SYNTAX syntax KItem ::= odrDecl(String, QualId, CId, LanguageLinkage, CPPType) - syntax Stmt ::= compoundStmt(Stmt, Stmt) + syntax Stmt ::= compoundStmt(K, Stmt) syntax Stmt ::= nullStmt() syntax SSList ::= toSSList(List) [klabel(toSSListcpp), function] @@ -1071,7 +1071,7 @@ module CPP-DYNAMIC-OTHER rule Translation() => notBool Execution() - rule compoundStmt(S1::Stmt, S2::Stmt) => S1 ~> S2 + rule compoundStmt(S1::K, S2::Stmt) => S1 ~> S2 rule nullStmt() => .K rule idOf(Class(_, X::CId, _)) => X diff --git a/semantics/cpp/language/execution/stmt/loop.k b/semantics/cpp/language/execution/stmt/loop.k index 60a0bea4a..744ee4518 100644 --- a/semantics/cpp/language/execution/stmt/loop.k +++ b/semantics/cpp/language/execution/stmt/loop.k @@ -4,7 +4,7 @@ module CPP-EXECUTION-STMT-LOOP imports CPP-DYNAMIC-SYNTAX imports CPP-SYNTAX - rule ForStmt(Control::Expr, Post::Stmt, S::Stmt) ~> K:K + rule ForStmt(Control::Expr, Post::Stmt, S::K) ~> K:K => loopMarked ~> ForStmt(Control, Post, S) ~> popLoop @@ -12,7 +12,7 @@ module CPP-EXECUTION-STMT-LOOP ListItem(Num::Int) ... .List => ListItem(kpair(Num, K)) ... - rule loopMarked ~> ForStmt(Control:Expr, Post::Stmt, S::Stmt) + rule loopMarked ~> ForStmt(Control:Expr, Post::Stmt, S::K) => IfStmt(Control, compoundStmt(S, compoundStmt(Post, compoundStmt(loopMarked, ForStmt(Control, Post, S)))), nullStmt()) @@ -24,7 +24,7 @@ module CPP-EXECUTION-STMT-LOOP ListItem(Num::Int) ... .List => ListItem(kpair(Num, K)) ... - rule loopMarked ~> WhileStmt(Control:Expr, S::Stmt) + rule loopMarked ~> WhileStmt(Control:Expr, S::K) => IfStmt(Control, compoundStmt(S, compoundStmt(loopMarked, WhileStmt(Control, S))), nullStmt()) From dd76982913bfe0af5ba60443bb2903a4f2752834 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 16:18:12 +0200 Subject: [PATCH 39/84] fix sorts --- .../cpp/language/execution/expr/assignment.k | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/semantics/cpp/language/execution/expr/assignment.k b/semantics/cpp/language/execution/expr/assignment.k index 33d15d031..b6185757b 100644 --- a/semantics/cpp/language/execution/expr/assignment.k +++ b/semantics/cpp/language/execution/expr/assignment.k @@ -55,21 +55,21 @@ module CPP-EXECUTION-EXPR-ASSIGNMENT rule compoundOp(compoundExprs(_, R::Expr) #as E:ResolvedExpr) => E requires isKResult(R) andBool Execution() - rule fillRHoles(V::PRVal, pre(L::Expr := E::Expr, Tr::Trace, T::CPPType)) => pre(L := fillRHoles(V, E), Tr, T) - rule fillRHoles(V::PRVal, V':PRV) => V' - rule fillRHoles(V::PRVal, ConvertType(T::CPPType, E::Expr)) => ConvertType(T, fillRHoles(V, E)) - rule fillRHoles(V::PRVal, compoundOp(E::Expr)) => compoundOp(fillRHoles(V, E)) - rule fillRHoles(V::PRVal, RHOLE) => V - rule fillRHoles(V::PRVal, L::Expr + R::Expr) => fillRHoles(V, L) + R - rule fillRHoles(V::PRVal, L::Expr - R::Expr) => fillRHoles(V, L) - R - rule fillRHoles(V::PRVal, L::Expr * R::Expr) => fillRHoles(V, L) * R - rule fillRHoles(V::PRVal, L::Expr / R::Expr) => fillRHoles(V, L) / R - rule fillRHoles(V::PRVal, L::Expr % R::Expr) => fillRHoles(V, L) % R - rule fillRHoles(V::PRVal, L::Expr & R::Expr) => fillRHoles(V, L) & R - rule fillRHoles(V::PRVal, L::Expr ^ R::Expr) => fillRHoles(V, L) ^ R - rule fillRHoles(V::PRVal, L::Expr | R::Expr) => fillRHoles(V, L) | R - rule fillRHoles(V::PRVal, L::Expr << R::Expr) => fillRHoles(V, L) << R - rule fillRHoles(V::PRVal, L::Expr >> R::Expr) => fillRHoles(V, L) >> R + rule fillRHoles(V::Expr, pre(L::Expr := E::Expr, Tr::Trace, T::CPPType)) => pre(L := fillRHoles(V, E), Tr, T) + rule fillRHoles(V::Expr, V':PRV) => V' + rule fillRHoles(V::Expr, ConvertType(T::CPPType, E::Expr)) => ConvertType(T, fillRHoles(V, E)) + rule fillRHoles(V::Expr, compoundOp(E::Expr)) => compoundOp(fillRHoles(V, E)) + rule fillRHoles(V::Expr, RHOLE) => V + rule fillRHoles(V::Expr, L::Expr + R::Expr) => fillRHoles(V, L) + R + rule fillRHoles(V::Expr, L::Expr - R::Expr) => fillRHoles(V, L) - R + rule fillRHoles(V::Expr, L::Expr * R::Expr) => fillRHoles(V, L) * R + rule fillRHoles(V::Expr, L::Expr / R::Expr) => fillRHoles(V, L) / R + rule fillRHoles(V::Expr, L::Expr % R::Expr) => fillRHoles(V, L) % R + rule fillRHoles(V::Expr, L::Expr & R::Expr) => fillRHoles(V, L) & R + rule fillRHoles(V::Expr, L::Expr ^ R::Expr) => fillRHoles(V, L) ^ R + rule fillRHoles(V::Expr, L::Expr | R::Expr) => fillRHoles(V, L) | R + rule fillRHoles(V::Expr, L::Expr << R::Expr) => fillRHoles(V, L) << R + rule fillRHoles(V::Expr, L::Expr >> R::Expr) => fillRHoles(V, L) >> R rule fillLHoles(LV::Expr, pre(LHOLE := R::Expr, Tr::Trace, T::CPPType)) => pre(LV := R, Tr, T) From eb36782ddbd17aa552a5cdd03a757fde207efb6d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 16:39:05 +0200 Subject: [PATCH 40/84] Fix sorts --- semantics/cpp/language/execution/stmt/block.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/semantics/cpp/language/execution/stmt/block.k b/semantics/cpp/language/execution/stmt/block.k index a2c521706..7dc14f03a 100644 --- a/semantics/cpp/language/execution/stmt/block.k +++ b/semantics/cpp/language/execution/stmt/block.k @@ -99,7 +99,7 @@ module CPP-EXECUTION-STMT-BLOCK rule (.K => destructLocal(IsException, Entry)) ~> destructLocals(IsException:Bool) ... - ListItem(Entry::KTuple) => .List ... + ListItem(Entry::KItem) => .List ... rule destructLocals(...) => .K ... .List From 095d64533921e82649c47ce0fd881620ac40a163 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 16:51:46 +0200 Subject: [PATCH 41/84] Parser: 'And-' --- clang-tools/ClangKast/ClangKast.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/ClangKast.cc b/clang-tools/ClangKast/ClangKast.cc index 53020f199..7fdb4aac3 100644 --- a/clang-tools/ClangKast/ClangKast.cc +++ b/clang-tools/ClangKast/ClangKast.cc @@ -141,7 +141,7 @@ string Kast::Node::escapeKLabel(const string & label) { case '#': subst = "Hash'"; break; case '$': subst = "Dolr'"; break; case '%': subst = "Perc'"; break; - case '&': subst = "And'" ; break; + case '&': subst = "And-'"; break; case '\'': subst = "Apos'"; break; case '(': subst = "LPar'"; break; case ')': subst = "RPar'"; break; From fbdad09f3dd1baef9545d50d912646e4141112ec Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 16:58:31 +0200 Subject: [PATCH 42/84] We no longer have sort BraceInit --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index dfc1a7e65..24abf1c49 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -2027,7 +2027,7 @@ class GetKastVisitor bool TraverseInitListExpr(InitListExpr *E) { InitListExpr *Syntactic = E->isSemanticForm() ? E->getSyntacticForm() ? E->getSyntacticForm() : E : E; - Kast::add(Kast::KApply("BraceInit", Sort::BRACEINIT, {Sort::LIST})); + Kast::add(Kast::KApply("BraceInit", Sort::INIT, {Sort::LIST})); KSeqList(Syntactic->getNumInits()); for (Stmt *SubStmt : Syntactic->children()) { TRY_TO(TraverseStmt(SubStmt)); From 1867f49177282b470222579b77b12d2736f2661d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 17 Apr 2020 17:30:01 +0200 Subject: [PATCH 43/84] fix sorts --- semantics/cpp/language/translation/decl/declarator.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/translation/decl/declarator.k b/semantics/cpp/language/translation/decl/declarator.k index de7d7af07..0d76a442d 100644 --- a/semantics/cpp/language/translation/decl/declarator.k +++ b/semantics/cpp/language/translation/decl/declarator.k @@ -115,7 +115,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR syntax Duration ::= getDuration(Set, Scope) [function] - syntax Namespace ::= getInnermostNamespace(NNSVal, Scope) [function] + syntax NNSVal ::= getInnermostNamespace(NNSVal, Scope) [function] rule getPreviousLinkage(X::QualId, T::CPPType, X |-> (stripType(T) |-> _ _::Map) _::Map, _) => ExternalLinkage @@ -186,7 +186,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR rule getInnermostNamespace(NoNamespace(), blockScope((localQual(Scope::BlockScope) :: _:ClassSpecifier) :: _, _, _) => Scope) - rule getInnermostNamespace(N::Namespace, _) => N + rule getInnermostNamespace(N::NNSVal, _) => N requires N =/=K NoNamespace() /* After everything is computed */ From 8219c337881dd474bb5c8ed08a34de4ef0d9619d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 20 Apr 2020 16:18:32 +0200 Subject: [PATCH 44/84] fix csetunion --- semantics/cpp/language/translation/overloading.k | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/semantics/cpp/language/translation/overloading.k b/semantics/cpp/language/translation/overloading.k index b2237374f..6be5889c4 100644 --- a/semantics/cpp/language/translation/overloading.k +++ b/semantics/cpp/language/translation/overloading.k @@ -117,7 +117,8 @@ module CPP-TRANSLATION-OVERLOADING // strict version rule cSetUnion(notFound(_), E::Expr) => E - rule cSetUnion(E::Expr, notFound(_)) => E + rule cSetUnion(E:KResult, notFound(_)) => E + requires notFound(_) :/=K E andBool cSet(_,_) :/=K E rule cSetUnion(cSet(M1::Map, QX::QualId), cSet(M2::Map, QX)) => cSet(M1 M2, QX) From b2cd6d88a31c60487cdc379b51425173d71e8bfa Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 28 Jun 2019 00:12:31 +0000 Subject: [PATCH 45/84] LLVM backend: kcc/runner scripts. --- Makefile | 2 +- scripts/kcc | 98 +++++++++++++++---------------- scripts/program-runner | 77 +++++++----------------- semantics/Makefile | 4 +- semantics/linking/configuration.k | 2 +- 5 files changed, 72 insertions(+), 111 deletions(-) diff --git a/Makefile b/Makefile index 9b28f6b69..38a808f41 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ export KOMPILE := $(K_BIN)/kompile export KDEP := $(K_BIN)/kdep # Appending to whatever the environment provided. -K_OPTS += -Xmx8g +K_OPTS += -Xmx16g K_OPTS += -Xss32m export K_OPTS diff --git a/scripts/kcc b/scripts/kcc index cf0e0b17b..4236a0256 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -37,6 +37,8 @@ use constant KRUN => do { my $ext = IS_CYGWIN? '.bat' : ''; $path . $ext; }; + +use constant LLVM_KRUN => kBinDir('llvm-krun'); use constant PRINTF => IS_CYGWIN? 'printf %%s' : 'printf %s'; use constant QUOTE_INT => IS_CYGWIN? printable("\"Int\"") : "\"Int\""; use constant QUOTE_STRING => IS_CYGWIN? printable("\"String\"") : "\"String\""; @@ -127,7 +129,7 @@ sub main { close(FILE); my $profDir = profileDir(); - my $krun = KRUN; + my $krun = LLVM_KRUN; $template =~ s?__EXTERN_SCRIPTS_DIR__?$profDir?g; $template =~ s?__EXTERN_HEAP_SIZE__?$heapSize?g; $template =~ s?__EXTERN_KRUN__?$krun?g; @@ -292,15 +294,15 @@ sub makeOptions { my @options = (); if (arg('-fno-native-compilation')) { - push(@options, "`NoNativeFallback`(.KList)"); + push(@options, "LblNoNativeFallback{}()"); } if (arg('-frecover-all-errors')) { - push(@options, "`RecoverAll`(.KList)"); + push(@options, "LblRecoverAll{}()"); } if (arg('-fuse-native-std-lib')) { - push(@options, "`UseNativeStdLib`(.KList)"); + push(@options, "LblUseNativeStdLib{})"); } if (arg('-flint') || arg('-Wlint')) { @@ -334,23 +336,23 @@ sub makeOptions { $stackSize = printable($stackSize); } my $int = QUOTE_INT; - push(@options, "`Lint`(.KList)"); - push(@options, "`Heap`(#token($heapSize, $int))"); - push(@options, "`Stack`(#token($stackSize, $int))"); + push(@options, "LblLint{}()"); + push(@options, "LblHeap{}(\\dv{SortInt{}}($heapSize))"); + push(@options, "LblStack{}(\\dv{SortInt{}}($stackSize))"); } if (arg('-e')) { my $entry = quote(printable(quote(arg('-e')))); my $string = QUOTE_STRING; - push(@options, "`EntryPoint`(#token($entry, $string))"); + push(@options, "LblEntryPoint{}(\\dv{SortString{}}($entry))"); } if (arg('-finteractive-fail')) { - push(@options, "`InteractiveFail`(.KList)"); + push(@options, "LblInteractiveFail{}()"); } if (arg('-Wfatal-errors')) { - push(@options, "`FatalErrors`(.KList)"); + push(@options, "LblFatalErrors{}()"); } if (arg('-funresolved-symbols=')) { @@ -373,22 +375,22 @@ sub makeOptions { $file = quote(printable(quote(rel2abs($file)))); $line = quote(printable($line)); my ($string, $int) = (QUOTE_STRING, QUOTE_INT); - push(@options, "`Breakpoint`(#token($file, $string), #token($line, $int))"); + push(@options, "LblBreakpoint{}(\\dv{SortString{}}($file), \\dv{SortInt{}}($line))"); } if ($link) { - push(@options, "`Link`(.KList)"); + push(@options, "LblLink{}()"); } - return makeSet(@options); + return makeOptionSet(@options); } sub addArg { - my ($name, $value, $category, @krunArgs) = @_; + my ($name, $value, $sort, $category, @krunArgs) = @_; if (useInterpreter()) { - push(@krunArgs, '-c', $name, $value, $category); + push(@krunArgs, '-c', $name, $value, $sort, $category); } else { push(@krunArgs, "-c$name=$value"); if ($category eq 'text' or $category eq 'binary') { @@ -429,7 +431,7 @@ sub linkAll { } sub getKRunCommand { - my ($output, $symbols, $sem) = @_; + my ($output, $sem) = @_; my $def = profileDir($sem); @@ -437,9 +439,9 @@ sub getKRunCommand { if (useInterpreter()) { my $dir = catfile($def, $sem); @krun = - ( catfile($dir, 'interpreter') - , catfile($dir, 'realdef.cma') - , $symbols + ( LLVM_KRUN + , '-d' + , $dir , '--output-file', $output ); } else { @@ -450,7 +452,6 @@ sub getKRunCommand { , '-d', $def , '-w', 'none' , '--smt', 'none' - , '--argv', $symbols ); if (arg('-d')) { @@ -466,7 +467,7 @@ sub getLinkingCommand { my @objs = objFiles(); - my @krun = getKRunCommand($output, $symbols, 'c-cpp-linking-kompiled'); + my @krun = getKRunCommand($output, 'c-cpp-linking-kompiled'); if (arg('-flinking-depth=')) { push(@krun, '--depth'); @@ -474,15 +475,15 @@ sub getLinkingCommand { } my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING); - my $json = "#token($rvErrorJson, $string)"; + my $json = "\\dv{SortString{}}($rvErrorJson)"; - @krun = addArg("OPTIONS", makeOptions($link), 'text', @krun); - @krun = addArg("JSON", $json, 'text', @krun); + @krun = addArg("OPTIONS", makeOptions($link), 'Set', 'kore', @krun); + @krun = addArg("JSON", $json, 'String', 'kore', @krun); my $uuid = create_uuid_as_string(); my $encodedUuid = quote(printable(quote($uuid))); - my $uuidOpt = "#token($encodedUuid, $string)"; - @krun = addArg("UUID", $uuidOpt, 'text', @krun); + my $uuidOpt = "\\dv{SortString{}}($encodedUuid)"; + @krun = addArg("UUID", $uuidOpt, 'String', 'kore', @krun); if (scalar @objs) { my $allObjsFile = tempFile('all-objs'); @@ -498,29 +499,24 @@ sub getLinkingCommand { }; } if (length $thisObj) { - # push(@objTexts, "`unwrapObj`($thisObj)"); - $thisObj = substr($thisObj, 8, -1); # wrap $thisObj with `unwrapObj`() - push(@objTexts, "$thisObj\x02\x00\x00\x00\x00\x00\x00\x00\x09\x00u\x00n\x00w\x00r\x00a\x00p\x00O\x00b\x00j\x00\x00\x00\x00\x01"); + push(@objTexts, "LblunwrapObj{}($thisObj)"); } } - my $objText = join('', @objTexts); - my $one = chr((scalar @objTexts >> 24) & 0xff); - my $two = chr((scalar @objTexts >> 16) & 0xff); - my $three = chr((scalar @objTexts >> 8) & 0xff); - my $four = chr((scalar @objTexts >> 0) & 0xff); - $objText = MAGIC . "\x04\x00\x01$objText\x03$one$two$three$four\x07"; + my $objText = 'dotk{}()'; + foreach my $obj (@objTexts) { + $objText = 'kseq{}(' . $obj . ', ' . $objText . ')'; + } + $objText = "Lblload{}($objText)"; open(my $file, '>', "$allObjsFile"); print $file $objText; close $file; - @krun = addArg("OBJS", $allObjsFile, 'binaryfile', @krun); + @krun = addArg("OBJS", $allObjsFile, 'KItem', 'korefile', @krun); } else { - @krun = addArg("OBJS", ".K", 'text', @krun); + @krun = addArg("OBJS", "Lblload{}(dotk{}())", 'KItem', 'text', @krun); } - @krun = addArg("PGM", ".K", 'text', @krun); - setShellDebugFile($output, 1); return @krun; } @@ -531,7 +527,7 @@ sub getTranslationCommand { my $cTransDef = profileDir("c-translation-kompiled"); my $cppTransDef = profileDir("cpp-translation-kompiled"); - my @krun = getKRunCommand($output, 'dummy', + my @krun = getKRunCommand($output, $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled'); if (arg('-ftranslation-depth=')) { @@ -540,17 +536,17 @@ sub getTranslationCommand { } my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING); - my $json = "#token($rvErrorJson, $string)"; + my $json = "\\dv{SortString{}}($rvErrorJson)"; - @krun = addArg("OPTIONS", makeOptions(0), 'text', @krun); - @krun = addArg("JSON", $json, 'text', @krun); + @krun = addArg("OPTIONS", makeOptions(0), 'Set', 'kore', @krun); + @krun = addArg("JSON", $json, 'String', 'kore', @krun); my $encodedUuid = quote(printable(quote($uuid))); - my $uuidOpt = "#token($encodedUuid, $string)"; - @krun = addArg("UUID", $uuidOpt, 'text', @krun); + my $uuidOpt = "\\dv{SortString{}}($encodedUuid)"; + @krun = addArg("UUID", $uuidOpt, 'String', 'kore', @krun); my $kast = parse($src, $lang, $trampolines); - @krun = addArg("PGM", $kast, 'textfile', @krun); + @krun = addArg("PGM", $kast, 'KItem', 'korefile', @krun); setShellDebugFile($output, 1); return @krun; @@ -627,7 +623,7 @@ sub parse { return $kast; } my $cparser = distDir('cparser'); - shell($cparser, $ppResult, '--trueName', $inputFile)->verbose()->stdout($kast)->run(); + shell($cparser, $ppResult, '--kore', '--trueName', $inputFile)->verbose()->stdout($kast)->run(); return $kast; } @@ -656,16 +652,16 @@ sub getStd { return "-std=$std"; } -sub makeSet { - my $set = '`.Set`(.KList)'; +sub makeOptionSet { + my $set = "Lbl'Stop'Set{}()"; foreach my $el (@_) { - $set = "`_Set_`(`SetItem`($el), $set)"; + $set = "Lbl'Unds'Set'Unds'{}(LblSetItem{}(inj{SortOpt{}, SortKItem{}}($el)), $set)"; } return $set; } sub useInterpreter { - -e profileDir('cpp-translation-kompiled', 'cpp-translation-kompiled', 'interpreter'); + return 1; } sub getRVErrorJson { diff --git a/scripts/program-runner b/scripts/program-runner index f9dff59b3..63cf81856 100755 --- a/scripts/program-runner +++ b/scripts/program-runner @@ -8,6 +8,7 @@ use File::Temp; use File::Copy; use MIME::Base64; use String::Escape qw(quote backslash); +use String::ShellQuote qw(shell_quote_best_effort); setpgrp; @@ -31,9 +32,9 @@ my $SCRIPTS_DIR = '__EXTERN_SCRIPTS_DIR__'; my $KRUN = '__EXTERN_KRUN__'; -my $EXEC_DEF = catfile($SCRIPTS_DIR, "c-cpp-kompiled"); -my $EXEC_ND_DEF = catfile($SCRIPTS_DIR, "c-nd-kompiled"); -my $EXEC_ND_THREAD_DEF = catfile($SCRIPTS_DIR, "c-nd-thread-kompiled"); +my $EXEC_DEF = catfile(catfile($SCRIPTS_DIR, "c-cpp-kompiled"), "c-cpp-kompiled"); +my $EXEC_ND_DEF = catfile(catfile($SCRIPTS_DIR, "c-nd-kompiled"), "c-nd-kompiled"); +my $EXEC_ND_THREAD_DEF = catfile(catfile($SCRIPTS_DIR, "c-nd-thread-kompiled"), "c-nd-thread-kompiled"); my @temporaryFiles = (); @@ -64,10 +65,9 @@ sub main { $objInput = ''; } - my $argv = reduce { our ($a, $b); "`_List_`($a,$b)" } (map {qq|`ListItem`(#token($_, "String"))|} (map {quote(backslash(quote(backslash($_))))} ($0, @ARGV))); + my $argv = reduce { our ($a, $b); "Lbl'Unds'List'Unds'{}($a,$b)" } (map {qq|LblListItem{}(inj{SortString{}, SortKItem{}}(\\dv{SortString{}}($_)))|} (map {quote(backslash($_))} ($0, @ARGV))); - my @cmd = ('--output', 'kast', '--no-sort-collections', '--no-alpha-renaming', '-d', $EXEC_DEF, "-cARGV=$argv", '-pARGV=printf %s', '-w', 'none', '--parser', - 'cat', $fileInput); + my @cmd = ('-d', $EXEC_DEF, "-c", "ARGV", $argv, "List", "kore", "-c", "PGM", $fileInput, "GeneratedTopCell", "korefile"); my $options = getOptions(); if (defined $ENV{HELP}) { @@ -84,73 +84,40 @@ sub main { return 1; } - if (defined $ENV{TRACE}) { - push @cmd, '--trace'; - } - if (defined $ENV{DEBUG}) { push @cmd, '--debug'; } - if (defined $ENV{VERBOSE}) { - push @cmd, '--verbose'; - } - - push @cmd, '--native-libraries'; - my $libs = nativeLibraries(); + #push @cmd, '--native-libraries'; + #my $libs = nativeLibraries(); # kcc may have been run as k++ so this is necessary - push @cmd, "-lstdc++ $libs $objInput"; + #push @cmd, "-lstdc++ $libs $objInput"; if (defined $ENV{DEPTH}) { push @cmd, '--depth'; push @cmd, $ENV{DEPTH}; } - if (defined $ENV{PROVE}) { - push @cmd, '--prove'; - push @cmd, $ENV{PROVE}; - push @cmd, '--smt_prelude'; - push @cmd, $ENV{SMT_PRELUDE}; - } else { - push @cmd, '--smt'; - push @cmd, 'none'; - push @cmd, '--output-file'; - push @cmd, $fileOutput; - } - - if (defined $ENV{SEARCH}) { - push @cmd, '--search-final'; - $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)"; - push @cmd, '-d'; - push @cmd, $EXEC_ND_DEF; - print 'Searching reachable states... '; - print "(with non-deterministic expression sequencing)\n"; - } - - if (defined $ENV{THREADSEARCH}) { - push @cmd, '--search-final'; - $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)"; - push @cmd, '-d'; - push @cmd, $EXEC_ND_THREAD_DEF; - print 'Searching reachable states... '; - print "(with non-deterministic thread interleaving)\n"; - } + push @cmd, '--output-file'; + push @cmd, $fileOutput; my $encodedJson = getJson(); - push @cmd, "-cOPTIONS=$options"; - push @cmd, '-pOPTIONS=printf %s'; - push @cmd, '-cJSON=#token(' . $encodedJson . ', "String")'; - push @cmd, '-pJSON=printf %s'; + push @cmd, "-c"; + push @cmd, "OPTIONS"; + push @cmd, $options; + push @cmd, "Set"; + push @cmd, "kore"; + push @cmd, "-c"; + push @cmd, "JSON"; + push @cmd, "\\dv{SortString{}}($encodedJson)"; + push @cmd, "String"; + push @cmd, "kore"; # Execute krun with the arguments in @cmd - print("'krun' '" . join("' '", @cmd) . "'\n") if defined $ENV{VERBOSE}; + print(join(' ', ($KRUN, map {shell_quote_best_effort($_)} @cmd)) . "\n") if defined $ENV{VERBOSE}; my $ret = system($KRUN, @cmd) >> 8; - if (defined $ENV{LTLMC} | defined $ENV{PROVE}) { - return 0; - } - return processResult($fileOutput, $ret, defined $ENV{VERBOSE}); } diff --git a/semantics/Makefile b/semantics/Makefile index e79ca7e21..1143222d4 100644 --- a/semantics/Makefile +++ b/semantics/Makefile @@ -8,9 +8,7 @@ OUTPUT_DIR := $(abspath $(BUILD_DIR)) PROFILE_DIR := $(realpath $(CURDIR)/../profiles/x86-gcc-limited-libc) # Appending to whatever the environment provided. -KOMPILE_FLAGS += --backend ocaml -KOMPILE_FLAGS += --non-strict -KOMPILE_FLAGS += --smt none +KOMPILE_FLAGS += --backend llvm # Generate a makefile list from a colon-separated one. # K_INCLUDE_PATH comes from the environment. diff --git a/semantics/linking/configuration.k b/semantics/linking/configuration.k index 339871e99..c8df194ea 100644 --- a/semantics/linking/configuration.k +++ b/semantics/linking/configuration.k @@ -17,7 +17,7 @@ module C-CONFIGURATION - load($OBJS:K) + $OBJS:KItem ~> linkProgram(getEntryPoint($OPTIONS:Set)) ~> cleanup From 5b76644f1fbb02c631c21167b12d0a26bd640ce7 Mon Sep 17 00:00:00 2001 From: chathhorn Date: Wed, 28 Aug 2019 17:38:49 -0500 Subject: [PATCH 46/84] Dockerfile: build LLVM backend. --- Dockerfile | 42 ++++++++++++++++++++++++++++-------------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/Dockerfile b/Dockerfile index 7d9cb9584..f60fe2d0e 100644 --- a/Dockerfile +++ b/Dockerfile @@ -4,12 +4,25 @@ FROM runtimeverificationinc/kframework:ubuntu-bionic # Install packages. # ##################### -RUN apt-get update -q \ - && apt install --yes \ - libstdc++6 \ - llvm-6.0 \ - clang++-6.0 \ - clang-6.0 +RUN apt-get update -q \ + && apt-get install --yes \ + libstdc++6 \ + llvm-6.0 \ + clang++-6.0 \ + clang-6.0 \ + clang-8 \ + libclang-8-dev \ + llvm-8-tools \ + lld-8 \ + zlib1g-dev \ + bison \ + flex \ + libboost-test-dev \ + libgmp-dev \ + libmpfr-dev \ + libyaml-dev \ + libjemalloc-dev \ + pkg-config RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.7 \ && cd z3 \ @@ -41,20 +54,21 @@ COPY --from=runtimeverificationinc/ocaml:ubuntu-bionic \ /home/user/.opam \ /home/user/.opam - -# This is where the rest of the dependencies go. -ENV DEPS_DIR="/home/user/c-semantics-deps" - ############ # Build K. # ############ +# This is where the rest of the dependencies go. +ENV DEPS_DIR="/home/user/c-semantics-deps" +ENV PATH="${DEPS_DIR}/k/llvm-backend/src/main/native/llvm-backend/build/bin:${PATH}" +ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin" + COPY --chown=user:user ./.build/k/ ${DEPS_DIR}/k RUN cd ${DEPS_DIR}/k \ - && mvn package -q -U \ + && mvn package -e -q -U \ -DskipTests -DskipKTest \ - -Dhaskell.backend.skip -Dllvm.backend.skip \ - -Dcheckstyle.skip + -Dhaskell.backend.skip \ + -Dcheckstyle.skip \ + -Dproject.build.type=FastBuild -ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin" From 9bd143f45cccb9c3ec000b97418681d648beb4cd Mon Sep 17 00:00:00 2001 From: chathhorn Date: Thu, 29 Aug 2019 19:05:36 -0500 Subject: [PATCH 47/84] Jenkinsfile: disable rule parse profiling. --- Jenkinsfile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index 97d6576d9..bd36c62d9 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -34,13 +34,13 @@ pipeline { eval $(opam config env) eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib) export KOMPILE_FLAGS=-O2 - make -j4 profile-rule-parsing --output-sync=line + make -j4 --output-sync=line ''' } } } - post { success { - archiveArtifacts 'dist/timelogs.d/timelogs.csv' - } } + // post { success { + // archiveArtifacts 'dist/timelogs.d/timelogs.csv' + // } } } stage ( 'Re-compile w/ timeout' ) { steps { timeout(time: 8, unit: 'SECONDS' ) { From 61bccb4f09a8aa339d2fe438dab456751abcce91 Mon Sep 17 00:00:00 2001 From: chathhorn Date: Thu, 19 Sep 2019 11:38:41 -0500 Subject: [PATCH 48/84] Jenkinsfile: remove parse profiling. --- Jenkinsfile | 3 --- 1 file changed, 3 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index bd36c62d9..4aa386f85 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -38,9 +38,6 @@ pipeline { ''' } } } - // post { success { - // archiveArtifacts 'dist/timelogs.d/timelogs.csv' - // } } } stage ( 'Re-compile w/ timeout' ) { steps { timeout(time: 8, unit: 'SECONDS' ) { From 6be94d3bcf29ae38b28117fa788b6a1e1c107477 Mon Sep 17 00:00:00 2001 From: chathhorn Date: Tue, 22 Oct 2019 15:55:08 -0500 Subject: [PATCH 49/84] Enable kore output for C++ parser. --- scripts/kcc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/kcc b/scripts/kcc index 4236a0256..63b802198 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -618,7 +618,7 @@ sub parse { push(@cppParserArgs, '-fno-diagnostics-color'); } - shell($cppParser, $ppResult, '--', @cppParserArgs)->verbose()->stdout($kast)->run(); + shell($cppParser, $ppResult, '--kore', '--', @cppParserArgs)->verbose()->stdout($kast)->run(); return $kast; } From b12feca589d4ad5f29c20941098d2f9c2c332fd9 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 6 Feb 2020 16:22:11 +0100 Subject: [PATCH 50/84] generate readable dumps --- scripts/RV_Kcc/Shell.pm | 32 ++++++++++++++++++++++++-------- scripts/kcc | 7 ++++--- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/scripts/RV_Kcc/Shell.pm b/scripts/RV_Kcc/Shell.pm index 2590be447..67fc5bcfd 100644 --- a/scripts/RV_Kcc/Shell.pm +++ b/scripts/RV_Kcc/Shell.pm @@ -11,12 +11,12 @@ use File::Spec::Functions qw(catfile); use String::ShellQuote qw(shell_quote_best_effort); use Exporter; -use RV_Kcc::Files qw(tempFile kBinDir IS_CYGWIN); +use RV_Kcc::Files qw(profileDir tempFile kBinDir IS_CYGWIN); use constant NULL => '/dev/null'; -use constant KBIN2TEXT => do { - my $path = kBinDir('k-bin-to-text'); +use constant KAST => do { + my $path = kBinDir('kast'); my $ext = IS_CYGWIN? '.bat' : ''; $path . $ext; }; @@ -30,6 +30,7 @@ our @EXPORT_OK = qw( enableDebugging saveArgv setShellDebugFile + setLanguageDefinition shell debug ); @@ -48,18 +49,24 @@ sub debug { } } -sub shell { - my ($cmd, @args) = @_; +sub shell_ex { + my ($out, $err, $cmd, @args) = @_; my $self = { CMD => $cmd , ARGS => \@args - , STDOUT => NULL - , STDERR => NULL + , STDOUT => $out + , STDERR => $err , TMP => '' }; return (bless $self); } +sub shell { + my ($cmd, @args) = @_; + return shell_ex(NULL, NULL, $cmd, @args) + +} + sub verbose { my ($self) = @_; $self->{STDOUT} = ''; @@ -167,11 +174,20 @@ sub commandName { ($debugFile, $isBinary) = @_; } + my $languageDefinition; + sub setLanguageDefinition { + ($languageDefinition) = @_; + } + sub checkError { my ($retval) = @_; if ($retval) { if ($debugFile && $isBinary) { - shell(KBIN2TEXT, $debugFile, 'kcc_config')->result(); + shell_ex('kcc_config', NULL, KAST, + '-i', 'kore', + '-o', 'pretty', + '-d', $languageDefinition, + $debugFile)->result(); } elsif ($debugFile) { copy($debugFile, 'kcc_config'); } diff --git a/scripts/kcc b/scripts/kcc index 63b802198..6e7976c8c 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -20,7 +20,7 @@ use RV_Kcc::Opts qw( cppArgs suppressions ifdefs ldArgs nativeObjFiles srcFiles objFiles trampolineFiles breakpoints RVMAIN BASE_LIBS MAGIC ); -use RV_Kcc::Shell qw(shell checkError setShellDebugFile saveArgv debug); +use RV_Kcc::Shell qw(shell checkError setShellDebugFile setLanguageDefinition saveArgv debug); # Here we trap control-c (and others) so we can clean up when that happens. $SIG{'ABRT'} = 'interruptHandler'; @@ -527,8 +527,8 @@ sub getTranslationCommand { my $cTransDef = profileDir("c-translation-kompiled"); my $cppTransDef = profileDir("cpp-translation-kompiled"); - my @krun = getKRunCommand($output, - $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled'); + my $def = $lang eq 'c++'? 'cpp-translation-kompiled' : 'c-translation-kompiled'; + my @krun = getKRunCommand($output, $def); if (arg('-ftranslation-depth=')) { push(@krun, '--depth'); @@ -548,6 +548,7 @@ sub getTranslationCommand { my $kast = parse($src, $lang, $trampolines); @krun = addArg("PGM", $kast, 'KItem', 'korefile', @krun); + setLanguageDefinition(profileDir($def)); setShellDebugFile($output, 1); return @krun; } From ae8d900d5d9c014280cc5e1e93895e80294653e1 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 6 Feb 2020 16:43:01 +0100 Subject: [PATCH 51/84] llvm-krun -save-temps --- scripts/kcc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/kcc b/scripts/kcc index 6e7976c8c..3dd7ff2a0 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -444,6 +444,9 @@ sub getKRunCommand { , $dir , '--output-file', $output ); + if (arg('-d')) { + push(@krun, '-save-temps'); + } } else { @krun = ( KRUN From 0d2a4bdf3000a7b5d98f1126598c50598200bfce Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 2 Mar 2020 13:03:39 +0100 Subject: [PATCH 52/84] kcc -fdebug-translation --- scripts/RV_Kcc/Opts.pm | 1 + scripts/kcc | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/scripts/RV_Kcc/Opts.pm b/scripts/RV_Kcc/Opts.pm index fc93e8d52..1d0700590 100644 --- a/scripts/RV_Kcc/Opts.pm +++ b/scripts/RV_Kcc/Opts.pm @@ -447,6 +447,7 @@ sub parseOpts { for GCC. { RV_Kcc::Opts::pushArg('cppArgs', "-d$chars"); } -ftranslation-depth= Compile program up to a given depth. [undocumented] + -fdebug-translation Run translation semantics with GDB. [undocumented] -flinking-depth= Link program up to a given depth. [undocumented] -fmessage-length=0 Write all error messages on a single line. -frunner-script Compile program to perl script with analysis tool options. [undocumented] diff --git a/scripts/kcc b/scripts/kcc index 3dd7ff2a0..2c7cac6ee 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -538,6 +538,10 @@ sub getTranslationCommand { push(@krun, arg('-ftranslation-depth=')); } + if (arg('-fdebug-translation')) { + push(@krun, '--debug'); + } + my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING); my $json = "\\dv{SortString{}}($rvErrorJson)"; From 04e280cb9b1275ed35792b136bff2ee1b877d9b2 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 5 Mar 2020 11:39:18 +0100 Subject: [PATCH 53/84] append sorts to symbols --- clang-tools/ClangKast/GetKastVisitor.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 0362d1168..2b8f1d8dc 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -266,7 +266,7 @@ class GetKastVisitor bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) { if (!info) { if (decl == 0) { - Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME)); + Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME)); } else { Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING})); VisitUnsigned((unsigned long long)decl); @@ -1503,7 +1503,7 @@ class GetKastVisitor switch (Kind) { #define OVERLOADED_OPERATOR(Name,Spelling,Token,Unary,Binary,MemberOnly) \ case OO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; #include "clang/Basic/OperatorKinds.def" default: @@ -1515,7 +1515,7 @@ class GetKastVisitor switch (Kind) { #define UNARY_OP(Name, Spelling) \ case UO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; UNARY_OP(PostInc, "_++") UNARY_OP(PostDec, "_--") @@ -1548,7 +1548,7 @@ class GetKastVisitor switch (Kind) { #define BINARY_OP(Name, Spelling) \ case BO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ break; BINARY_OP(PtrMemD, ".*") BINARY_OP(PtrMemI, "->*") @@ -2250,7 +2250,7 @@ class GetKastVisitor VisitUnsigned(presumed.getColumn()); VisitBool(mgr.isInSystemHeader(loc)); } else { - Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC)); + Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC)); } } From b904c32a6aa6b026ee6c681f4d07348d7322378f Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 5 Mar 2020 14:20:59 +0100 Subject: [PATCH 54/84] fix lookupEnumerator --- .build/k | 2 +- semantics/cpp/language/translation/name.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.build/k b/.build/k index 748a6d579..739907788 160000 --- a/.build/k +++ b/.build/k @@ -1 +1 @@ -Subproject commit 748a6d57943317c0470eb8a136c205fd4da3029f +Subproject commit 739907788e2aa66cf90ea5ef008d9455dd91682f diff --git a/semantics/cpp/language/translation/name.k b/semantics/cpp/language/translation/name.k index 54893f216..8c9434fbd 100644 --- a/semantics/cpp/language/translation/name.k +++ b/semantics/cpp/language/translation/name.k @@ -263,7 +263,7 @@ module CPP-TRANSLATION-NAME ... X |-> V::PRVal requires variable in Mask - rule lookupEnumerator(X::CId, E::Enum, Mask::Set, C:K) => #if C ==K .K #then prv(V, Tr, ET) #else classSet(prv(V, Tr, ET), {C}:>Class :: X, SetItem({C}:>Class)) #fi ... + rule lookupEnumerator(X::CId, E::Enum, Mask::Set, C:K) => #if C ==K .K #then {prv(V, Tr, ET)}:>KItem #else {classSet(prv(V, Tr, ET), {C}:>Class :: X, SetItem({C}:>Class))}:>KItem #fi ... Sc::Scope E ET::CPPType From bd1fd9cd9e146aee8bd696245751fe3c59c21119 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 5 Mar 2020 11:39:29 +0100 Subject: [PATCH 55/84] fix --- semantics/cpp/language/common/dynamic.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index 97af1464c..09cd777b7 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -273,8 +273,8 @@ module CPP-QUALID-SYNTAX imports CPP-QUALID-SORTS // self imports CPP-SORTS // CId, Name - syntax NNS ::= NoNNS() - | NNS "::" NNSSpecifier [klabel(NestedName)] + syntax NNS ::= NoNNS() [symbol] + | NNS "::" NNSSpecifier [klabel(NestedName), symbol] syntax NNSSpecifier ::= NNS(CId) | TemplateNNS(CId) From 722765b7718ce4f1bddbdc5695a62ad1f3f1494c Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 13 Mar 2020 11:04:13 +0100 Subject: [PATCH 56/84] rename isNoInit => hasInit --- semantics/cpp/language/translation/decl/initializer.k | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k index a4e29abcb..e39c72d7e 100644 --- a/semantics/cpp/language/translation/decl/initializer.k +++ b/semantics/cpp/language/translation/decl/initializer.k @@ -329,13 +329,13 @@ module CPP-TRANSLATION-DECL-INITIALIZER syntax Bool ::= hasInit(CId, Map) [function] - rule hasInit(X:CId, X |-> M::Map _) => notBool isNoInit(M) + rule hasInit(X:CId, X |-> M::Map _) => notBool hasNoInit(M) - syntax Bool ::= isNoInit(Map) [function] + syntax Bool ::= hasNoInit(Map) [function] - rule isNoInit(_ |-> (_, NoInit())) => true + rule hasNoInit(_ |-> (_, NoInit())) => true - rule isNoInit(_ |-> _) => false [owise] + rule hasNoInit(_ |-> _) => false [owise] syntax Expr ::= classAggInit(base: LVal, fields: List, initList: List, initializers: Map, class: Class, initExp: K, ctype: ConstructorType, duration: Duration) From f8f01a32ec7f4d69351701472a5d635d86a06c99 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 13 Mar 2020 14:10:23 +0100 Subject: [PATCH 57/84] Revert "append sorts to symbols" This reverts commit bb1a33f03aa2d6c4b0992c78e4cc84e59825732a. --- clang-tools/ClangKast/GetKastVisitor.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 2b8f1d8dc..0362d1168 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -266,7 +266,7 @@ class GetKastVisitor bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) { if (!info) { if (decl == 0) { - Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME)); + Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME)); } else { Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING})); VisitUnsigned((unsigned long long)decl); @@ -1503,7 +1503,7 @@ class GetKastVisitor switch (Kind) { #define OVERLOADED_OPERATOR(Name,Spelling,Token,Unary,Binary,MemberOnly) \ case OO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ break; #include "clang/Basic/OperatorKinds.def" default: @@ -1515,7 +1515,7 @@ class GetKastVisitor switch (Kind) { #define UNARY_OP(Name, Spelling) \ case UO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ break; UNARY_OP(PostInc, "_++") UNARY_OP(PostDec, "_--") @@ -1548,7 +1548,7 @@ class GetKastVisitor switch (Kind) { #define BINARY_OP(Name, Spelling) \ case BO_##Name: \ - Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \ + Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \ break; BINARY_OP(PtrMemD, ".*") BINARY_OP(PtrMemI, "->*") @@ -2250,7 +2250,7 @@ class GetKastVisitor VisitUnsigned(presumed.getColumn()); VisitBool(mgr.isInSystemHeader(loc)); } else { - Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC)); + Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC)); } } From 36408873c7b9c8e7af23ae57b033593f78defbac Mon Sep 17 00:00:00 2001 From: chathhorn Date: Tue, 22 Oct 2019 17:52:32 -0500 Subject: [PATCH 58/84] C++ semantics [symbol] tags. --- semantics/cpp/language/translation/syntax.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index a61bd8756..e390f2eac 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -191,7 +191,7 @@ module CPP-ABSTRACT-SYNTAX | ForTStmt(Stmt, Decl, Stmt, Stmt) | ForTStmt(Expr, Stmt, Stmt) | TemplateDefinitionStmt(K) [symbol] // synthetic statement created by the body of a function template definition when it's evaluted before instantiation - | TReturnOp(init: Expr, obj: K) + | TReturnOp(init: Expr, obj: K) [symbol] syntax AStmt ::= NoStatement() [symbol] | CompoundAStmt(List) [symbol] From 315a00db66856eebf09c884b84cc608ec0f633a5 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 27 Mar 2020 11:37:52 +0100 Subject: [PATCH 59/84] update K --- .build/k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.build/k b/.build/k index 739907788..51686b228 160000 --- a/.build/k +++ b/.build/k @@ -1 +1 @@ -Subproject commit 739907788e2aa66cf90ea5ef008d9455dd91682f +Subproject commit 51686b228230341d0fb851767734ed44d88ecfcb From cc2ef4388dec948b4db464b99e9a7b9c9fbb9da7 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 27 Mar 2020 11:39:18 +0100 Subject: [PATCH 60/84] llvm debug --- semantics/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/semantics/Makefile b/semantics/Makefile index 1143222d4..3ebc11bd2 100644 --- a/semantics/Makefile +++ b/semantics/Makefile @@ -27,6 +27,7 @@ KOMPILE_FLAGS += --no-prelude KOMPILE_FLAGS += -w all KOMPILE_FLAGS += -v KOMPILE_FLAGS += --debug +KOMPILE_FLAGS += -ccopt -g # Used specifically in the timestamp_of rules. From f35abc8d7393c5d2275288cf0a8e4f9ac251346d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 25 Mar 2020 11:27:19 +0100 Subject: [PATCH 61/84] UnknownCabsLoc --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 0362d1168..4b68b3121 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -2250,7 +2250,7 @@ class GetKastVisitor VisitUnsigned(presumed.getColumn()); VisitBool(mgr.isInSystemHeader(loc)); } else { - Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC)); + Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC)); } } From 0d13a7495ef16e03cdd84ba52925e0ca614b7496 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 1 Apr 2020 11:50:04 +0200 Subject: [PATCH 62/84] workaround for K bug https://github.com/kframework/k/issues/1193 --- semantics/common/configuration.k | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/semantics/common/configuration.k b/semantics/common/configuration.k index 7ecccd4be..a482f4cc5 100644 --- a/semantics/common/configuration.k +++ b/semantics/common/configuration.k @@ -6,6 +6,9 @@ module COMMON-CONFIGURATION imports STRING-SYNTAX imports COMMON-SYNTAX + syntax Enum ::= DummyEnum() + syntax Class ::= DummyClass() + configuration .Map @@ -101,7 +104,7 @@ module COMMON-CONFIGURATION - .K + DummyClass() .K true .List @@ -127,7 +130,7 @@ module COMMON-CONFIGURATION - .K + DummyEnum() .K false .Map From dd089789831d8ea1644af583f7f32c5c097466b4 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 1 Apr 2020 17:58:42 +0200 Subject: [PATCH 63/84] C++ parser: toplevel sort is KItem --- clang-tools/ClangKast/ClangKast.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/ClangKast.cc b/clang-tools/ClangKast/ClangKast.cc index bed0c41aa..99ecb3cb7 100644 --- a/clang-tools/ClangKast/ClangKast.cc +++ b/clang-tools/ClangKast/ClangKast.cc @@ -330,7 +330,7 @@ void Kast::add(const T & node) { Kast::Nodes.push_back(make_unique(node)); } -void Kast::print() { print(Sort::K, 0); } +void Kast::print() { print(Sort::KITEM, 0); } int Kast::print(Sort parentSort, int idx) { if (!Nodes[idx]) throw logic_error("parse error"); From 0de15eb647d5d183a7e1fb1e20b8c574ca0ce28a Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 2 Apr 2020 11:38:48 +0200 Subject: [PATCH 64/84] C++ parser #NoName --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 4b68b3121..76bd2cb87 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -266,7 +266,7 @@ class GetKastVisitor bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) { if (!info) { if (decl == 0) { - Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME)); + Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME)); } else { Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING})); VisitUnsigned((unsigned long long)decl); From 63b33c71b1ad3bbe0aa94402e1911c6014de5748 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 24 Apr 2020 16:32:44 +0000 Subject: [PATCH 65/84] fix kcc script merge conflict --- scripts/kcc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/kcc b/scripts/kcc index 2c7cac6ee..f37d54d42 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -358,16 +358,16 @@ sub makeOptions { if (arg('-funresolved-symbols=')) { my $string_arg = arg('-funresolved-symbols='); if ($string_arg eq 'ignore-all') { - push(@options, "`UnresolvedSymbols`(`IgnoreAll`(.KList))"); + push(@options, "LblUnresolvedSymbols{}(LblIgnoreAll{}())"); } elsif ($string_arg eq 'warn-all') { - push(@options, "`UnresolvedSymbols`(`WarnAll`(.KList))"); + push(@options, "LblUnresolvedSymbols{}(LblWarnAll{}())"); } elsif ($string_arg eq 'report-all') { - push(@options, "`UnresolvedSymbols`(`ReportAll`(.KList))"); + push(@options, "LblUnresolvedSymbols{}(LblReportAll{}())"); } elsif ($string_arg eq 'warn-unreachable') { - push(@options, "`UnresolvedSymbols`(`WarnUnreachable`(.KList))"); + push(@options, "LblUnresolvedSymbols{}(LblWarnUnreachable{}())"); } } else { - push(@options, "`UnresolvedSymbols`(`WarnUnreachable`(.KList))"); + push(@options, "LblUnresolvedSymbols{}(LblWarnUnreachable{}())"); } for (breakpoints()) { From 998108d6f2f5f3b2690d97b2720f75ea56236b24 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 29 Apr 2020 14:07:07 +0200 Subject: [PATCH 66/84] fix checkLoc [owise] works only for functions --- semantics/c/language/common/check-use.k | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/semantics/c/language/common/check-use.k b/semantics/c/language/common/check-use.k index 22962ed98..316ae1e6e 100644 --- a/semantics/c/language/common/check-use.k +++ b/semantics/c/language/common/check-use.k @@ -3,7 +3,7 @@ module C-CHECK-USE-SYNTAX imports SYMLOC-SORTS syntax KItem ::= checkUse(KItem) [strict] - syntax KItem ::= checkLoc(SymLoc) + syntax K ::= checkLoc(SymLoc) [function] endmodule @@ -43,21 +43,18 @@ module C-CHECK-USE [structural] syntax Error ::= "errorLinkUnresolved" - rule checkLoc(loc(Base:LinkBase, _)) + rule checkLoc(loc(Base:LinkBase, _)) => EXT-UNDEF("TDR2", "No definition for symbol with external linkage.") ~> errorLinkUnresolved - ... requires currentSemantics() ==K ExecutionSemantics() - [structural] - rule checkLoc(loc(Base:LinkBase, _, _)) + + rule checkLoc(loc(Base:LinkBase, _, _)) => EXT-UNDEF("TDR2", "No definition for symbol with external linkage.") ~> errorLinkUnresolved - ... requires currentSemantics() ==K ExecutionSemantics() - [structural] - rule checkLoc(Loc::SymLoc) => checkLocAllowLink(Loc) - ... - [structural, owise] + + rule checkLoc(Loc::SymLoc) => checkLocAllowLink(Loc) + [owise] syntax KItem ::= checkLocAllowLink(SymLoc) From 61249773e551afe2b6aa9ee8475f908a7d06355b Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 29 Apr 2020 19:02:39 +0200 Subject: [PATCH 67/84] fix missing [function] --- semantics/common/options.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/semantics/common/options.k b/semantics/common/options.k index 3b2233cee..a67d82455 100644 --- a/semantics/common/options.k +++ b/semantics/common/options.k @@ -12,7 +12,7 @@ module OPTIONS-SYNTAX | WarnAll() [symbol] | WarnUnreachable() [symbol] - syntax String ::= showUnresolvedSymbolsOpt(UnresolvedSymbolsOpt) + syntax String ::= showUnresolvedSymbolsOpt(UnresolvedSymbolsOpt) [function] syntax Opt ::= Debug() [symbol] | Link() [symbol] // Resolve uses to definitions. From c323c294cae409b307a23b2e535269cfa27346d4 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 29 Apr 2020 20:42:12 +0200 Subject: [PATCH 68/84] little refactoring --- clang-tools/ClangKast/GetKastVisitor.h | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 24abf1c49..405c8001c 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -564,21 +564,16 @@ class GetKastVisitor } void VisitAccessSpecifier(AccessSpecifier Spec) { - const char *spec; - switch (Spec) { - case AS_public: - spec = "Public"; - break; - case AS_protected: - spec = "Protected"; - break; - case AS_private: - spec = "Private"; - break; - case AS_none: - spec = "NoAccessSpec"; - break; - } + const char * const spec = [&]{ + switch (Spec) { + case AS_public: return "Public"; + case AS_protected: return "Protected"; + case AS_private: return "Private"; + case AS_none: return "NoAccessSpec"; + } + assert(false && "Unknown access specifier"); + return (const char *)nullptr; + }(); Kast::add(Kast::KApply(spec, Sort::ACCESSSPECIFIER)); } From a937f17293f0a250354809d69e7d6b9b87d75223 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 29 Apr 2020 20:42:31 +0200 Subject: [PATCH 69/84] fix missing [symbol] --- semantics/cpp/language/common/syntax.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/semantics/cpp/language/common/syntax.k b/semantics/cpp/language/common/syntax.k index 3233c2ce6..6e3e0d894 100644 --- a/semantics/cpp/language/common/syntax.k +++ b/semantics/cpp/language/common/syntax.k @@ -101,7 +101,7 @@ module CPP-SYNTAX syntax Tag ::= ClassKey | Enum() [symbol] | Typename() [symbol] | NoTag() [symbol] - syntax AccessSpecifier ::= Public() [symbol] | Private() [symbol] | Protected() [symbol] | NoAccessSpec() + syntax AccessSpecifier ::= Public() [symbol] | Private() [symbol] | Protected() [symbol] | NoAccessSpec() [symbol] syntax RefQualifier ::= RefLValue() [symbol] | RefRValue() [symbol] | RefNone() [symbol] From 76e595315a0a6edba6f0dccc946e4cdf1cb26c45 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 30 Apr 2020 11:27:46 +0200 Subject: [PATCH 70/84] Constructor takes AStmt --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- semantics/cpp/language/translation/syntax.k | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 405c8001c..4269607b8 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -455,7 +455,7 @@ class GetKastVisitor if (D->isThisDeclarationADefinition()) { if (CXXConstructorDecl *Ctor = dyn_cast(D)) { - Kast::add(Kast::KApply("Constructor", Sort::STMT, {Sort::LIST, Sort::STMT})); + Kast::add(Kast::KApply("Constructor", Sort::STMT, {Sort::LIST, Sort::ASTMT})); int i = 0; for (auto *I : Ctor->inits()) { if (I->isWritten()) i++; diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index fbf60c44f..15131feaf 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -214,7 +214,7 @@ module CPP-ABSTRACT-SYNTAX syntax Stmt ::= Defaulted() [symbol] | Deleted() [symbol] - | Constructor(List, Stmt) [symbol] + | Constructor(List, AStmt) [symbol] | Destructor() [symbol] syntax CatchDecl ::= Decl | Ellipsis() [symbol] From 0c3571d64d2b1174984b2f96cd77d05e53820c10 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 30 Apr 2020 11:41:52 +0200 Subject: [PATCH 71/84] Revert "fix csetunion" This reverts commit 8219c337881dd474bb5c8ed08a34de4ef0d9619d. --- semantics/cpp/language/translation/overloading.k | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/semantics/cpp/language/translation/overloading.k b/semantics/cpp/language/translation/overloading.k index a81398b60..c7b926cb2 100644 --- a/semantics/cpp/language/translation/overloading.k +++ b/semantics/cpp/language/translation/overloading.k @@ -126,8 +126,7 @@ module CPP-TRANSLATION-OVERLOADING // strict version rule cSetUnion(notFound(_), E::Expr) => E - rule cSetUnion(E:KResult, notFound(_)) => E - requires notFound(_) :/=K E andBool cSet(_,_) :/=K E + rule cSetUnion(E::Expr, notFound(_)) => E rule cSetUnion(cSet(M1::Map, QX::QualId), cSet(M2::Map, QX)) => cSet(M1 M2, QX) From 614aeca6ff109d1c0e68cd142a76fa18dfaf0568 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 30 Apr 2020 12:24:17 +0200 Subject: [PATCH 72/84] make csetunion work with types --- semantics/cpp/language/translation/overloading.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/translation/overloading.k b/semantics/cpp/language/translation/overloading.k index c7b926cb2..22bf45f32 100644 --- a/semantics/cpp/language/translation/overloading.k +++ b/semantics/cpp/language/translation/overloading.k @@ -124,9 +124,9 @@ module CPP-TRANSLATION-OVERLOADING rule getArgs(Args::List, _, constructor, _) => Args // strict version - rule cSetUnion(notFound(_), E::Expr) => E + rule cSetUnion(notFound(_), E::KItem) => E - rule cSetUnion(E::Expr, notFound(_)) => E + rule cSetUnion(E::KItem, notFound(_)) => E rule cSetUnion(cSet(M1::Map, QX::QualId), cSet(M2::Map, QX)) => cSet(M1 M2, QX) From 93a6b30d7b20c4c7b76d00979a348a8b7a6b444e Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 30 Apr 2020 13:01:22 +0200 Subject: [PATCH 73/84] fix sorts --- semantics/cpp/language/common/typing.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantics/cpp/language/common/typing.k b/semantics/cpp/language/common/typing.k index 90f9cf2d5..d4e0fd1bd 100644 --- a/semantics/cpp/language/common/typing.k +++ b/semantics/cpp/language/common/typing.k @@ -409,7 +409,7 @@ module CPP-TYPING rule getParams(t(_, _, functionType(... paramTypes: L::CPPTypes, methodInfo: methodInfo(... constructor: true)))) => toList(L) - rule getParams(t(_, _, functionType(... paramTypes: L::CPPTypes, methodInfo: methodInfo(RQ::RefQualifier, CVS::Quals, IsStatic::Bool, _, _, _, C::Class, _, false)))) => ListItem(implicitObjectParameter(getImpliedParamType(RQ, CVS, IsStatic, C))) toList(L) + rule getParams(t(_, _, functionType(... paramTypes: L::CPPTypes, methodInfo: methodInfo(RQ::RefQualifier, CVS::Quals, IsStatic::Bool, _, _, _, C::K, _, false)))) => ListItem(implicitObjectParameter(getImpliedParamType(RQ, CVS, IsStatic, C))) toList(L) rule getRealParams(T::CPPType) => #getRealParams(getParams(T)) @@ -451,7 +451,7 @@ module CPP-TYPING rule hasImplicitParameter(_) => false [owise] // TODO(traiansf): Handle conversion functions and functions introduced by using declarations - syntax CPPType ::= getImpliedParamType(RefQualifier, Quals, static: Bool, Class) [function] + syntax CPPType ::= getImpliedParamType(RefQualifier, Quals, static: Bool, class: K) [function] // 13.3.1:4 rule getImpliedParamType(... static: true) => type(no-type) From 45c70babbd037ad2899988ebb3ee32f80c2d74f9 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 30 Apr 2020 13:48:02 +0200 Subject: [PATCH 74/84] remove the content of `` in the link time it is not used during execution, but it can contain translation labels --- semantics/linking/init.k | 3 +++ 1 file changed, 3 insertions(+) diff --git a/semantics/linking/init.k b/semantics/linking/init.k index 4b698cb79..e1b1b3abe 100644 --- a/semantics/linking/init.k +++ b/semantics/linking/init.k @@ -373,4 +373,7 @@ module LINKING-INIT rule hasTrace(_) => noTrace [anywhere] + rule M => .Map + requires M =/=K .Map [anywhere] + endmodule From 3dd482dc460fb88f8ac931a2e5d0a95f1a2bc70e Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 30 Apr 2020 16:59:53 +0200 Subject: [PATCH 75/84] fix sorts --- semantics/cpp/language/translation/env.k | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/semantics/cpp/language/translation/env.k b/semantics/cpp/language/translation/env.k index 14d82cc72..06eaae10e 100644 --- a/semantics/cpp/language/translation/env.k +++ b/semantics/cpp/language/translation/env.k @@ -17,7 +17,7 @@ module CPP-TRANSLATION-ENV-SYNTAX syntax KItem ::= "pushLocals" | "popLocals" - syntax KItem ::= updateDefaultArguments(QualId, CPPType, DefaultArguments) [strict(3)] + syntax KItem ::= updateDefaultArguments(QualId, CPPType, DefaultArguments) syntax List ::= getDefaultArgsVals(DefaultArgumentsResult) [function] @@ -42,6 +42,11 @@ module CPP-TRANSLATION-ENV rule updateDefaultArguments(_, T::CPPType, _) => .K requires notBool isCPPFunctionType(T) + // if T is not a function type, the HOLE evaluates to `krlist`, + // which is not of sort `DefaultArguments` + context updateDefaultArguments(_, T::CPPType, HOLE:DefaultArguments) + requires isCPPFunctionType(T) + rule addToEnv(N:Namespace :: X::CId, t(... st: functionType(...)) #as T::CPPType, Base::SymBase, IsUsing::Bool) => .K ... From 8810ac88e8ab4fba3c904e6559485ebde0467865 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Fri, 1 May 2020 14:50:00 +0200 Subject: [PATCH 76/84] parser: skip default arguments in a call --- clang-tools/ClangKast/GetKastVisitor.h | 30 +++++++++++++++----------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index 4269607b8..e6b467519 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -1444,19 +1444,23 @@ class GetKastVisitor bool TraverseCallExpr(CallExpr *E) { Kast::add(Kast::KApply("CallExpr", Sort::RESOLVEDEXPR, {Sort::EXPR, Sort::STRICTLIST, Sort::STRICTLISTRESULT})); - unsigned i = 0; - for (Stmt *SubStmt : E->children()) { - i++; - } - if (i-1 != E->getNumArgs()) { - throw std::logic_error("unimplemented: pre_args???"); - } - bool first = true; - for (Stmt *SubStmt : E->children()) { - TRY_TO(TraverseStmt(SubStmt)); - if (first) List(i-1); - first = false; - } + + // 1 + TRY_TO(TraverseStmt(E->getCallee())); + + // 2 + Kast::add(Kast::KApply("list", Sort::STRICTLIST, {Sort::LIST})); + for (unsigned int i = 0; i < E->getNumArgs(); i++) { + clang::Expr * arg = E->getArg(i); + if (!isa(arg)) { + Kast::add(Kast::KApply("_List_", Sort::LIST, {Sort::LIST, Sort::LIST})); + Kast::add(Kast::KApply("ListItem", Sort::LIST, {Sort::KITEM})); + TRY_TO(TraverseStmt(arg)); + } + } + Kast::add(Kast::KApply(".List", Sort::LIST)); + + // 3 Kast::add(Kast::KApply("krlist", Sort::STRICTLISTRESULT, {Sort::LIST})); Kast::add(Kast::KApply(".List", Sort::LIST)); return true; From 8dcf2ed581a7214f13cbef33d0b9ea4fee8e59ba Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 11 May 2020 16:12:14 +0200 Subject: [PATCH 77/84] fix sorts --- semantics/cpp/language/execution/binding.k | 13 ++++++++++--- semantics/cpp/language/execution/expr/members.k | 4 ++-- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/semantics/cpp/language/execution/binding.k b/semantics/cpp/language/execution/binding.k index febb7868f..3fe7027bf 100644 --- a/semantics/cpp/language/execution/binding.k +++ b/semantics/cpp/language/execution/binding.k @@ -8,7 +8,7 @@ module CPP-BINDING-SYNTAX syntax KItem ::= bindParam(CId, CPPType, Init) [klabel(bindParamCpp3)] - syntax KItem ::= setThis(Expr) [strict(c)] + syntax KItem ::= setThis(K) endmodule module CPP-EXECUTION-BINDING @@ -23,6 +23,13 @@ module CPP-EXECUTION-BINDING imports CPP-SYNTAX imports CPP-TYPING-SYNTAX + rule setThis(.K) => .K ... + _ => .K + + rule setThis(E:Expr) => #setThis(E) + + syntax KItem ::= #setThis(Expr) [strict(c)] + rule (.K => bindParam(X, T, V)) ~> bind( (ListItem(X::CId) => .List) _, @@ -30,7 +37,7 @@ module CPP-EXECUTION-BINDING (ListItem(V::Init) => .List) _) ... - rule (.K => setThis(V)) + rule (.K => #setThis(V)) ~> bind( _, (ListItem(implicitObjectParameter(T::CPPType)) => .List) _, @@ -52,7 +59,7 @@ module CPP-EXECUTION-BINDING rule bindVariadics(.List) => .K - rule setThis(Obj:PRVal) => .K ... + rule #setThis(Obj:PRVal) => .K ... _ => Obj rule beginConstruction(Obj:LVal, IsBaseClassSubobject:Bool) => Obj ... diff --git a/semantics/cpp/language/execution/expr/members.k b/semantics/cpp/language/execution/expr/members.k index b44c53fb6..184a02717 100644 --- a/semantics/cpp/language/execution/expr/members.k +++ b/semantics/cpp/language/execution/expr/members.k @@ -15,10 +15,10 @@ module CPP-EXECUTION-EXPR-MEMBERS rule evalBraceOrEqualInitializer(C::Class, lv(Loc::SymLoc, Tr::Trace, T::CPPType) #as Base::LVal, E::Expr) => setThis(prv(Loc, Tr, type(pointerType(type(classType(C)))))) ~> E ~> returnFromBraceOrEqualInitializer(Base, OldScope) ~> setThis(OldThis) ... OldScope::Scope => classScope(C, true) - OldThis::PRVal + OldThis::K requires Execution() - rule V:Val ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) ~> setThis(OldThis::PRVal) => .K) ... + rule V:Val ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) ~> setThis(OldThis::K) => .K) ... _ => Scope _ => OldThis requires Execution() andBool notBool (isLExpr(V) orBool isPRExpr(V)) From be8951f38a9c32900854ec387a1957902acfbbbb Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Tue, 12 May 2020 15:32:57 +0200 Subject: [PATCH 78/84] fixes --- clang-tools/ClangKast/GetKastVisitor.h | 2 +- semantics/cpp/language/common/typing.k | 2 +- semantics/cpp/language/translation/overloading.k | 4 ++-- semantics/cpp/language/translation/stmt/try.k | 2 +- semantics/cpp/language/translation/syntax.k | 2 ++ 5 files changed, 7 insertions(+), 5 deletions(-) diff --git a/clang-tools/ClangKast/GetKastVisitor.h b/clang-tools/ClangKast/GetKastVisitor.h index e6b467519..80222a068 100644 --- a/clang-tools/ClangKast/GetKastVisitor.h +++ b/clang-tools/ClangKast/GetKastVisitor.h @@ -238,7 +238,7 @@ class GetKastVisitor TRY_TO(TraverseDeclarationName(NNS->getAsNamespaceAlias()->getDeclName())); break; case NestedNameSpecifier::TypeSpec: - Kast::add(Kast::KApply("NNSCId", Sort::NNSSPECIFIER, {Sort::CID})); + Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME})); TRY_TO(TraverseType(QualType(NNS->getAsType(), 0))); break; case NestedNameSpecifier::TypeSpecWithTemplate: diff --git a/semantics/cpp/language/common/typing.k b/semantics/cpp/language/common/typing.k index d4e0fd1bd..3edb74425 100644 --- a/semantics/cpp/language/common/typing.k +++ b/semantics/cpp/language/common/typing.k @@ -977,7 +977,7 @@ module CPP-TYPING rule setType(T::CPPType, lv(Loc::SymLoc, Tr::Trace, _)) => lv(Loc, Tr, T) - rule setType(T::CPPType, prv(Loc::SymLoc, Tr::Trace, _)) => prv(Loc, Tr, T) + rule setType(T::CPPType, prv(V::CPPValue, Tr::Trace, _)) => prv(V, Tr, T) rule isEnumScoped(t(_, _, scopedEnum(_, _))) => true diff --git a/semantics/cpp/language/translation/overloading.k b/semantics/cpp/language/translation/overloading.k index 22bf45f32..8c75e4872 100644 --- a/semantics/cpp/language/translation/overloading.k +++ b/semantics/cpp/language/translation/overloading.k @@ -1099,8 +1099,8 @@ module CPP-TRANSLATION-OVERLOADING #fi requires isCPPRefType(T) - rule resolveUniqueDecl(V:KResult, _, _) => V - requires notBool isCandidateSet(V) andBool notBool isNotFoundNameRef(V) + rule resolveUniqueDecl(V:KItem, _, _) => V + requires isKResult(V) andBool notBool isCandidateSet(V) andBool notBool isNotFoundNameRef(V) rule (.K => ILL("TOL1", "No declaration found for name '" +String showCId(X) +String "'.")) ~> resolveUniqueDecl(notFound(X::CId), _, _) diff --git a/semantics/cpp/language/translation/stmt/try.k b/semantics/cpp/language/translation/stmt/try.k index 06f88dead..7e9bde1d9 100644 --- a/semantics/cpp/language/translation/stmt/try.k +++ b/semantics/cpp/language/translation/stmt/try.k @@ -98,6 +98,6 @@ module CPP-TRANSLATION-STMT-TRY rule processCatchDecl(NormalizedDecl(... type: t(... st: functionType(...)) #as T::CPPType => type(pointerType(T)))) - rule processCatchDecl(D::Decl) => D [owise] + rule processCatchDecl(D::Declarator) => D [owise] endmodule diff --git a/semantics/cpp/language/translation/syntax.k b/semantics/cpp/language/translation/syntax.k index 15131feaf..9bdcaac81 100644 --- a/semantics/cpp/language/translation/syntax.k +++ b/semantics/cpp/language/translation/syntax.k @@ -99,6 +99,8 @@ module CPP-ABSTRACT-SYNTAX syntax Enumerator ::= Enumerator(CId, AExpr) [symbol] + syntax Decl ::= Enumerator + syntax CPPType // defined in CPP-TYPING-SYNTAX syntax ATypeResult ::= NoType() [symbol] From eda43b424b152486c78ca57c56b1c86eef21950d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 14 May 2020 12:01:15 +0200 Subject: [PATCH 79/84] kcc -fdebug-linking --- scripts/RV_Kcc/Opts.pm | 1 + scripts/kcc | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/scripts/RV_Kcc/Opts.pm b/scripts/RV_Kcc/Opts.pm index 1d0700590..70045e3b0 100644 --- a/scripts/RV_Kcc/Opts.pm +++ b/scripts/RV_Kcc/Opts.pm @@ -449,6 +449,7 @@ sub parseOpts { -ftranslation-depth= Compile program up to a given depth. [undocumented] -fdebug-translation Run translation semantics with GDB. [undocumented] -flinking-depth= Link program up to a given depth. [undocumented] + -fdebug-linking Run linking semantics with GDB. [undocumented] -fmessage-length=0 Write all error messages on a single line. -frunner-script Compile program to perl script with analysis tool options. [undocumented] -fissue-report= Write issues to the specified file. diff --git a/scripts/kcc b/scripts/kcc index f37d54d42..bc97b48f0 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -477,6 +477,10 @@ sub getLinkingCommand { push(@krun, arg('-flinking-depth=')); } + if (arg('-fdebug-linking')) { + push(@krun, '--debug'); + } + my ($rvErrorJson, $string) = (getRVErrorJson(), QUOTE_STRING); my $json = "\\dv{SortString{}}($rvErrorJson)"; From 3818a61d6e08bcb098518ab95702de7e49b4d923 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 14 May 2020 12:05:16 +0200 Subject: [PATCH 80/84] kcc: fix generating kcc_config from linking semantics --- scripts/kcc | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/kcc b/scripts/kcc index bc97b48f0..dbc39a7c7 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -524,6 +524,7 @@ sub getLinkingCommand { @krun = addArg("OBJS", "Lblload{}(dotk{}())", 'KItem', 'text', @krun); } + setLanguageDefinition(profileDir('c-cpp-linking-kompiled')); setShellDebugFile($output, 1); return @krun; } From 2891833a9bc5fd9cf268ff991a5c529df7f57977 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 14 May 2020 15:52:14 +0200 Subject: [PATCH 81/84] linking: overwrite with the same value --- semantics/linking/cpp-resolution.k | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/semantics/linking/cpp-resolution.k b/semantics/linking/cpp-resolution.k index b898e27ab..ae4c28558 100644 --- a/semantics/linking/cpp-resolution.k +++ b/semantics/linking/cpp-resolution.k @@ -45,7 +45,9 @@ module LINKING-CPP-RESOLUTION Tu N ... X |-> (stripType(T) |-> (_, envEntry(... base: Base::SymBase => Base')) _::Map) ... - ... .Map => Base |-> Base' ... + Linkings::Map => Linkings[Base <- Base'] + // do not overwrite the old value with a different one + requires (Linkings[Base] orDefault Base') ==K Base' rule resolveCPPReference(OdrBase::SymBase) ... ... From a5b4248e9742908aeb6cc73fb6e26f57fb901954 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 14 May 2020 15:52:50 +0200 Subject: [PATCH 82/84] brace initialization: fix sorts --- semantics/cpp/language/common/class.k | 2 +- .../cpp/language/translation/decl/class.k | 24 ++++++++++--------- .../language/translation/decl/initializer.k | 2 +- 3 files changed, 15 insertions(+), 13 deletions(-) diff --git a/semantics/cpp/language/common/class.k b/semantics/cpp/language/common/class.k index 0d28e5ff1..c8e9f050d 100644 --- a/semantics/cpp/language/common/class.k +++ b/semantics/cpp/language/common/class.k @@ -169,7 +169,7 @@ module CPP-CLASS-SYNTAX syntax Expr ::= evalBraceOrEqualInitializer(class: Class, object: Expr, initializer: Expr) [strict(c; 2)] - syntax KItem ::= returnFromBraceOrEqualInitializer(LVal, Scope) + syntax KItem ::= returnFromBraceOrEqualInitializer(Expr, Scope) syntax This ::= This() [symbol] diff --git a/semantics/cpp/language/translation/decl/class.k b/semantics/cpp/language/translation/decl/class.k index ebfec3a82..f793a021c 100644 --- a/semantics/cpp/language/translation/decl/class.k +++ b/semantics/cpp/language/translation/decl/class.k @@ -1471,22 +1471,22 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)] rule pad(V::Int, _) => V [owise] // brace-or-equal initializers need to be evalauted in class scope - rule evalBraceOrEqualInitializer(C::Class, Base::LVal, E::Expr) => E ~> returnFromBraceOrEqualInitializer(Base, OldScope) ... + rule evalBraceOrEqualInitializer(C::Class, Base::Expr, E::Expr) => E ~> returnFromBraceOrEqualInitializer(Base, OldScope) ... OldScope::Scope => classScope(C, true) - requires Translation() + requires Translation() andBool isKResult(Base) rule le(E::Expr => evalBraceOrEqualInitializer(C, Base, E), _, _) - ~> (returnFromBraceOrEqualInitializer(Base::LVal, Scope::Scope) => .K) + ~> (returnFromBraceOrEqualInitializer(Base::Expr, Scope::Scope) => .K) ... classScope(C::Class, _) => Scope rule xe(E::Expr => evalBraceOrEqualInitializer(C, Base, E), _, _) - ~> (returnFromBraceOrEqualInitializer(Base::LVal, Scope::Scope) => .K) + ~> (returnFromBraceOrEqualInitializer(Base::Expr, Scope::Scope) => .K) ... classScope(C::Class, _) => Scope rule pre(E::Expr => evalBraceOrEqualInitializer(C, Base, E), _, _) - ~> (returnFromBraceOrEqualInitializer(Base::LVal, Scope::Scope) => .K) + ~> (returnFromBraceOrEqualInitializer(Base::Expr, Scope::Scope) => .K) ... classScope(C::Class, _) => Scope @@ -1494,20 +1494,22 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)] _ => Scope requires notBool (isLExpr(V) orBool isPRExpr(V)) - rule typeof(evalBraceOrEqualInitializer(C::Class, Base::LVal, E::Expr) => E) - ~> (.K => returnFromBraceOrEqualInitializer(Base, OldScope)) + syntax KItem ::= restoreScope(Scope) + + rule typeof(evalBraceOrEqualInitializer(C::Class, _, E::Expr) => E) + ~> (.K => restoreScope(OldScope)) ... OldScope::Scope => classScope(C, true) - rule typeof(V:CPPType) ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) => .K) ... + rule typeof(V:CPPType) ~> (restoreScope(Scope::Scope) => .K) ... _ => Scope - rule catof(evalBraceOrEqualInitializer(C::Class, Base::LVal, E::Expr) => E) - ~> (.K => returnFromBraceOrEqualInitializer(Base, OldScope)) + rule catof(evalBraceOrEqualInitializer(C::Class, _, E::Expr) => E) + ~> (.K => restoreScope(OldScope)) ... OldScope::Scope => classScope(C, true) - rule catof(V:ValueCategory) ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) => .K) ... + rule catof(V:ValueCategory) ~> (restoreScope(Scope::Scope) => .K) ... _ => Scope rule Class.getNonStaticDataMembers(... L::List ...) => L diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k index b323420ab..05a61e832 100644 --- a/semantics/cpp/language/translation/decl/initializer.k +++ b/semantics/cpp/language/translation/decl/initializer.k @@ -409,7 +409,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER ~> classAggInit(... base: Base::LVal, fields: (ListItem(Class.DataMember(F:CId, _)) => .List) _, initList: .List, - initializers: (F |-> (_::CPPType |-> (T::CPPType, Init::Expr))) _, + initializers: (F |-> (_::CPPType |-> (T::CPPType, Init::Init))) _, class: C::Class, duration: D::Duration) From 8615063df1573d0bb7a20a422bf84ce10990fcd8 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 14 May 2020 16:42:16 +0200 Subject: [PATCH 83/84] for: fix sort --- semantics/cpp/language/execution/stmt/loop.k | 4 ++-- semantics/cpp/language/translation/process-label.k | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/semantics/cpp/language/execution/stmt/loop.k b/semantics/cpp/language/execution/stmt/loop.k index 744ee4518..9ddf3bc47 100644 --- a/semantics/cpp/language/execution/stmt/loop.k +++ b/semantics/cpp/language/execution/stmt/loop.k @@ -4,7 +4,7 @@ module CPP-EXECUTION-STMT-LOOP imports CPP-DYNAMIC-SYNTAX imports CPP-SYNTAX - rule ForStmt(Control::Expr, Post::Stmt, S::K) ~> K:K + rule ForStmt(Control::Expr, Post::K, S::K) ~> K:K => loopMarked ~> ForStmt(Control, Post, S) ~> popLoop @@ -12,7 +12,7 @@ module CPP-EXECUTION-STMT-LOOP ListItem(Num::Int) ... .List => ListItem(kpair(Num, K)) ... - rule loopMarked ~> ForStmt(Control:Expr, Post::Stmt, S::K) + rule loopMarked ~> ForStmt(Control:Expr, Post::K, S::K) => IfStmt(Control, compoundStmt(S, compoundStmt(Post, compoundStmt(loopMarked, ForStmt(Control, Post, S)))), nullStmt()) diff --git a/semantics/cpp/language/translation/process-label.k b/semantics/cpp/language/translation/process-label.k index 747932b26..e80f86581 100644 --- a/semantics/cpp/language/translation/process-label.k +++ b/semantics/cpp/language/translation/process-label.k @@ -106,7 +106,7 @@ module CPP-TRANSLATION-PROCESS-LABEL rule waitingOnGotoMap ... - (ForStmt(Control:Expr, Post::Stmt, S::K) => .K) + (ForStmt(Control:Expr, Post::K, S::K) => .K) ~> K:K Tail:K From e88a01b6b49fa1d53ca49c41810dd0c893684f4f Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 14 May 2020 17:05:43 +0200 Subject: [PATCH 84/84] isKResult --- semantics/cpp/language/common/dynamic.k | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/semantics/cpp/language/common/dynamic.k b/semantics/cpp/language/common/dynamic.k index aadf6738a..d2ab9a292 100644 --- a/semantics/cpp/language/common/dynamic.k +++ b/semantics/cpp/language/common/dynamic.k @@ -1006,7 +1006,8 @@ module CPP-DYNAMIC-OTHER rule showTemplateArgs(T:CPPType, T2:TemplateArg, Ts::TemplateArgs) => showCPPType(T) +String "," +String showTemplateArgs(T2, Ts) - rule _:KResult ~> discard => .K + rule X:KItem ~> discard => .K + requires isKResult(X) context makePRVal(HOLE:Expr => reval(HOLE)) ... true [result(PRV)]