Avoid tab-space mix in compiler output

[cameel]

After #15026 there remain two sources of random tabs in the sources we store in the repo:

• SMTChecker includes indentation in its source locations so it's also included in code snippets.
• Jump labels in --asm output are prepended with a tab.

I think either of those is unnecessary and removing them would make automatic style checks simpler (less files to exclude). Not only for us but for anyone storing this output in their repository.

Still, this is more of an annoyance than a real issue so I don't expect that we'll work on it any time soon. I'm submitting an issue more to document what I discovered while addressing #15026 than to get someone to actually work on it.

Tabs in SMTChecker output

This happens only if the input file is indented

test.sol

// SPDX-License-Identifier: GPL-3.0
pragma solidity *;

contract C {
    function f() public {
		assert    ( false )    ;    
    }
}

Note that the assert line has leading and trailing tabs.

solc test.sol --model-checker-engine all

Warning: Function state mutability can be restricted to pure
 --> test.sol:5:5:
  |
5 |     function f() public {
  |     ^ (Relevant source part starts here and spans across multiple lines).

Warning: CHC: Assertion violation happens here.
Counterexample:


Transaction trace:
C.constructor()
C.f()
 --> test.sol:6:3:
  |
6 | 		assert    ( false )    ;    
  | 		^^^^^^^^^^^^^^^^^^^

Note that the assert line is included as is, including the leading and trailing indentation. The ^^^^^ marker repeats that indentation too.

Tab as separator in jump labels

solc test.sol --asm

    tag_3:
      tag_4
      tag_5
      jump	// in
    tag_4:
      stop
    tag_5:
        /* "test.sol":109:114  false */
      0x00
        /* "test.sol":97:116  assert    ( false ) */
      tag_7
      jumpi
      tag_8
      tag_9
      jump	// in

Note that jump // in includes a tab character as a separator. It seems to be a deliberate decision made in #1330:

solidity/libevmasm/AssemblyItem.cpp

Lines 331 to 338 in b61c2a9

	if (m_jumpType == JumpType::IntoFunction || m_jumpType == JumpType::OutOfFunction)
	{
	text += "\t//";
	if (m_jumpType == JumpType::IntoFunction)
	text += " in";
	else
	text += " out";
	}

The PR does not have any justification for that decision though and it seems to me that using a space there would work just as well.

[cocohearts]

@cameel is this a good first issue? I'd like to work on this, since it seems sufficiently self-contained