Simplification rule fails to apply in the C semantics

This issue is an attempt to collect information from several other issues and Slack discussions in one place so that it can be properly investigated.

Context

In the C semantics, we found that our smoke test for the Haskell backend was failing intermittently. The code under test is a program that simply returns 42 from main; the object of the test is to assert that the Haskell backend executes this program correctly to a single output configuration. We assert that there are no #Or or #And connectives in the output configuration, and that it contains the correct return value.

At some point[^1] we noticed that this test was failing because the configuration produced by executing the program above contained an #Or connective. These failures were nondeterministic.

Initial Investigation

@mariaKt narrowed down the problem substantially by identifying that the problem occurs consistently once the program in question has been translated.[^2] Given a particular translated kore file, we could consistently observe the failure in question.

The other observation made by @mariaKt is that the configurations that succeed, and those that exhibit this bug differ only in concrete values (for strings, integers) chosen by the translation semantics. There are no structural differences between the configurations.

I investigated further, and found that the problematic configuration looked something like this:

    #Not ( {
      addressOfEntity ( unique ( "261de9ba-e84e-4428-a1fb-96bf0282dcba" , ".str.6d61696e00" , 0 ) , 5 ) +Int 2
    #Equals
      addressOfEntity ( unique ( "261de9ba-e84e-4428-a1fb-96bf0282dcba" , "__func__.main" , 0 ) , 5 ) +Int 2
    } )
  #And
    <generatedTop>
      ... successful execution, exit code 42 ...
    </generatedTop>
#Or
    <generatedTop>
      ... unsuccessful execution, stuck on <k> updateObjects </k>
    </generatedTop>
  #And
    {
      addressOfEntity ( unique ( "261de9ba-e84e-4428-a1fb-96bf0282dcba" , ".str.6d61696e00" , 0 ) , 5 ) +Int 2
    #Equals
      addressOfEntity ( unique ( "261de9ba-e84e-4428-a1fb-96bf0282dcba" , "__func__.main" , 0 ) , 5 ) +Int 2
    }

