search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
450 stars 149 forks source link

[K-Bug] Error in output of `kmir run` #3604

Closed dkcumming closed 1 year ago

dkcumming commented 1 year ago

What component is the issue in?

Front-End

Which command

What K Version?

v6.0.71 and back to at least v6.0.67

Operating System

Linux

K Definitions (If Possible)

No response

Steps to Reproduce

daniel@daniel-MS-7E06 mir-semantics$ git checkout origin/master
Note: switching to 'origin/master'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 576344f Add logging infrastructure (#203)
daniel@daniel-MS-7E06 mir-semantics$ cd kmir/
daniel@daniel-MS-7E06 kmir$ make build
poetry install
Installing dependencies from lock file

No dependencies to install or update

Installing the current project: kmir (0.1.0)
poetry run kbuild kompile llvm
/home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm
poetry run kbuild kompile haskell
/home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/haskell
poetry build
Building kmir (0.1.0)
  - Building sdist
  - Built kmir-0.1.0.tar.gz
  - Building wheel
  - Built kmir-0.1.0-py3-none-any.whl
daniel@daniel-MS-7E06 kmir$ poetry run kmir run --verbose --debug --definition-dir $(poetry run kbuild which llvm) --output pretty src/tests/integration/test-data/handwritten-mir/execution/arithm-simple.mir 
INFO 2023-08-25 19:27:11,048 pyk.ktool.kprint - Running: kast /home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm/parser_Mir_MIR-PARSER-SYNTAX --definition /home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm --module MIR-PARSER-SYNTAX --sort Mir --gen-glr-parser
INFO 2023-08-25 19:27:12,580 pyk.ktool.kprint - Completed in 1.532s with status 0: kast /home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm/parser_Mir_MIR-PARSER-SYNTAX --definition /home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm --module MIR-PARSER-SYNTAX --sort Mir --gen-glr-parser
INFO 2023-08-25 19:27:12,580 pyk.ktool.krun - Running: krun /tmp/tmpjy_2havf --definition /home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm --output pretty -pPGM=/home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm/parser_Mir_MIR-PARSER-SYNTAX
INFO 2023-08-25 19:27:12,657 pyk.ktool.krun - Completed in 0.077s with status 0: krun /tmp/tmpjy_2havf --definition /home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm --output pretty -pPGM=/home/daniel/.kbuild/mir-semantics/5a0ac5c/target/v6.0.71/llvm/parser_Mir_MIR-PARSER-SYNTAX
<generatedTop>
  <k>
    .
  </k>
  <returncode>
    0
  </returncode>
  <mir>
    <simulator>
      <callStack>
        .List
      </callStack>
      <currentBasicBlock>
        1
      </currentBasicBlock>
      <phase>
        Finalization
      </phase>
    </simulator>
    <data>
      <functions>
        <function>
          <fnKey>
            Fn ( main :: .FunctionPath )
          </fnKey>
          <localDecls>
            <localDecl>
              <index>
                0
              </index>
              <mutability>
                Not
              </mutability>
              <internal>
                false
              </internal>
              <ty>
                ( )
              </ty>
              <value>
                Unit
              </value>
            </localDecl> <localDecl>
              <index>
                1
              </index>
              <mutability>
                Not
              </mutability>
              <internal>
                false
              </internal>
              <ty>
                bool 
              </ty>
              <value>
                true
              </value>
            </localDecl> <localDecl>
              <index>
                2
              </index>
              <mutability>
                Not
              </mutability>
              <internal>
                false
              </internal>
              <ty>
                usize 
              </ty>
              <value>
                2
              </value>
            </localDecl> <localDecl>
              <index>
                3
              </index>
              <mutability>
                Not
              </mutability>
              <internal>
                false
              </internal>
              <ty>
                usize 
              </ty>
              <value>
                2
              </value>
            </localDecl> <localDecl>
              <index>
                4
              </index>
              <mutability>
                Not
              </mutability>
              <internal>
                false
              </internal>
              <ty>
                usize 
              </ty>
              <value>
                4
              </value>
            </localDecl> <localDecl>
              <index>
                5
              </index>
              <mutability>
                Not
              </mutability>
              <internal>
                false
              </internal>
              <ty>
                usize 
              </ty>
              <value>
                2
              </value>
            </localDecl>
          </localDecls>
          <basicBlocks>
            <basicBlock>
              <bbName>
                0
              </bbName>
              <bbBody>
                { _2 = Add ( const 1_usize , const 1_usize ) ;  _3 = Sub ( const 5_usize , const 3_usize ) ;  _4 = Mul ( _2 , _3 ) ;  _5 = Div ( _4 , const 2_usize ) ;  _1 = Eq ( _5 , const 2_usize ) ;  .Statements assert ( _1 , .AssertArgumentList ) -> bb1  ; }
              </bbBody>
            </basicBlock> <basicBlock>
              <bbName>
                1
              </bbName>
              <bbBody>
                { _0 = const ( ) ;  .Statements return ; }
              </bbBody>
            </basicBlock>
          </basicBlocks>
        </function>
      </functions>
    </data>
  </mir>
<generatedCounter>
  0
</generatedCounter>

Expected Results

<generatedCounter>
  0
</generatedCounter>

should be

</generatedTop>
dkcumming commented 1 year ago

Hi, this issue on mir-semantics is the origin of this problem. You can see the discussion between me and @geo2a

radumereuta commented 1 year ago

@dkcumming is this still an issue? I see that the original issue you mention is closed.

dkcumming commented 1 year ago

@radumereuta Yes this is still an issue. The reason the first issue is closed is that it was about the difference between the nix and poetry builds. Which after investigation we realised they were on different versions. Now they are on the same version but we have uncovered the bug in this issue.

radumereuta commented 1 year ago

I think something is wrong with the formatting of the cell. We have some code that generates the format option for the configuration. We need to inspect if that is being done correctly.

radumereuta commented 1 year ago

I'm investigating now and found the root cause of the problem. We have a step which should correct the format attribute for the GeneratedTopCell, but this gets lost because the module transformer doesn't check for attribute differences. This happens when we have a configuration that is not in the main module.

module TEST-SYNTAX
    imports INT-SYNTAX
endmodule
module MIR-CONFIG
  imports TEST-SYNTAX
  configuration
    <k> $PGM:Int </k>
    <returncode exit=""> 4 </returncode> 
endmodule
module TEST
    imports TEST-SYNTAX
    imports MIR-CONFIG
endmodule
radumereuta commented 1 year ago

This is blocked on https://github.com/runtimeverification/k/issues/3530

radumereuta commented 1 year ago

Another thing that needs to be fixed is this line: https://github.com/runtimeverification/k/blob/master/kore/src/main/scala/org/kframework/definition/outer.scala#L535 which needs to include the has for attributes.

ehildenb commented 1 year ago

We should make it so that compilation passes are self-contained. Instead of having a pass that comes through and adjusts th eformat attribute after the fact, it should just be updated at the time the configuration is modified, so that later passes don't have to think about it at all. The definition between each compilation pass should be a valid (or at least self-consistent) one.