Removing run time checks

Google Group
21

G1ofg0 is overloaded.

In this case, it resolves to

castfn g1ofg0_int: int → [i:int] int(i)

which casts an un-index int to an indexed one.

Obviously, only static casting is involved here.On Wednesday, October 28, 2015 at 12:03:30 AM UTC-4, Mike Jones wrote:

I do program in Haskell, but my current application has to be inspectable
by C programmers, so on first go I don’t want to scare them off.

That said, what does the g1ofg0 do? Some searching seems to say it
introduces an index, but it is unclear what value it adds to the
conditional logic.

22

I forgot to mention one very important issue.

There are really two kinds of casts in ATS: static cast and dynamic cast

For instance, casting uint8 to int_u8 is a static cast in the sense that
there
is no actual clamping; casting int_u8 to uint8 is also a static cast but
the C
compiler may not know it (so it would still generate code like (x & 0xFF)).

In order to fully take advantage of the type information provided by ATS,
one
probably has to write one’s own C compiler.On Monday, October 26, 2015 at 9:29:31 AM UTC-4, gmhwxi wrote:

For every n, int(n) and int have the same representation.

$UN.cast{uint8}(x) is translated to ((uint8)(x)) in C, which I think is
just a form of clamping.

Types like int8 and uint8 are mostly used to classify components of a
struct or array. For classifying
variables, please use int_i8 and int_u8:

typedef int_i8 = intBtw(~128, 127) and int_u8 = intBtw(0, 255)

Using int_i8 and int_u8 can also let you discover potential overflows.

I don’t know much about MISRA, but I am pretty certain that you can do a
lot better with types like int_i8 and int_u8 :slight_smile:

Cheers!

On Mon, Oct 26, 2015 at 12:13 AM, Mike Jones <…> wrote:

Keeping more to the original, applying your lesson, the code below.

Now a question about representation in memory. I assume that
cast(n) reduces the memory used from int to uint8_t with a memory
copy. Therefore, the older code would run slower. The new code would use
int in all places except pec_add(), and should run faster. I assume this
based on the idea that the constraint, say: n0 <= 127 would not affect the
representation size.

If I am correct, then in general this pattern of nested constraints
should be safer (less casts) and run faster (less conversions).

Is this correct?

