Removing run time checks

[Mike Jones]

Now that my application works, I'm trying to remove some dynamic checks to static checks and so I'm looking for a way to do it. The goal is faster code, and prevention of code errors in maintenance if some new person plays with it.

The code basically accepts a 127 byte frame, where the first byte is size, and the last byte is a CRC. For now, ignore that the first byte can be bigger than 127, as a 1 in the left most bit has a special meaning we can ignore for discussion.

The code below reads one frame from the USB. There are three functions that effectively ensure the values are nats within the size, so that the constraints in the code are satisfied.

The problem is these can't prevent a bug. If I call loop with a value too big, it will just clamp it and run. That will prevent a memory problem, but not an error.

The question boils down to something like how to get the compiler to see something like:

n7m2(!packetInCount - TWO)

and know that because it is TWO smaller, it satisfies the constraint of the array.

Is there a way to define constraints in such a way it can make this check?

macdef packetIn =

  $extval(arrayref(uint8, 127),"packetIn")

macdef packetInCount =

  $extval(ref(uint8),"packetInCount")

macdef packetInHeader =

  $extval(ref(uint8),"packetInHeader")

extern fun{} n7 (x: uint8): natLte(127)

implement{} n7 (x)  = cast{natLte(127)}(x land u8(0x7F))

extern fun{} n7m1 (x: uint8): natLte(126)

implement{} n7m1 (x)  = if x > u8(126) then cast{natLte(126)}(126) else cast{natLte(126)}(x)

extern fun{} n7m2 (x: uint8): natLte(125)

implement{} n7m2 (x)  = if x > u8(125) then cast{natLte(125)}(125) else cast{natLte(125)}(x)

  fun read_frame(): bool = let

    val () = !packetInCount := serial_poll_for_byte() // Discarded the multi-frame bit

    val ok = if !packetInCount >= THREE // Three is the minimum packet size other than zero.

             then let

              fun loop  {n: nat | n <= 125} .<n>. (cnt: int(n), cksum: uint8): uint8 =

                if cnt > 0

                  then let 

                    val byte = serial_poll_for_byte()

                    val () = packetIn[n7m2(!packetInCount - u8(cnt) - ONE)] := byte

                    in loop (cnt - 1, pec_add(cksum, byte)) end

                  else cksum

              val cksum = loop (n7m2(!packetInCount - TWO), pec_add(ZERO, !packetInCount))

              val packetInChecksum = serial_poll_for_byte()

              val () = packetIn[n7m1(!packetInCount - ONE)] := packetInChecksum

              in cksum = packetInChecksum end

             else false

  in 

    ok 

  end

[gmhwxi]

Given my understanding of your code, here is what I suggest:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test23.dats

[Mike jones]

So, fundamentally I must pass the root number (count) to a function with a constraint, so that a second function (loop) inside it can refer to its static value in a second constraint.

Very helpful. I can use this for several other similar problems reading and creating frames.

Would the <n> still work? Is it not necessary for some reason?

[Hongwei Xi]

>>Would the <n> still work? Is it not necessary for some reason?

Yes, it works. It is just that I don't find termination-checking to be really

valuable in practice. On the other hand, if someone can relate termination-checking

to certain timing constraints, it will be truly fantastic!

--
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/C711F7E3-0BC5-4768-AC0E-7A44C77333C3%40gmail.com.

[Mike Jones]

Yes, if a max time were given and the compiler rejected a time violation, that would be fantastic. But that is a hard problem. I would be happy just to eliminate bugs and only have errors.

[Mike Jones]

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

Now a question about representation in memory. I assume that cast<uint8>(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} .<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

[Hongwei Xi]

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 :)

Cheers!

--
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.

[gmhwxi]

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 :)

Cheers!

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

Visit this group at http://groups.google.com/group/ats-lang-users.

[Mike Jones]

I think the MISRA approach is to add constraints to the C code, with tools to enforce them. All violations must be fixed or documented. Practically, this means embedded code has some amount of documentation.

The difficulty for ATS is that if a MISRA tool is run on the generated C code, it may not be easy to translate it back to ATS to fix, etc. I suppose a set of constraints on ATS could generate MISRA compliant code, but that is a lot of effort, and probably an entirely new research project.

that said, if there were an ATS compiler and prelude that prevented most violations except those that are unavoidable, like interrupt handling code, and if it were proven to be such, it would offer an alternative to direct MISRA C programming.

Whether the market would accept this or not I do not know. This is just my pondering the possible.

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.

[gmhwxi]

On Monday, October 26, 2015 at 1:02:51 PM UTC-4, Mike Jones wrote:

I think the MISRA approach is to add constraints to the C code, with tools to enforce them. All violations must be fixed or documented. Practically, this means embedded code has some amount of documentation.

