kore-exec: Function in configuration is not evaluated

[ttuegel]

Using kore-exec for symbolic execution (not using --prove), a function with partial arguments is not evaluated. The backend should infer that the arguments are defined because they appear in the configuration.

To reproduce:

# Unpack attached files, then:
kore-exec definition.kore --module C --pattern uninitialized-0072.kore --output result.kore --depth 0
# result.kore will be the same as uninitialized-0072.kore,
# indicating that the function at the top of the <k> cell was not evaluated.

Files: uninitialized.tar.gz

[ana-pantilie]

In

haskell-backend/kore/src/Kore/Rewrite.hs

Line 200 in 9ea642d

configs <- lift $ Pattern.simplifyTopConfiguration config

we should use simplify...Defined. We need to see if anything breaks.

[ana-pantilie]

This change doesn't significantly alter performance. The numbers are the following:

New Ceil: #3209

Master vs Master with modif

anapantilie@Anas-MBP: ~/RV/haskell-backend/test/regression-c fix-exec-definedness!
$ env GHCRTS='-s' make test-smoke100.sh.out                                                                                                                              [18:31:27]
>>> /Users/anapantilie/RV/haskell-backend/test/regression-c test-smoke100.sh
rm -f test-smoke100.sh.out
./test-smoke100.sh > test-smoke100.sh.out || true
kore-exec: [332516832] Warning (WarnIfLowProductivity):
    Productivity dropped to: 89%
    Relevant K files include:
        /home/dwightguth/c-semantics/semantics/c.k
    Poor productivity may indicate a performance bug.
    Please file a bug report: https://github.com/runtimeverification/haskell-backend/issues
 556,204,124,112 bytes allocated in the heap
  11,882,859,224 bytes copied during GC
   1,072,200,800 bytes maximum residency (9 sample(s))
     131,107,760 bytes maximum slop
            3368 MiB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1188 colls,  1188 par   31.933s   3.247s     0.0027s    0.1516s
  Gen  1         9 colls,     8 par    6.844s   2.542s     0.2824s    1.0913s

  Parallel GC work balance: 31.02% (serial 0%, perfect 100%)

  TASKS: 34 (1 bound, 33 peak workers (33 total), using -N16)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.003s  (  0.109s elapsed)
  MUT     time  304.259s  (326.761s elapsed)
  GC      time   38.777s  (  5.789s elapsed)
  EXIT    time    0.000s  (  0.003s elapsed)
  Total   time  343.039s  (332.662s elapsed)

  Alloc rate    1,828,058,449 bytes per MUT second

  Productivity  88.7% of total user, 98.2% of total elapsed

diff -u test-smoke100.sh.out.golden test-smoke100.sh.out || ( mv test-smoke100.sh.out test-smoke100.sh.out.fail && false )





anapantilie@Anas-MBP: ~/RV/haskell-backend/test/regression-c fix-exec-definedness!
$ env GHCRTS='-s' make test-smoke100.sh.out                                                                                                                              [18:40:00]
>>> /Users/anapantilie/RV/haskell-backend/test/regression-c test-smoke100.sh
rm -f test-smoke100.sh.out
./test-smoke100.sh > test-smoke100.sh.out || true
kore-exec: [343732199] Warning (WarnIfLowProductivity):
    Productivity dropped to: 89%
    Relevant K files include:
        /home/dwightguth/c-semantics/semantics/c.k
    Poor productivity may indicate a performance bug.
    Please file a bug report: https://github.com/runtimeverification/haskell-backend/issues
 560,412,101,088 bytes allocated in the heap
  12,955,388,768 bytes copied during GC
   1,072,203,936 bytes maximum residency (9 sample(s))
     131,117,200 bytes maximum slop
            3368 MiB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1196 colls,  1196 par   35.608s   3.305s     0.0028s    0.1627s
  Gen  1         9 colls,     8 par    6.598s   2.467s     0.2741s    1.1520s

  Parallel GC work balance: 28.01% (serial 0%, perfect 100%)

  TASKS: 34 (1 bound, 33 peak workers (33 total), using -N16)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.002s  (  0.108s elapsed)
  MUT     time  311.238s  (337.971s elapsed)
  GC      time   42.206s  (  5.772s elapsed)
  EXIT    time    0.000s  (  0.008s elapsed)
  Total   time  353.447s  (343.859s elapsed)

  Alloc rate    1,800,589,960 bytes per MUT second

  Productivity  88.1% of total user, 98.3% of total elapsed

