wclines: fast counting newlines

[gmhwxi]

FYI.

I implemented wclines (i.e., wc --lines) in a way that makes use of rawmemchr
(available with the flag -D_GNU_SOURCE). It should be faster than the version
using memchr. Here is the source code of wclines:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/wclines.dats

This implementation also shows a style of mixing C code with ATS code, which I
have been learning, exploring and practicing for quite some time.

Cheers,

--Hongwei

[Brandon Barker]

Very interesting code, in more ways than one (I didn't know about  -D_GNU_SOURCE or rawmemchr).

I'm ashamed to say I got nearly all the way through backporting to ATS1 but one line in particular is keeping it from typechecking (if commented out it typechecks). Having a bit of trouble exactly interpreting the error.

/media/RAID5/share/ATS_learning/wclines.dats: 2707(line=133, offs=30) -- 2709(line=133, offs=32): error(3): unsolved constraint: C3STRprop(main; S2Eeqeq(S2Eapp(S2Ecst(add_addr_int_addr); S2EVar(2437), S2Eint(1)), S2Eapp(S2Ecst(add_addr_int_addr); S2EVar(2436), S2Eapp(S2Ecst(sizeof); S2EVar(2434)))))

type-checking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.

exit(ATS): uncaught exception: _2fhome_2ffac2_2fhwxi_2fresearch_2fATS_2fIMPLEMENT_2fGeizella_2fAnairiats_2fsvn_2fats_2dlang_2fsrc_2fats_error_2esats__FatalErrorException(1233)

staload _(*anon*) = "libc/SATS/stdio.sats"

//

staload _(*anon*) = "prelude/DATS/array.dats"

staload _(*anon*) = "prelude/DATS/array0.dats"

//

staload _(*anon*) = "prelude/DATS/list.dats"

staload _(*anon*) = "prelude/DATS/list0.dats"

staload _(*anon*) = "prelude/DATS/list_vt.dats"

//

staload _(*anon*) = "prelude/DATS/matrix.dats"

staload _(*anon*) = "prelude/DATS/matrix0.dats"

//

staload _(*anon*) = "prelude/DATS/option.dats"

staload _(*anon*) = "prelude/DATS/option0.dats"

//

staload _(*anon*) = "prelude/DATS/pointer.dats"

//

staload _(*anon*) = "prelude/DATS/reference.dats"

//

(* ****** ****** *)

staload

UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)

staload "libc/SATS/stdio.sats"

(* ****** ****** *)

viewdef bytes_v (l:addr, n:int) = bytes (n) @ l

extern

fun ptr0_add_bytesize (p: ptr, ofs: size_t):<> ptr 

implement

ptr0_add_bytesize(p,ofs) = p+ofs

symintr ptr_succ

extern

fun

ptr0_succ (p: ptr):<> ptr

overload ptr_succ with ptr0_succ

extern

fun

ptr1_succ {l:addr} (p: ptr l):<> ptr (l+1)

overload ptr_succ with ptr1_succ

implement

ptr1_succ {l} (p) =

$UN.cast{ptr(l+1)}(ptr0_succ (p))

  

implement

ptr0_succ (p) = ptr0_add_bytesize (p, 1)

extern

praxi

bytes_v_unsplit

  {l:addr}{n1,n2:int}

  (pf1: (bytes_v (l, n1), bytes_v (l+n1, n2))): bytes_v (l, n1+n2)

// end of [bytes_v_unsplit]

(* ****** ****** *)

%{^

extern

void

*rawmemchr(const void *s, int c);

#define atslib_rawmemchr rawmemchr

%}

extern

fun rawmemchr

  {l:addr}{m:int}

(

  pf: bytes_v (l, m) | p: ptr l, c: int

) : [l2:addr | l+m > l2]

(

  bytes_v (l, l2-l), bytes_v (l2, l+m-l2) | ptr l2

) = "mac#atslib_rawmemchr" // end of [rawmemchr]

(* ****** ****** *)

#define BUFSZ 16384 

(* ****** ****** *)

extern fun fread1 {l:addr} {n:nat} {f:fm} (pf_mod: file_mode r 

  | dest: ptr l, sz: size_t 1, count: size_t n, fil: FILEref)

  : [m:nat] size_t m = "mac#fread"

extern

fun freadc // read bytes and then add [c] at the end 

  {b:nat} 

  {l:addr}

(

  pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: char, b: size_t b

) : size_t // end of [freadc]

implement