The difficulty for ATS is that if a MISRA tool is run on the generated C code, it may not be easy to translate it back to ATS to fix, etc. I suppose a set of constraints on ATS could generate MISRA compliant code, but that is a lot of effort, and probably an entirely new research project.

Personally I do not feel this is too hard or requires too much effort. It is more like a commercial project than a research project, and a MISRA expert is needed for such a
project.
 

that said, if there were an ATS compiler and prelude that prevented most violations except those that are unavoidable, like interrupt handling code, and if it were proven to be such, it would offer an alternative to direct MISRA C programming.

Whether the market would accept this or not I do not know. This is just my pondering the possible.

I would not recommend this approach. At least not for now.

[Mike Jones]

I applied the technique to another case, and can't figure out why I get a constraint error on the last line. The code below removes unnecessary code as an attempt to satisfy the compiler. The error includes:

15912(line=546, offs=34) -- 15912(line=546, offs=34): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>=); S2EVar(2129->S2Eapp(S2Ecst(sub_int_int); S2Evar(n0(5697)), S2Eintinf(1))), S2Eintinf(0)))

I assume it can't figure out count -1 on the last line satisfies n0 - 1 > n.

But this is basically the same form as my last code.

Any insight on what is wrong?

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

    fun loop {n: nat | n0 - 1 >= n} .<n>. (cnt: int(n), p: uint8): uint8 =

      if cnt > 0 

      then loop(cnt - 1, pec_add(ZERO, p))

      else p

  in packetOut[count - 1] := loop(count - 1, ZERO) end

[Hongwei Xi]

The error message says that count-1 (in loop(count-1, ZERO)) cannot

be proven to be nonnegative. This is clearly true. Imagine you call set_n(0).

--
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/946c92b4-5ca5-4f36-aaaa-f58b10fa8d8f%40googlegroups.com.

[Mike Jones]

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.

[Mike Jones]

Looking through old posts, perhaps I really need:

extern fun{} n73 (x: uint8): [n: int | n >= 3 && n <= 127] int(n)

This compiles better but it barfs with:

‘g0int2uint’ undeclared

So I added:

staload "prelude/SATS/integer.sats"

Which gives lots of errors, as it breaks previously working code, mainly uint8 code, things like:

val ok = u8(0)
val OK = u8(1)
val b = if ok <> OK ...

Is there some basic incompatibility of integer_fixed and integer?

[gmhwxi]


There is a misuse of quantifier here:

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

What you need is

extern fun{} n73(x: int): [n:int | 3 <= n; n <= 127] int(n)

or you can write

extern fun{} n73(x: int): intBtwe(3, 127).

[gmhwxi]

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)

[gmhwxi]

Not sure about what happened.

The following line should really be like a no-op as 'integer.sats'
has already been loaded be default:

staload "prelude/SATS/integer.sats"

[gmhwxi]

ATS has rich syntatic support.

If you program in Haskell, you would likely prefer
the following higher-order style of coding:

typedef
intsub(p:int->bool) = [i:int | p(i)] int(i)

stadef
intBtwe(i:int, j:int) =
  lam (a:int): bool => (i <= a && a <= j)
typedef
intBtwe(i:int, j:int) = intsub(intBtwe(i, j))
typedef
intBtwe2(i1:int, j1:int, i2:int, j2:int) =
  intsub(lam(a) => intBtwe(i1, j1)(a) || intBtwe(i2, j2)(a))

typedef hex = intBtwe2(0x30, 0x39, 0x41, 0x46)

fun
int2hex
  (i:int): hex = let
  val i = g1ofg0(i)
  val _0_ = 0x30 and _9_ = 0x39
  val _a_ = 0x41 and _f_ = 0x46
in
  if i < _a_
    then _0_
    else (
      if i > _9_
    then (if i < _a_ then _0_ else (if i > _f_ then _0_ else i)) else i
      // end of [if]
    ) (* else *)
end // end of [int2hex]

[Mike Jones]

So a bit about the integer.sats problem

Starting with what compiles:

#include "config.hats"

#include "{$TOP}/avr_prelude/kernel_staload.hats"

staload "prelude/SATS/bool.sats"

staload CH = "prelude/SATS/char.sats"

staload "prelude/SATS/unsafe.sats"

extern fun{} n73 (x: uint8): [n: int | n >= 3; n <= 127] int(n)

implement{} n73 (x)  =    if x < 3

                          then  3

                          else  if x > 127

                                then 127

                                else cast{intBtwe(3,127)}(x)

Now, as soon as I add to main:

val v = n73(FOUR)

I get these errors:

In file included from DATS/main_dats.c:15:0:

DATS/main_dats.c: In function ‘ATSLIB_056_prelude__lt_g0uint_int__211__1’:

DATS/main_dats.c:18821:23: error: ‘PMVtmpltcstmat’ undeclared (first use in this function)

 ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

                       ^