Also, related to types, the MISRA spec (
http://caxapa.ru/thumbs/468328/misra-c-2004.pdf) has a whole section on
promotions, casting and similar problems. In general, does ATS eliminate
these problems, or does one still have to be concerned?

My intuition is that most ATS code is of type int with constraints, or
mapped to a more specific type, but must then be converted with cast. If
cast is well enough behaved, perhaps the typical MISRA problems are
eliminated, due to the fact that what you see is what you get?

If this is the case, has anyone looked at MISRA or ISO26262 wrt ATS and
is there a considered opinion whether ATS could be an alternative to these
standards?

fun read_frame(): bool = let
val () = !packetInCount := serial_poll_for_byte()
fun read {n0: nat | n0 <= 127} (count: int(n0)): bool =
if count >= 3
then let
fun loop {n: nat | n0 - 2 >= n} .. (cnt: int(n), cksum:
uint8): uint8 =
if cnt > 0
then let
val byte = serial_poll_for_byte()
val () = packetIn[count - cnt - 1] := byte
in loop (cnt - 1, pec_add(cksum, byte)) end
else cksum
val cksum = loop (count - 2, pec_add(ZERO, u8(count)))
val packetInChecksum = serial_poll_for_byte()
val () = packetIn[count - 1] := packetInChecksum
in cksum = packetInChecksum end
else false
in
read(n7(!packetInCount))
end

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/dfb4f081-2442-45c5-8a9c-4e06c68647ee%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/dfb4f081-2442-45c5-8a9c-4e06c68647ee%40googlegroups.com?utm_medium=email&utm_source=footer
.

23

typedef g1uintBtwe2
(tk:tk, lb0:int, ub0:int, lb1:int, ub1:int) = [i: int | lb0 <= i; i <= ub0 ; lb1 <= i; i <= ub1] g1uint (tk, i)

Should be

typedef g1uintBtwe2
(tk:tk, lb0:int, ub0:int, lb1:int, ub1:int) = [i: int | (lb0 <= i && i <= ub0) || (lb1 <= i && i <= ub1)] g1uint (tk, i)On Tuesday, October 27, 2015 at 7:21:25 PM UTC-4, Mike Jones wrote:

So to solve I tried to change the constraint to be between numbers. Then
add a conversion function to clamp the data.

However, the constraint on the return value of n73 causes compile
problems. It does not like ‘then 3’, nor ‘else’ x.

I figured that because this takes an int input and returns an int, the
code just has to satisfy the constraint, and simple conditionals would be
solvable. I assume it will treat the 3 or 127 as ints as that is what is
expected to be returned. As far as returning x, it would just have to
figure out that if the extremes are clamped, what is left must be ok.

Eventually I need to pass uint8 into n73 as it comes from the array
reference, but that caused even more constraint failures.

extern fun{} n73 {n: nat | n >= 3 && n <= 127} (x: int): int(n)
implement{} n73 (x) = if x < 3
then 3
else if x > 127
then 127
else x

fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void = let

Another case that does work:

typedef g1uintBtwe2
(tk:tk, lb0:int, ub0:int, lb1:int, ub1:int) = [i: int | lb0 <= i; i <= ub0; lb1 <= i; i <= ub1] g1uint (tk, i)
typedef uintBtwe2 (lb0:int, ub0:int, lb1:int, ub1:int) = g1uintBtwe2
(uint_kind, lb0, ub0, lb1, ub1)

typedef hex_t = uintBtwe2(0x30, 0x39, 0x41, 0x46)

fun uint82hex (i: uint8) : hex_t = let
val nv = if ((i >= u8(0x30) && i <= u8(0x39)) || (i >= u8(0x41) && i <=
u8(0x46))) then i else u8(0x30)
in
cast{hex_t}(nv)
end

defines a type and uses a case. But because I am calling set_n with a
constraint that has a loop with an extended constraint, I can’t use a
typedef. Is there some way to cast in n73 like cast{n: nat | n >= 3 && n
<= 127}(3) that solves the problem? This would seem like cheating. Your
sort of certifying that the values are within the constraints rather than
let the solver prove it.

24

For every n, int(n) and int have the same representation.

$UN.cast{uint8}(x) is translated to ((uint8)(x)) in C, which I think is
just a form of clamping.

Types like int8 and uint8 are mostly used to classify components of a
struct or array. For classifying
variables, please use int_i8 and int_u8:

typedef int_i8 = intBtw(~128, 127) and int_u8 = intBtw(0, 255)

Using int_i8 and int_u8 can also let you discover potential overflows.

I don’t know much about MISRA, but I am pretty certain that you can do a
lot better with types like int_i8 and int_u8 :slight_smile:

Cheers!On Mon, Oct 26, 2015 at 12:13 AM, Mike Jones proc...@gmail.com wrote:

Keeping more to the original, applying your lesson, the code below.

Now a question about representation in memory. I assume that
cast(n) reduces the memory used from int to uint8_t with a memory
copy. Therefore, the older code would run slower. The new code would use
int in all places except pec_add(), and should run faster. I assume this
based on the idea that the constraint, say: n0 <= 127 would not affect the
representation size.

If I am correct, then in general this pattern of nested constraints should
be safer (less casts) and run faster (less conversions).

Is this correct?

Also, related to types, the MISRA spec (
http://caxapa.ru/thumbs/468328/misra-c-2004.pdf) has a whole section on
promotions, casting and similar problems. In general, does ATS eliminate
these problems, or does one still have to be concerned?

My intuition is that most ATS code is of type int with constraints, or
mapped to a more specific type, but must then be converted with cast. If
cast is well enough behaved, perhaps the typical MISRA problems are
eliminated, due to the fact that what you see is what you get?

If this is the case, has anyone looked at MISRA or ISO26262 wrt ATS and is
there a considered opinion whether ATS could be an alternative to these
standards?

fun read_frame(): bool = let
val () = !packetInCount := serial_poll_for_byte()
fun read {n0: nat | n0 <= 127} (count: int(n0)): bool =
if count >= 3
then let
fun loop {n: nat | n0 - 2 >= n} .. (cnt: int(n), cksum:
uint8): uint8 =
if cnt > 0
then let
val byte = serial_poll_for_byte()
val () = packetIn[count - cnt - 1] := byte
in loop (cnt - 1, pec_add(cksum, byte)) end
else cksum
val cksum = loop (count - 2, pec_add(ZERO, u8(count)))
val packetInChecksum = serial_poll_for_byte()
val () = packetIn[count - 1] := packetInChecksum
in cksum = packetInChecksum end
else false
in
read(n7(!packetInCount))
end

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/dfb4f081-2442-45c5-8a9c-4e06c68647ee%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/dfb4f081-2442-45c5-8a9c-4e06c68647ee%40googlegroups.com?utm_medium=email&utm_source=footer
.