freadc (pf | inp, p, c, b) = let

  val [m:int] m = fread1(file_mode_r | p, 1, b, inp) 

  val () = assertloc (p > null)

//  val _ = if p <> null then  

  val () = $UN.ptrset<char> (p+m, c)

   

//  else ()

in

  m

end (* end of [freadc] *)

(* ****** ****** *)

extern

fun wclbuf

  {l:addr}{n:int}

(

  pf: !bytes_v (l, n) | p: ptr l, pz: ptr, c: int, res: int

) : int // end of [wclbuf]

implement

wclbuf (pf | p, pz, c, res) =

(

  if p < pz then let

    val (pf1, pf2 | p2) = rawmemchr (pf | p, c)

    prval (pf21, pf22) = array_v_uncons (pf2)

    val _ = $showtype p

    val p2 = ptr_succ(p2)

    val _ = $showtype p

    val res = wclbuf (pf22 | p2, pz, c, res + 1)

    prval () = pf2 := array_v_cons (pf21, pf22)

    prval () = pf := bytes_v_unsplit (pf1, pf2)

  in

    res

  end else

    res

  // end of [if]

) // end of [wcbuf]

(* ****** ****** *)

extern

fun wclfil{l:addr}

(

  pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: int

) : int // end of [wclfil]

implement

wclfil{l}

  (pf | inp, p, c) = let

//

fun loop

(

  pf: !bytes_v (l, BUFSZ)

| inp: FILEref, p: ptr l, c: int, res: int

) : int = let

//

val n = freadc (pf | inp, p, $UN.cast{char}(c), size1_of_int1(BUFSZ-1))

//

in

//

if n > 0 then let

  //val pz = ptr_add<char> (p, n)

  val pz = p+n

  val res = wclbuf (pf | p, pz, c, res)

in

  loop (pf | inp, p, c, res)

end else res (* end of [if] *)

//

end // end of [loop]

//

in

  loop (pf | inp, p, c, 0(*res*))

end (* end of [wclfil] *)

(* ****** ****** *)

implement

main {n} (argc, argv) = () where 