/opt/ATS/ATS2-Postiats-0.2.3/ccomp/runtime/pats_ccomp_instrset.h:266:37: note: in definition of macro ‘ATSINSmove’

 #define ATSINSmove(tmp, val) (tmp = val)

                                     ^

DATS/main_dats.c:18821:23: note: each undeclared identifier is reported only once for each function it appears in

 ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

                       ^

/opt/ATS/ATS2-Postiats-0.2.3/ccomp/runtime/pats_ccomp_instrset.h:266:37: note: in definition of macro ‘ATSINSmove’

 #define ATSINSmove(tmp, val) (tmp = val)

                                     ^

DATS/main_dats.c:18821:41: error: ‘g0int2uint’ undeclared (first use in this function)

 ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

                                         ^

/opt/ATS/ATS2-Postiats-0.2.3/ccomp/runtime/pats_ccomp_instrset.h:266:37: note: in definition of macro ‘ATSINSmove’

 #define ATSINSmove(tmp, val) (tmp = val)

                                     ^

DATS/main_dats.c:18821:1: warning: implicit declaration of function ‘S2Eextkind’ [-Wimplicit-function-declaration]

 ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

 ^

In file included from DATS/main_dats.c:15:0:

DATS/main_dats.c:18821:63: error: expected expression before ‘atstype_int’

 ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

                                                               ^

/opt/ATS/ATS2-Postiats-0.2.3/ccomp/runtime/pats_ccomp_instrset.h:266:37: note: in definition of macro ‘ATSINSmove’

 #define ATSINSmove(tmp, val) (tmp = val)

                                     ^

DATS/main_dats.c:18821:88: error: expected expression before ‘atstype_uint8’

 ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

No going to the C code:

ATSstatic()

/*

imparg = tk(4495)

tmparg = S2Evar(tk(4495))

tmpsub = Some(tk(4495) -> S2Eextkind(atstype_uint8))

*/

atstkind_t0ype(atstype_bool)

ATSLIB_056_prelude__lt_g0uint_int__211__1(atstkind_t0ype(atstype_uint8) arg0, atstkind_t0ype(atstype_int) arg1)

{

/* tmpvardeclst(beg) */

ATStmpdec(tmpret720__1, atstkind_t0ype(atstype_bool)) ;

ATStmpdec(tmp721__1, atstkind_t0ype(atstype_uint8)) ;

/* tmpvardeclst(end) */

ATSfunbody_beg()

/*

emit_instr: loc0 = /opt/ATS/ATS2-Postiats-0.2.3/prelude/DATS/integer.dats: 30626(line=879, offs=1) -- 30682(line=879, offs=57)

*/

ATSINSflab(__patsflab_lt_g0uint_int):

/*

emit_instr: loc0 = /opt/ATS/ATS2-Postiats-0.2.3/prelude/DATS/integer.dats: 30667(line=879, offs=42) -- 30680(line=879, offs=55)

*/

ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

/*

emit_instr: loc0 = /opt/ATS/ATS2-Postiats-0.2.3/prelude/DATS/integer.dats: 30649(line=879, offs=24) -- 30682(line=879, offs=57)

*/

ATSINSmove(tmpret720__1, atspre_g0uint_lt_uint8(arg0, tmp721__1)) ;

ATSfunbody_end()

ATSreturn(tmpret720__1) ;

} /* end of [ATSLIB_056_prelude__lt_g0uint_int__211__1] */

The error is specifically on this line:

/*

emit_instr: loc0 = /opt/ATS/ATS2-Postiats-0.2.3/prelude/DATS/integer.dats: 30667(line=879, offs=42) -- 30680(line=879, offs=55)

*/

ATSINSmove(tmp721__1, PMVtmpltcstmat[0](g0int2uint<S2Eextkind(atstype_int), S2Eextkind(atstype_uint8)>)(arg1)) ;

The arduino_ats tree includes the integer.cats/dats in its prelude.

Is the compile process supposed to generate a function g0int2uint and put it in the application C file?

[Hongwei Xi]

The error indicates that the compiler could not find g0int2uint<int,uint8>, which is for casting int to uint8.

You can use $UN.cast to replace g0int2uint, or simply add the following implementation somewhere in your code:

implement

g0int2uint<int,uint8> (x) = $UN.cast{uint8}(x)

--
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/1cd4da0e-0860-49b6-bc0d-81805744b00b%40googlegroups.com.

[Mike Jones]

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.

[gmhwxi]

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.

[Mike Jones]

Ah.....

Typically when the compiler error points to the ATS code, it is a bit easier to guess the problem. I found the place to fix, but had I written a lot of code at once, it might be hard to find.

At least I have been trained by Haskell to expect some compiler messages difficult to decode :-)

Mike

[gmhwxi]

intBtwe2(0x30, 0x39, 0x41, 0x46)

can also be written as intBtwe2('0', '9', 'A', 'F').

When a char is used as an index, it is mapped to its ascii code.