[CN] Figure out how to propagate location information via generated binders

In the below example, there's a type error (the expected CN basetype of the left operand sizeof(..) does not match its inferred one for some reason) but the location information is not localised to the left, instead pointing to the whole expression.

16:58 ➜  cerberus git:(master) cat illtyped_multiply.error.c && cn -d2 --no-inherit-loc illtyped_multiply.error.c 2>tmp.out
#include<inttypes.h>
#include<limits.h>
#include<stddef.h>
size_t f(int x) {
    return sizeof(uintptr_t) * CHAR_BIT;
}
[1/1]: f
16:58 ➜  cerberus git:(master) cat /tmp/3__mucore.mucore
-- Aggregates
def struct a_488 :=todo: implement struct type printer

def struct a_520 :=todo: implement struct type printer

-- Fun map

proc f = (x : i32) -> (=

  return label ret_543

  body =
    {--} let strong _: unit =
      {--} let strong &x: pointer = {--} create({--} align_of({--} ''signed int''), signed int) in
      {--} let strong _: unit = {--} store(signed int, {--} &x, {--} x NA) in
      {--} let strong _: unit =
        {-#stmt#-}{-<line:4:16, line:6:1>-} let strong _: unit =
          {-#stmt#-}{-<col:4 - 50>-} let strong a_549: loaded integer =
            {--} bound({-#expr#-}{-#type size_t#-}{-<col:11 - 49> col:29-} let weak (a_544: loaded integer, a_545: loaded integer) = {--} unseq({-#expr#-}{-#type size_t#-}{-<line:5:11 - 28> col:11-} pure({--} size_of({--} ''uintptr_t'')), {-#expr#-}{-#type signed int#-}{-<col:31 - 49>-} pure({--} 8)) in
              {--} pure({--} bound_op(wrap<size_t>, '*', {--} conv_int({--} ''unsigned int'', {--} a_544), {--} conv_int({--} ''unsigned int'', {--} a_545)))) in
          {--} let strong _: unit = {--} kill(signed int, {--} &x) in
          {--} run ret_543({--} conv_loaded_int({--} ''size_t'', {--} a_549)) in
        {--} pure({--} Unit) in
      {--} let strong _: unit = {--} kill(signed int, {--} &x) in
      {--} pure({--} Unit) in
    {-#TODO(label)#-}{-<tests/cn/illtyped_multiply.error.c:4:0, line:6:1> col:7 - line:4:8-} run ret_543({--} undef(<<UB088_reached_end_of_function>>)))

The CN code responsible for this is this https://github.com/rems-project/cerberus/blob/5fa5cf0f8d68d740b1994f111256b6d915a21835/backend/cn/check.ml#L648-L660

Even changing loc to loc_of_pexpr pe1 (and loc_of_pexpr pe2) is not helpful, because the a_544 in the core does not have location annotations, but inherits it from the nearest ancestor expression (or statement). In principle, it should be possible to flow the information through binders, but a good way of implementing this is not clear:

Option 1: do this in core_to_mucore.ml. This is where the location inheritance takes place, and perhaps a more sophisticated translation could propagate more location information (some might be lost in partial evaluation).
Option 2: do this in check.ml. The typing context maintains an environment of mappings from variables to indexTerms, and the indexTerms have location information, so this could work here.

rems-project / cerberus

[CN] Figure out how to propagate location information via generated binders #270