{

var inp: FILEref = stdin_ref

val () =

(

if argc >= 2 then

  inp := fopen_ref_exn (argv[1], file_mode_r)

// end of [if]

)

//

val (

  pfopt | p

) = malloc_ngc (BUFSZ)

val () = assert_errmsg (p > null, #LOCATION)

prval malloc_v_succ (pf_ngc, pf_buf) = pfopt

prval () = pf_buf := bytes_v_of_b0ytes_v (pf_buf)

val res = wclfil (pf_buf | inp, p, $UN.cast2int('\n'))

val () = free_ngc (pf_ngc, pf_buf | p)

//

val () = println! ("wclines: number of lines = ", res)

//

val () = if argc >= 2 then fclose_exn (inp)

} (* end of [main0] *)

(* ****** ****** *)

(* end of [wclines.dats] *)

[gmhwxi]

The typechecker does not know sizeof(byte) = 1. You can introduce
the following lemma and use it somewhere inside the body of wclbuf:

extern
praxi lemma_sizeof_byte (): [sizeof(byte)==1] void

[gmhwxi]

I just tried your code. You also need the following line:

staload _(*anon*) = "prelude/DATS/unsafe.dats"

That is it!

Cheers,

--Hongwei

[gmhwxi]

BTW, I have never compared rawmemchr with memchr in terms of performance.
Is wclines faster than your version that uses memchr?

[Brandon Barker]

Yes, I discovered that anonymous staload problem.

All i can say is that it is as fast as wc -l on my ubuntu 64 box :), and slightly faster than my memchr version (the only difference between my c memchr version and wc is that wc uses a function called "safe_read", so that may be balancing it out somehow. I can look in to safe_read as well as trying out memchr vs rawmemchr.

Unfortunately I'm getting an off by 1 disagreement with wclines and other programs on a large file. It isn't the last bit of the file causing the problem either (at least, not using "tail large_file > test.txt" . I will check it more tomorrow.

[gmhwxi]

>>Unfortunately I'm getting an off by 1 disagreement with wclines and other programs on a large file. It isn't the last bit of the file causing the problem either (at least, not using "tail large_file > test.txt" . I will check it more tomorrow.

I think that the reason for this off-by-1 disagreement is this: for 'wc', EOF is considered a newline if it does not follow '\n' immediately; for wclines, 'EOF' is never counted as a newline.

[gmhwxi]

In the above comment, 'wc' and 'wclines' should be swapped.

Anyway, I made a quick fix. Now 'wc --lines' and 'wclines' should always concur. Changes have been uploaded.

[Brandon Barker]

Now that I look more closely; my backported version is not just off by 1; it is reading in more lines.

I'm trying to build your latest version in ATS2 to check to see if it is something I did, but I'm encountering some build errors (I fetched the most recent ATS2 version from github, copied over the old directory, then rebuilt per instructions). Here's the makefile for wclines:

brandon@gulab:/media/RAID5/share/ATS_learning$ make -f Makefile_wclines_a2 

gcc -std=c99 -D_GNU_SOURCE -O2     -I"/media/RAID5/share/ATS_learning/ATS-Postiats" -I"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/runtime -DATS_MEMALLOC_LIBC -o wclines_a2.exe wclines_a2_dats.c -L"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/atslib/lib -latslib

wclines_a2_dats.c:139:1: warning: data definition has no type or storage class [enabled by default]

wclines_a2_dats.c:139:1: warning: type defaults to ‘int’ in declaration of ‘ATSdyncst_unknown’ [enabled by default]

wclines_a2_dats.c:139:1: warning: parameter names (without types) in function declaration [enabled by default]

wclines_a2_dats.c: In function ‘ATSLIB_056$prelude_ptr0_succ$12$1’:

wclines_a2_dats.c:487:1: error: ‘atstype_byte’ undeclared (first use in this function)

wclines_a2_dats.c:487:1: note: each undeclared identifier is reported only once for each function it appears in

wclines_a2_dats.c: In function ‘mainats_argc_argv_0’:

wclines_a2_dats.c:790:1: error: ‘ATSLIB_056$prelude_file_mode_r’ undeclared (first use in this function)

make: *** [wclines_a2.exe] Error 1

This results in:

brandon@gulab:/media/RAID5/share/ATS_learning$ make -f Makefile_wclines_a2 

gcc -std=c99 -D_GNU_SOURCE -O2     -I"/media/RAID5/share/ATS_learning/ATS-Postiats" -I"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/runtime -DATS_MEMALLOC_LIBC -o wclines_a2.exe wclines_a2_dats.c -L"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/atslib/lib -latslib

wclines_a2_dats.c:139:1: warning: data definition has no type or storage class [enabled by default]

wclines_a2_dats.c:139:1: warning: type defaults to ‘int’ in declaration of ‘ATSdyncst_unknown’ [enabled by default]

wclines_a2_dats.c:139:1: warning: parameter names (without types) in function declaration [enabled by default]

wclines_a2_dats.c: In function ‘ATSLIB_056$prelude_ptr0_succ$12$1’:

wclines_a2_dats.c:487:1: error: ‘atstype_byte’ undeclared (first use in this function)

wclines_a2_dats.c:487:1: note: each undeclared identifier is reported only once for each function it appears in

wclines_a2_dats.c: In function ‘mainats_argc_argv_0’:

wclines_a2_dats.c:790:1: error: ‘ATSLIB_056$prelude_file_mode_r’ undeclared (first use in this function)

make: *** [wclines_a2.exe] Error 1

[Brandon Barker]

Also a minor note, it seems I needed to add this in:

extern

praxi b0ytes2bytes_v {bsz:int}

  {l:addr} (pf: b0ytes (bsz) @ l):<prf> bytes (bsz) @ l

[gmhwxi]

I think you forgot to do

make -f codegen/Makefile_atslib

:)

Also, the above lemma is already in ATS2.

[gmhwxi]

I forgot to put the following line in stdio.cats:

#define atslib_fopen_ref_exn atslib_fopen_exn

You can put it in wclines.dats directly or git-pull again (and then do 'make -f codegen/Makefile_atslib').

[Brandon Barker]

You're right, I did forget make -f codegen/Makefile_atslib; I found the new build directions on the wiki now.

All of those fixes cleared everything up. It is the same speed as "wc -l" on my system. I think I'll save playing with speeding it up further for another time; it is good enough I think.

As for the bug, I think the original wclbuf conditional may have allowed the '\n' from freadc at the end of the buffer to be counted as well.

[Brandon Barker]

I'm trying to extend the code to return a dependently typed value (wclines should always return a natural number).  The last line of the wclfil function in minDisj.dats is giving a constraint error. Perhaps this is caused by a missing "upstream" constraint somewhere? I haven't found it yet if so.

[gmhwxi]

 int1_of_int(0) should be changed to 0; then the code typechecks.

[Brandon Barker]

Thanks; I see that both of these are dependent types now (any constant integer type appears to be a dependent type). Why is it that int1_of_int(0) does not work in this case? I think I'm missing something important here.

[gmhwxi]

int1_of_int : int -> Int; so the type of int1_of_int(0) is Int, which is for an integer of unknown value. That is why the typechecker complained.

[Brandon Barker]

Porting some changes I made in the ATS version to the ATS2 version (to recognize a missing \n before the EOF as a line) is giving me an error I'm not so sure of:

wclines_a2_dats.c:792:1: warning: implicit declaration of function âHITundefâ [-Wimplicit-function-declaration]

wclines_a2_dats.c:792:1: warning: implicit declaration of function âHSEs2expâ [-Wimplicit-function-declaration]

wclines_a2_dats.c:792:1: warning: implicit declaration of function âS2EVarâ [-Wimplicit-function-declaration]

wclines_a2_dats.c:792:1: error: expected â;â before âtmp44â

wclines_a2_dats.c:835:1: error: âtmp44â undeclared (first use in this function)

wclines_a2_dats.c:835:1: note: each undeclared identifier is reported only once for each function it appears in

(*

**

** A fast approach to counting newlines

**

** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)

** Time: April 17, 2013

**

*)

(* ****** ****** *)

//

#include

"share/atspre_staload_tmpdef.hats"

//

(* ****** ****** *)

staload

UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)

