KLEE failed to get concrete value for arguments when calling void ObjectState::flushToConcreteStore()

[qichang3]

I run KLEE3.0 on program base64 in coreutils-9.4 and found KLEE cannot get correct concrete value for pointer arguments.

My KLEE version

KLEE 3.0 (https://klee.github.io)
  Build mode: Debug (Asserts: ON)
  Build revision: dfa53ed4f5711ee2d378abb267bff1da8623f7e7

LLVM (http://llvm.org/):
  LLVM version 13.0.1
  Optimized build with assertions.
  Default target: x86_64-unknown-linux-gnu
  Host CPU: goldmont

The command line options used for execution are :

/home/user/coreutils-test/coreutils-9.4-bc# klee --max-solver-time=30 --search=bfs --libc=uclibc --posix-runtime -watchdog -max-time=600 -output-dir=/home/user/coreutils-test/coreutils-9.4-bc/result_all/base64_output --external-calls=all --only-output-states-covering-new --write-cov --write-kqueries base64.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout

I hold back the difinition of String library in uclibc so KLEE will take function in String library as external functions.
When KLEE encounters a call for strcmp(which both arguments are pointer) such as:

  if (argc - optind > 1)
    {
      error (0, 0, _("extra operand %s"), quote (argv[optind + 1]));
      usage (EXIT_FAILURE);
    }

  if (optind < argc)
    infile = argv[optind];
  else
    infile = "-";

  if (STREQ (infile, "-"))
    {
      xset_binary_mode (STDIN_FILENO, O_BINARY);
      input_fh = stdin;
    }
  else
    {
      input_fh = fopen (infile, "rb");
      if (input_fh == nullptr)
        error (EXIT_FAILURE, errno, "%s", quotef (infile));
    }

KLEE will call flushToConcreteStore() for objectStates that pointed by pointer arguments to get concrete value for each symbolic byte in the objectState. Here the two objectStates are:

// calling strcmp(arg00, "-")
-- ObjectState --
        MemoryObject ID: 5430
        Root Object: 0x563d900
        Size: 3
        Bytes:
                [0] concrete? 0 known-sym? 0 unflushed? 0 = (Read w8 0 arg00)
                [1] concrete? 0 known-sym? 0 unflushed? 0 = (Read w8 1 arg00)
                [2] concrete? 1 known-sym? 0 unflushed? 1 = 0
        Updates:
-- ObjectState --
        MemoryObject ID: 658
        Root Object: 0x0
        Size: 2
        Bytes:
                [0] concrete? 1 known-sym? 0 unflushed? 1 = 45
                [1] concrete? 1 known-sym? 0 unflushed? 1 = 0
        Updates:

When executing strcmp, the path constraints of current state is:

array A_data_stat[144] : w32 -> w8 = symbolic
array arg00[3] : w32 -> w8 = symbolic
array n_args[4] : w32 -> w8 = symbolic
array n_args_1[4] : w32 -> w8 = symbolic
array stdin_stat[144] : w32 -> w8 = symbolic
array stdout_stat[144] : w32 -> w8 = symbolic
(query [(Ult N0:(ReadLSB w32 0 n_args)
              2)
         (Eq false (Slt 0 N0))
         (Ult N1:(ReadLSB w32 0 n_args_1)
              3)
         (Slt 0 N1)
         (Eq false (Slt 1 N1))
         (Eq false
             (Eq 0
                 (And w64 (ReadLSB w64 8 A_data_stat)
                          2147483647)))
         (Eq 0
             (And w64 (ReadLSB w64 56 A_data_stat)
                      18446744073709486080))
         (Eq false
             (Eq 0
                 (And w64 (ReadLSB w64 8 stdin_stat)
                          2147483647)))
         (Eq 0
             (And w64 (ReadLSB w64 56 stdin_stat)
                      18446744073709486080))
         (Eq false
             (Eq 0
                 (And w64 (ReadLSB w64 8 stdout_stat)
                          2147483647)))
         (Eq 0
             (And w64 (ReadLSB w64 56 stdout_stat)
                      18446744073709486080))
         (Eq 45 (Read w8 0 arg00))
         (Eq 0 (Read w8 1 arg00))]
        false)

According to the path constraints, arg00 has been set to "-", which first byte is 45 and second byte is 0. The result of strcmp(arg00,"-") is expected to be 0. However, the acutal result of strcmp(arg00, "-") is not 0 but -45.

I investigated the reason and found:
According to the semantic of flushToConcreteStore() , KLEE will only try to get a concrete value for bytes that are knownSymbolic and store the concrete value into concreteStore.

void ObjectState::flushToConcreteStore(TimingSolver *solver,
                                       const ExecutionState &state) const {
  for (unsigned i = 0; i < size; i++) {
    if (isByteKnownSymbolic(i)) {
      ref<ConstantExpr> ce;
      bool success = solver->getValue(state.constraints, read8(i), ce,
                                      state.queryMetaData);
      if (!success)
        klee_warning("Solver timed out when getting a value for external call, "
                     "byte %p+%u will have random value",
                     (void *)object->address, i);
      else
        ce->toMemory(concreteStore + i);
    }
  }
}

However, the source code of ObjectState constructor show that for these ObjectState created with an array(like arg00)，KLEE will not set the bytes to knownSymbolic(as you can see in the objectState). So when calling flushToConcrete() for these objectStates, nothing happens.

By setting all bytes to knownSymbolic and set each knownSymbolic[offset] to corresponding ReadExpr to array when KLEE creates objectState with array, the above problem will not happen again.

// log printed when flushToConcreteStore
flush (Read w8 0 arg00) to 45
flush (Read w8 1 arg00) to 0

// after flush, symbolic bytes is still symbolic
-- ObjectState --
        MemoryObject ID: 5425
        Root Object: 0x5cdd810
        Size: 3
        Bytes:
                [0] concrete? 0 known-sym? 1 unflushed? 0 = (Read w8 0 arg00)
                [1] concrete? 0 known-sym? 1 unflushed? 0 = (Read w8 1 arg00)
                [2] concrete? 1 known-sym? 0 unflushed? 1 = 0
        Updates:
-- ObjectState --
        MemoryObject ID: 657
        Root Object: 0x0
        Size: 2
        Bytes:
                [0] concrete? 1 known-sym? 0 unflushed? 1 = 45
                [1] concrete? 1 known-sym? 0 unflushed? 1 = 0
        Updates:

// execution result
result is: 0

I do not know the reason for original implementation of the ObjectState constructor but it seems that it makes flushToConcrete() not work when encountering similar situation. I want to know whether it is a bug or there are other reasons for designing ObjectState constructor like this?

Looking forward to your kind reply!

[ccadar]

@qichang3 thanks for the report.

I think this has likely been fixed in the recently released KLEE 3.1, most exactly via #1407. Can you try the latest version and confirm?