My expectation is that this configuration could in fact be simplified. We have a rule in the semantics that looks like it should apply:

  rule { addressOfEntity(E, Len) +Int Off #Equals addressOfEntity(E', Len') +Int Off' } => #Bottom
    requires E =/=K E' andBool Off <Int Len andBool Off' <Int Len' [simplification]

@ana-pantilie and I spent some time digging into this on Slack. Specifically, I added a --debug-equation call for the rule above to see when it was applying and failing to apply.

Observations

I wrote a script to parse the output of the kore-exec logs, and found that the simplification rule above seems to stop applying after a certain point, but only when the arguments to +Int are both 2.[^3] All other applications keep happening consistently as the program executes; this output counts how many times the rule applies in the log file for a particular combination of arguments:

1 1: 1885
1 2: 271
1 3: 1871
1 4: 495
2 1: 277
2 2: 8
2 3: 271
2 4: 267
3 1: 967
3 2: 271
3 3: 957
3 4: 495
4 1: 14667
4 2: 271
4 3: 7347
4 4: 495

The output I'm parsing for looks like this:

kore-exec: [11107330] Debug (DebugAttemptEquation):
    applying equation at /home/bruce/code/c-semantics/semantics/c.k:627:18-628:67 to term:
        /* Spa */
        \equals{SortInt{}, SortInt{}}(
            /* Fl Fn D Sfa */
            Lbl'UndsPlus'Int'Unds'{}(
                /* Fl Fn D Sfa */
                LbladdressOfEntity'LParUndsCommUndsRParUnds'C-EXECUTION-ADDRESSES-SYNTAX'Unds'Int'Unds'EntityId'Unds'Int{}(
                    /* Fl Fn D Sfa Cl */
                    Lblunique'LParUndsCommUndsCommUndsRParUnds'C-ENTITY-SYNTAX'Unds'EntityId'Unds'String'Unds'String'Unds'Int{}(
                        /* Fl Fn D Sfa Cl */
                        \dv{SortString{}}("261de9ba-e84e-4428-a1fb-96bf0282dcba"),
                        /* Fl Fn D Sfa Cl */
                        \dv{SortString{}}(".str.6d61696e00"),
                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                    ),
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5")
                ),
                /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2")
            ),
            /* Fl Fn D Sfa */
            Lbl'UndsPlus'Int'Unds'{}(
                /* Fl Fn D Sfa */
                LbladdressOfEntity'LParUndsCommUndsRParUnds'C-EXECUTION-ADDRESSES-SYNTAX'Unds'Int'Unds'EntityId'Unds'Int{}(
                    /* Fl Fn D Sfa Cl */
                    Lblunique'LParUndsCommUndsCommUndsRParUnds'C-ENTITY-SYNTAX'Unds'EntityId'Unds'String'Unds'String'Unds'Int{}(
                        /* Fl Fn D Sfa Cl */
                        \dv{SortString{}}("261de9ba-e84e-4428-a1fb-96bf0282dcba"),
                        /* Fl Fn D Sfa Cl */ \dv{SortString{}}("__func__.main"),
                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                    ),
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5")
                ),
                /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")
            )
        )
Context:
    (DebugAttemptEquation) while applying equation at /home/bruce/code/k/k-distribution/target/release/k/include/kframework/builtin/domains.md:422:8-422:90
        (DebugAttemptEquation) while applying equation at /home/bruce/code/c-semantics/semantics/c.k:627:18-628:67
kore-exec: [11111551] Debug (DebugAttemptEquation):
    equation is applicable

The other observation that I made was that the 2/2 argument case (i.e. the stuck configuration) appears in a slightly different context: note that there is no nesting of (DebugAttemptEquation) entries as there is above.

kore-exec: [19666609] Debug (DebugAttemptEquation):
    applying equation at /home/bruce/code/c-semantics/semantics/c.k:627:18-628:67 to term:
        /* Spa */
        \equals{SortInt{}, SortInt{}}(
            /* Fl Fn D Sfa */
            Lbl'UndsPlus'Int'Unds'{}(
                /* Fl Fn D Sfa */
                LbladdressOfEntity'LParUndsCommUndsRParUnds'C-EXECUTION-ADDRESSES-SYNTAX'Unds'Int'Unds'EntityId'Unds'Int{}(
                    /* Fl Fn D Sfa Cl */
                    Lblunique'LParUndsCommUndsCommUndsRParUnds'C-ENTITY-SYNTAX'Unds'EntityId'Unds'String'Unds'String'Unds'Int{}(
                        /* Fl Fn D Sfa Cl */
                        \dv{SortString{}}("261de9ba-e84e-4428-a1fb-96bf0282dcba"),
                        /* Fl Fn D Sfa Cl */
                        \dv{SortString{}}(".str.6d61696e00"),
                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                    ),
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5")
                ),
                /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2")
            ),
            /* Fl Fn D Sfa */
            Lbl'UndsPlus'Int'Unds'{}(
                /* Fl Fn D Sfa */
                LbladdressOfEntity'LParUndsCommUndsRParUnds'C-EXECUTION-ADDRESSES-SYNTAX'Unds'Int'Unds'EntityId'Unds'Int{}(
                    /* Fl Fn D Sfa Cl */
                    Lblunique'LParUndsCommUndsCommUndsRParUnds'C-ENTITY-SYNTAX'Unds'EntityId'Unds'String'Unds'String'Unds'Int{}(
                        /* Fl Fn D Sfa Cl */
                        \dv{SortString{}}("261de9ba-e84e-4428-a1fb-96bf0282dcba"),
                        /* Fl Fn D Sfa Cl */ \dv{SortString{}}("__func__.main"),
                        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                    ),
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5")
                ),
                /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2")
            )
        )
Context:
    (DebugAttemptEquation) while applying equation at /home/bruce/code/c-semantics/semantics/c.k:627:18-628:67
kore-exec: [19669867] Debug (DebugAttemptEquation):
    equation is applicable

No other argument combinations appear in a context like this, and there are no successful 2/2 applications after this happens:

1 1: 
1 2: 
1 3: 
1 4: 
2 1: 
2 2: 2
2 3: 
2 4: 
3 1: 
3 2: 
3 3: 
3 4: 
4 1: 
4 2: 
4 3: 
4 4: 

I'm not sure how to investigate further given these logs.

Reproduction

I've generated a set of input files that include the Haskell backend definition and translated input for the C semantics, as well as a rule name for the simplification rule in question.

Download this tarball of input files, then run:

kore-exec haskellDefinition.bin --module C --pattern smoke-test.executable.kore --output result.bad.kore --debug-equation C-EXECUTION-ADDRESSES-SYMBOLIC.broken

on the files it contains to generate the log file I mention above. You can get a copy of it directly here as well to save time.

Log Parsing Script

Needs ag to be installed. Save and run as ./script.sh $kore_exec_stderr_file

#!/usr/bin/env bash

for i in $(seq 1 4); do
  for j in $(seq 1 4); do
    echo -n "$i $j: "
    ag "SortInt{}}\(\"$i\"\)(\\n.*){15}SortInt{}}\(\"$j\"\)(\\n.*){7}is applic" -c "$1"

    if [ "$?" -ne 0 ]; then
      echo
    fi
  done
done

echo

for i in $(seq 1 4); do
  for j in $(seq 1 4); do
    echo -n "$i $j: "
    ag "SortInt{}}\(\"$i\"\)(\\n.*){15}SortInt{}}\(\"$j\"\)(\\n.*){6}is applic" -c "$1"

    if [ "$?" -ne 0 ]; then
      echo
    fi
  done
done

[^1]: Unfortunately, our CI had a reasonably serious bug that prevents us from quickly seeing exactly when the problem started.
[^2]: The C semantics translate, then execute a program in two separate execution phases. The translation phase uses the LLVM backend and is not specifically relevant here.
[^3]: The actual values differ per failing input file, but seem to be consistent for a given file.

Start with the simplification rule in semantics/c.k at lines 627–628, the smoke test in test/smoke-test.c, and its assertions in Makefile lines 16–18. Reproduce with the provided tarball using the kore-exec command and inspect the debug-equation output and parsing script; done means explaining why the 2/2 case stops simplifying and establishing a reliable correction or regression check.