staload "libc/SATS/stdio.sats"

(* ****** ****** *)

//extern

//praxi b0ytes2bytes_v {bsz:int}

//  {l:addr} (pf: b0ytes (bsz) @ l):<prf> bytes (bsz) @ l

  

extern

praxi

bytes_v_unsplit

  {l:addr}{n1,n2:int}

  (pf: bytes_v (l, n1), bytes_v (l+n1, n2)): bytes_v (l, n1+n2)

// end of [bytes_v_unsplit]

(* ****** ****** *)

%{^

extern

void

*rawmemchr(const void *s, int c);

#define atslib_rawmemchr rawmemchr

%}

extern

fun rawmemchr

  {l:addr}{m:int}

(

  pf: bytes_v (l, m) | p: ptr l, c: int

) : [l2:addr | l+m > l2]

(

  bytes_v (l, l2-l), bytes_v (l2, l+m-l2) | ptr l2

) = "mac#atslib_rawmemchr" // end of [rawmemchr]

(* ****** ****** *)

#define BUFSZ (16*1024)

(* ****** ****** *)

extern

fun freadc // read bytes and then add [c] at the end

  {l:addr}

(

  pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: char

) : [n:nat] size_t n // end of [freadc]

implement

freadc (pf | inp, p, c) = let

  val n = $extfcall

    ([n:nat] size_t n, "fread", p, sizeof<char>, BUFSZ-1, inp)

  val () = $UN.ptr0_set<char> (ptr_add<char> (p, n), c)

in

  n

end (* end of [freadc] *)

(* ****** ****** *)

extern

fun wclbuf

  {l:addr}{n:int}

(

  pf: !bytes_v (l, n) | p: ptr l, pz: ptr, c: int, res: int

) : int // end of [wclbuf]

implement

wclbuf (pf | p, pz, c, res) = let

  val (pf1, pf2 | p2) = rawmemchr (pf | p, c)

in

//

if p2 < pz then let

  prval (pf21, pf22) = array_v_uncons (pf2)

  val res = wclbuf (pf22 | ptr_succ<byte>(p2), pz, c, res + 1)

  prval () = pf2 := array_v_cons (pf21, pf22)

  prval () = pf := bytes_v_unsplit (pf1, pf2)

in

  res

end else let

  prval () = pf := bytes_v_unsplit (pf1, pf2)

in

    res

end // end of [if]

//

end (* end of [wcbuf] *)

(* ****** ****** *)

extern

fun wclfil{l:addr}

(

  pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: int

) : int // end of [wclfil]

implement

wclfil{l}

  (pf | inp, p, c) = let

//

fun loop

(

  pf: !bytes_v (l, BUFSZ)

| inp: FILEref, p: ptr l, c: int, res: int

) : int = let

//

val n = freadc (pf | inp, p, $UN.cast{char}(c))

//

in

//