diff -u test-smoke100.sh.out.golden test-smoke100.sh.out || ( mv test-smoke100.sh.out test-smoke100.sh.out.fail && false )
 
anapantilie@Anas-MBP: ~/RV/haskell-backend/test/regression-c fix-exec-definedness!

New Ceil vs New Ceil with modif

anapantilie@Anas-MBP: ~/RV/haskell-backend/test/regression-c fix-ceil-performance!
$ env GHCRTS='-s' make test-smoke100.sh.out                                                                                                                              [18:58:15]
>>> /Users/anapantilie/RV/haskell-backend/test/regression-c test-smoke100.sh
rm -f test-smoke100.sh.out
./test-smoke100.sh > test-smoke100.sh.out || true
kore-exec: [302167272] Warning (WarnIfLowProductivity):
    Productivity dropped to: 84%
    Relevant K files include:
        /home/dwightguth/c-semantics/semantics/c.k
    Poor productivity may indicate a performance bug.
    Please file a bug report: https://github.com/runtimeverification/haskell-backend/issues
 501,550,433,992 bytes allocated in the heap
  13,085,926,064 bytes copied during GC
   1,072,203,984 bytes maximum residency (9 sample(s))
     131,113,056 bytes maximum slop
            3367 MiB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1071 colls,  1071 par   44.044s   3.145s     0.0029s    0.1605s
  Gen  1         9 colls,     8 par    6.276s   2.066s     0.2296s    1.2028s

  Parallel GC work balance: 29.11% (serial 0%, perfect 100%)

  TASKS: 34 (1 bound, 33 peak workers (33 total), using -N16)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.002s  (  0.095s elapsed)
  MUT     time  261.758s  (296.965s elapsed)
  GC      time   50.320s  (  5.212s elapsed)
  EXIT    time    0.000s  (  0.010s elapsed)
  Total   time  312.081s  (302.281s elapsed)

  Alloc rate    1,916,084,210 bytes per MUT second

  Productivity  83.9% of total user, 98.2% of total elapsed

diff -u test-smoke100.sh.out.golden test-smoke100.sh.out || ( mv test-smoke100.sh.out test-smoke100.sh.out.fail && false )

anapantilie@Anas-MBP: ~/RV/haskell-backend/test/regression-c fix-ceil-performance!
$ env GHCRTS='-s' make test-smoke100.sh.out                                                                                                                              [19:06:20]
>>> /Users/anapantilie/RV/haskell-backend/test/regression-c test-smoke100.sh
rm -f test-smoke100.sh.out
./test-smoke100.sh > test-smoke100.sh.out || true
kore-exec: [307732536] Warning (WarnIfLowProductivity):
    Productivity dropped to: 89%
    Relevant K files include:
        /home/dwightguth/c-semantics/semantics/c.k
    Poor productivity may indicate a performance bug.
    Please file a bug report: https://github.com/runtimeverification/haskell-backend/issues
 510,066,481,936 bytes allocated in the heap
  11,427,908,080 bytes copied during GC
   1,072,203,936 bytes maximum residency (9 sample(s))
     131,113,104 bytes maximum slop
            3368 MiB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      1089 colls,  1089 par   31.145s   3.360s     0.0031s    0.2212s
  Gen  1         9 colls,     8 par    6.312s   2.360s     0.2623s    1.1178s

  Parallel GC work balance: 27.15% (serial 0%, perfect 100%)

  TASKS: 34 (1 bound, 33 peak workers (33 total), using -N16)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.003s  (  0.145s elapsed)
  MUT     time  279.584s  (302.021s elapsed)
  GC      time   37.457s  (  5.721s elapsed)
  EXIT    time    0.000s  (  0.006s elapsed)
  Total   time  317.044s  (307.892s elapsed)

  Alloc rate    1,824,378,793 bytes per MUT second

  Productivity  88.2% of total user, 98.1% of total elapsed

diff -u test-smoke100.sh.out.golden test-smoke100.sh.out || ( mv test-smoke100.sh.out test-smoke100.sh.out.fail && false )