[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[RFC] Indexing array values with offsets, and constructing arrays by siz

From: Jose E. Marchesi
Subject: [RFC] Indexing array values with offsets, and constructing arrays by size
Date: Wed, 17 Feb 2021 19:12:35 +0100
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (gnu/linux)

In the recent work with btf.pk that David Faust did, we have something
like this:

type BTF_Section =
    string[header.str_len] strings @ str_off;

    /* Given an offset into the BTF strings section, return the string.  */
    method get_string = (offset<uint<32>,B> off) string:
        return string @ strings'offset + off;

i.e. the string table in the BTF section can be comfortably expressed as
an array of strings.

But then, in the BTF world strings are referred using an offset relative
to the string table, and not the ordinal order of the string in the
table.  This is similar to other string tables in other formats like

The method above works, but it has a problem: it is not what I call
"agnostic" Poke code.  This means that the code needs assumes the data
is mapped.  In this case, the method only works when invoked in a BTF
section that is mapped.

Most Poke code should be agnostic if needed, so I am proposing two
additions to the language:

1) Indexing array values with offsets.

   We shall support indexing arrays, both mapped and non-mapped, with an
   offset value.  Like in:

   var a = [1,2,3];

   a[0#B] -> 1
   a[4#B] -> 2
   a[8#B] -> 3

   The provided offset should match the offset of some particular
   element in the array.  Otherwise, we get an E_out_of_bounds

   a[5#B] -> raises E_out_of_bounds
   a[10#Kb] -> raises E_out_of_bounds

   Using this support, we don't need the `get_string' method above.
   Given an offset into the string table the user can just do:


   which would be agnostic Poke code: it would work as well with both
   mapped and non-mapped BTF sections.

2) Constructing arrays by size.

   Currently we can create array values in Poke using three different

   - Using an array literal: [1,2,3], ["foo", "bar"], etc.
   - Using an array constructor:

      int[] (3)  -> [0,0,0] of type int[]
      int[3] (3) -> [0,0,0] of type int[3]
      string (2) -> ["",""]

   - Mapping an array:

     + Unbounded: int[] @ OFFSET -> maps until EOF or constraint failure.
     + Bounded by number of elements: int[3] @ OFFSET -> [1,2,3]
     + Bounded by size: int[12#B] @ OFFSET -> [1,2,3]

   I am proposing to add the possibility of constructing an array by
   size as well, like in:

      int[] (12#B) -> [0,0,0]
      int[] (0#B) -> []

   The question with this is: what exception to raise when the given
   size doesn't span for a whole number of the elements of the array
   type?  Currently, that situation when mapping arrays by size raises
   E_map_bounds.  I think in the case of constructing by size we should
   raise E_out_of_bounds instead.

What do you people think about these proposals?

reply via email to

[Prev in Thread] Current Thread [Next in Thread]