if n > 0 then let

  val pz = ptr_add<char> (p, n)

   //val () = assertloc (p > null)

  val nEOF = if n < (BUFSZ-1) then 

    (if ($UN.ptr0_get<char> (ptr_add<char> (p,sz2i(n)-1))) = '\n' then 0 else 1) 

    else 0  // end of [nEOF] 

  val res = wclbuf (pf | p, pz, c, res)

in

  loop (pf | inp, p, c, res)

end else res (* end of [if] *)

//

end // end of [loop]

//

in

  loop (pf | inp, p, c, 0(*res*))

end (* end of [wclfil] *)

(* ****** ****** *)

implement

main0 (argc, argv) =

{

var inp: FILEref = stdin_ref

val () =

(

if argc >= 2 then

  inp := fopen_ref_exn (argv[1], file_mode_r)

// end of [if]

)

//

val (

  pfat, pfgc | p

) = malloc_gc (g1i2u(BUFSZ))

prval () = pfat := b0ytes2bytes_v (pfat)

val res = wclfil (pfat | inp, p, $UN.cast2int('\n'))

val () = mfree_gc (pfat, pfgc | p)

[Brandon Barker]

Also I forgot to add in to wclfil:

val res = wclbuf (pf | p, pz, c, res)

should be:

val res = wclbuf (pf | p, pz, c, res+nEOF)

[gmhwxi]

You need a type annotation for now:

val nEOF =
  (

  if n < (BUFSZ-1) then
    (if ($UN.ptr0_get<char> (ptr_add<char> (p,sz2i(n)-1))) = '\n' then 0
    else 1)
    else 0

  ) : int  // end of [nEOF]

This will probably be fixed later so that such an annotation is not needed.

[gmhwxi]

Say, the file contains exactly BUFSZ many chars and none of them are '\n'. You version of wclines returns 0 but I think that you want it to return 1.

[Brandon Barker]

oh right, that is certainly a problem. 

I tried to correct it by doing:

val nEOF = (if n < (BUFSZ-1) orelse fileref_is_eof(inp)  ...

but I suppose EOF is not set yet either.

I will write a different version to retain the last read char.

[Brandon Barker]

I just wanted to post the corrected version of the loop:

fun loop

(

  pf: !bytes_v (l, BUFSZ)

| inp: FILEref, p: ptr l, c: int, res: int, last_c: int

) : int = let

//

val n = freadc (pf | inp, p, $UN.cast{char}(c))

//

in

//

if n > 0 then let

  val pz = ptr_add<char> (p, n)

  val last_c = $UN.cast2int($UN.ptr0_get<char> (ptr_add<char> (p,sz2i(n)-1)))

  val res = wclbuf (pf | p, pz, c, res (*+nEOF*))

in

  loop (pf | inp, p, c, res, last_c)

end else if last_c = c then res else res+1 (* end of [if n > 0] *)

[gmhwxi]

sz2i(n)-1 ==> pred(n)

It seems easier and faster if you keep the value of the [n] obtained in the previous round.
Then you only need to compute last_c once.

[Brandon Barker]

That sounds good; I didn't see it at first. When I try this, I get confronted with a dependent type error (just when I thought I was getting the hang of them). I also tried annotating with an "if last_n > 0", which seems necessary anyway given the starting condition for last_n.

extern

fun wclfil{l:addr}

(

  pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: int

) : int // end of [wclfil]

implement

wclfil{l}

  (pf | inp, p, c) = let

//

fun loop  {n:nat}

(

  pf: !bytes_v (l, BUFSZ)

| inp: FILEref, p: ptr l, c: int, res: int, last_n: size_t n

) : int = let

//

//val n = freadc (pf | inp, p, $UN.cast{char}(c), size1_of_int1(BUFSZ-1))

val n = freadc (pf | inp, p, $UN.cast{char}(c), size1_of_int1(BUFSZ))

//

in

//

if n > 0 then let

  //val pz = ptr_add<char> (p, n)

  val () = assertloc (p > null)

  val pz = p+n

  val res = wclbuf (pf | p, pz, c, res)

in

  loop (pf | inp, p, c, res, n)

end else (* else of [if n > 0] *) (if last_n > 0 then

  (if $UN.cast2int($UN.ptrget<char> (p+last_n-1)) = c then res

  else res + 1):int

  else 0):int

//

end // end of [loop]

//

in

  loop (pf | inp, p, c, 0(*res*), size1_of_int1(0) (*last_n*))

[gmhwxi]

First, svn-update your ATS (no need to re-compile).

Then change ptrget to ptr0_get. The latter is less picky.

It should fix this issue.