6efa70d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Move buffer offset handling into idris code

6efa70dShea Levy13 years ago

libs/base/Data/Buffer.idr+30−36

compare with master

unifiedsplit

@@ -19,11 +19,14 @@ module Data.Buffer

19-- 6. Conversion from Fin to Bits64 (which, re 2, should eventually

20-- be a fixed-width implementation-dependent type) is likely

21-- inefficient relative to conversion from Nat to Bits64

22+-- 7. We may want to have a separate type that is a product of Buffer

23+-- and offset rather than storing the offset in Buffer itself, which

24+-- would require exposing the offset argument of prim__appendBuffer

23-- A contiguous chunk of n bytes

26-- A contiguous chunk of n bytes

24abstract

27abstract

25record Buffer : Nat -> Type where

28record Buffer : Nat -> Type where

26− MkBuffer : ( realBuffer : prim__UnsafeBuffer ) -> Buffer n

29+ MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n

28bitsFromNat : Nat -> Bits64

31bitsFromNat : Nat -> Bits64

29bitsFromNat Z = 0

32bitsFromNat Z = 0

@@ -38,28 +41,8 @@ bitsFromFin (fS k) = 1 + bitsFromFin k

38-- approximate ultimate size of the Buffer is known. Users can assume

41-- approximate ultimate size of the Buffer is known. Users can assume

39-- the new Buffer is word-aligned.

42-- the new Buffer is word-aligned.

40public

43public

41−allocate : ( hint : Nat ) -> Buffer 0

44+allocate : ( hint : Nat ) -> Buffer Z

42−allocate = MkBuffer . prim__allocate . bitsFromNat

45+allocate = MkBuffer Z . prim__allocate . bitsFromNat

43−

44−-- Copy a buffer. Since multiple buffers can reference the same

45−-- underlying chunk of memory, it may happen that a reference to

46−-- a relatively small bit of data might be preventing the runtime

47−-- from freeing a much larger chunk. copy allows giving up references

48−-- to the larger chunk without losing the smaller one.

49−%assert_total

50−public

51−copy : Buffer n -> Buffer n

52−copy { n } = MkBuffer . prim__copy ( bitsFromNat n ) . realBuffer

53−

54−-- Read a Buffer from another Buffer starting at offset

55−-- (i.e. create a view of a subset of the Buffer)

56−%assert_total

57−public

58−peekBuffer : Buffer ( m + n ) ->

59− ( offset : Fin ( S n ) ) ->

60− Buffer m

61−peekBuffer ( MkBuffer real ) =

62− MkBuffer . prim__peekBuffer real . bitsFromFin

64-- Append count repetitions of a Buffer to another Buffer

47-- Append count repetitions of a Buffer to another Buffer

65%assert_total

48%assert_total

@@ -67,24 +50,35 @@ public

67appendBuffer : Buffer n ->

50appendBuffer : Buffer n ->

68 ( count : Nat ) ->

51 ( count : Nat ) ->

69 Buffer m ->

52 Buffer m ->

70− Buffer ( n + m * count )

53+ Buffer ( n + count * m )

71−appendBuffer { n } { m } ( MkBuffer input ) count =

54+appendBuffer { n } { m } ( MkBuffer o1 r1 ) c ( MkBuffer o2 r2 ) =

72− MkBuffer . app . realBuffer

55+ MkBuffer o1 $ prim__appendBuffer r1 size1 count size2 off r2

73 where

56 where

74− nBits : Bits64

57+ size1 : Bits64

75− nBits = bitsFromNat n

58+ size1 = bitsFromNat ( n + o1 )

76− mBits : Bits64

59+ size2 : Bits64

77− mBits = bitsFromNat m

60+ size2 = bitsFromNat m

78− cBits : Bits64

61+ count : Bits64

79− cBits = bitsFromNat count

62+ count = bitsFromNat c

80− app = prim__appendBuffer input nBits cBits mBits

63+ off : Bits64

64+ off = bitsFromNat o2

65+

66+-- Copy a buffer, potentially allowing the (potentially large) space it

67+-- pointed to to be freed

68+public

69+copy : Buffer n -> Buffer n

70+copy { n } = replace ( plusZeroRightNeutral n ) . appendBuffer ( allocate n ) 1

72+-- Create a view over a buffer

73+public

74+peekBuffer : { n : Nat } -> { offset : Nat } -> Buffer ( n + offset ) -> ( offset : Nat ) -> Buffer n

75+peekBuffer ( MkBuffer o r ) off = MkBuffer ( o + off ) r

83peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->

77peekBits : ( prim__UnsafeBuffer -> Bits64 -> a ) ->

84 Buffer ( m + n ) ->

78 Buffer ( m + n ) ->

85 ( offset : Fin ( S n ) ) ->

79 ( offset : Fin ( S n ) ) ->

86 a

80 a

87−peekBits prim ( MkBuffer real ) = prim real . bitsFromFin

81+peekBits prim ( MkBuffer o r ) = prim r . bitsFromNat . plus o . finToNat

89appendBits : ( prim__UnsafeBuffer ->

83appendBits : ( prim__UnsafeBuffer ->

90 Bits64 ->

84 Bits64 ->

@@ -95,8 +89,8 @@ appendBits : ( prim__UnsafeBuffer ->

95 ( count : Nat) ->

89 ( count : Nat) ->

96 a ->

90 a ->

97 Buffer ( n + count * size )

91 Buffer ( n + count * size )

98−appendBits { n } prim ( MkBuffer real ) count =

92+appendBits { n } prim ( MkBuffer o r ) count =

99− MkBuffer . prim real ( bitsFromNat n ) ( bitsFromNat count )

93+ MkBuffer o . prim r ( bitsFromNat $ n + o ) ( bitsFromNat count )

100

101

102-- Read a Bits8 from a Buffer starting at offset

96-- Read a Bits8 from a Buffer starting at offset

rts/idris_gc.c+1−8

@@ -30,9 +30,6 @@ VAL copy(VM* vm, VAL x) {

30 case BUFFER:

31 cl = MKBUFFERc(vm, x->info.buf);

32 break;

33− case BUFOFFSET:

34− cl = MKBUFOFFSETc(vm, x->info.buf_offset);

35− break;

36 case BIGINT:

33 case BIGINT:

37 cl = MKBIGMc(vm, x->info.ptr);

34 cl = MKBIGMc(vm, x->info.ptr);

38 break;

35 break;

@@ -69,7 +66,7 @@ void cheney(VM *vm) {

69 while(scan < vm->heap.next) {

66 while(scan < vm->heap.next) {

70 size_t inc = *((size_t*)scan);

67 size_t inc = *((size_t*)scan);

71 VAL heap_item = (VAL)(scan+sizeof(size_t));

68 VAL heap_item = (VAL)(scan+sizeof(size_t));

72− // If it's a CON, STROFFSET, or BUFOFFSET, copy its arguments

69+ // If it's a CON or STROFFSET, copy its arguments

73 switch(GETTY(heap_item)) {

70 switch(GETTY(heap_item)) {

74 case CON:

71 case CON:

75 ar = ARITY(heap_item);

72 ar = ARITY(heap_item);

@@ -84,10 +81,6 @@ void cheney(VM *vm) {

84 heap_item->info.str_offset->str

81 heap_item->info.str_offset->str

85 = copy(vm, heap_item->info.str_offset->str);

82 = copy(vm, heap_item->info.str_offset->str);

86 break;

83 break;

87− case BUFOFFSET:

88− heap_item->info.buf_offset->buf

89− = copy(vm, heap_item->info.buf_offset->buf);

90− break;

91 default: // Nothing to copy

84 default: // Nothing to copy

92 break;

85 break;

93 }

86 }

rts/idris_heap.c−9

@@ -106,15 +106,6 @@ void heap_check_pointers(Heap * heap) {

106 }

107 break;

108 }

109− case BUFOFFSET:

110− if (!ref_in_heap(heap, heap_item->info.buf_offset->buf)) {

111− fprintf(stderr,

112− "RTS ERROR: heap closure broken. "\

113− "<HEAP %p %p %p> <REF %p>\n",

114− heap->heap, heap->next, heap->end, heap_item->info.buf_offset->buf);

115− exit(EXIT_FAILURE);

116− }

117− break;

118 case FWD:

109 case FWD:

119 // Check for artifacts after cheney gc.

110 // Check for artifacts after cheney gc.

120 fprintf(stderr, "RTS ERROR: FWD in working heap.\n");

111 fprintf(stderr, "RTS ERROR: FWD in working heap.\n");

rts/idris_rts.c+54−165

@@ -483,22 +483,6 @@ VAL MKBUFFERc(VM* vm, Buffer* buf) {

483 return cl;

484}

485

486−static VAL make_buf_offset(VM* vm, BufOffset* off, int outerlock) {

487− Closure* cl = allocate(vm, sizeof(Closure) + sizeof *off, outerlock);

488− SETTY(cl, BUFOFFSET);

489− cl->info.buf_offset = (BufOffset*)((void*)cl + sizeof(Closure));

490− memmove(cl->info.buf_offset, off, sizeof *off);

491− return cl;

492−}

493−

494−static VAL MKBUFOFFSET(VM* vm, BufOffset* off) {

495− return make_buf_offset(vm, off, 0);

496−}

497−

498−VAL MKBUFOFFSETc(VM* vm, BufOffset* off) {

499− return make_buf_offset(vm, off, 1);

500−}

501−

502static VAL internal_allocate(VM *vm, size_t hint) {

486static VAL internal_allocate(VM *vm, size_t hint) {

503 size_t size = hint + sizeof(Closure) + sizeof(Buffer);

487 size_t size = hint + sizeof(Closure) + sizeof(Buffer);

504

488

@@ -523,17 +507,6 @@ VAL idris_allocate(VM* vm, VAL hint) {

523 return cl;

507 return cl;

524}

508}

525

509

526−VAL idris_copy(VM* vm, VAL len, VAL src) {

527− size_t length = len->info.bits64;

528− Closure* cl = internal_allocate(vm, length);

529− memmove(cl->info.buf->store, (GETTY(src) == BUFOFFSET ?

530− src->info.buf_offset->buf->info.buf->store + src->info.buf_offset->offset :

531− src->info.buf->store

532− ), length);

533− cl->info.buf->fill = length;

534− return cl;

535−}

536−

537static void internal_memset(void *dest, const void *src, size_t size, size_t num) {

510static void internal_memset(void *dest, const void *src, size_t size, size_t num) {

538 while (num--) {

511 while (num--) {

539 memmove(dest, src, size);

512 memmove(dest, src, size);

@@ -541,95 +514,49 @@ static void internal_memset(void *dest, const void *src, size_t size, size_t num

541 }

514 }

542}

515}

543

516

544−static void internal_prepare_append(VM* vm, VAL buf, size_t bufLen, size_t appLen, void** storePtr, Closure** valPtr) {

517+static VAL internal_prepare_append(VM* vm, VAL buf, size_t bufLen, size_t appLen) {

545 size_t totalLen = bufLen + appLen;

518 size_t totalLen = bufLen + appLen;

546− // Might be able to get rid of some duplication here...

519+ Closure* cl;

547− if (GETTY(buf) == BUFOFFSET) {

548− if (buf->info.buf_offset->offset + bufLen !=

549− buf->info.buf_offset->buf->info.buf->fill ||

520+ if (bufLen != buf->info.buf->fill ||

550− buf->info.buf_offset->offset + totalLen >

551− buf->info.buf_offset->buf->info.buf->cap) {

521+ totalLen > buf->info.buf->cap) {

552− // We're not at the fill or are over cap, so need a new buffer

522+ // We're not at the fill or are over cap, so need a new buffer

553− *valPtr = internal_allocate(vm, totalLen);

523+ cl = internal_allocate(vm, totalLen);

554− memmove((*valPtr)->info.buf->store,

524+ memmove(cl->info.buf->store,

555− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset,

525+ buf->info.buf->store,

556− bufLen);

526+ bufLen);

557− (*valPtr)->info.buf->fill = totalLen;

527+ cl->info.buf->fill = totalLen;

558− *storePtr = (*valPtr)->info.buf->store + bufLen;

559− } else {

560− // Hooray, can just bump the fill

561− *valPtr = buf;

562− buf->info.buf_offset->buf->info.buf->fill += appLen;

563− *storePtr = buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + bufLen;

564− }

565 } else {

528 } else {

566− Buffer* newBuf;

567− if (bufLen != buf->info.buf->fill ||

568− totalLen > buf->info.buf->cap) {

569− // We're not at the fill or are over cap, so need a new buffer

570− *valPtr = internal_allocate(vm, totalLen);

571− newBuf = (*valPtr)->info.buf;

572− memmove(newBuf->store,

573− buf->info.buf->store,

574− bufLen);

575− newBuf->fill = totalLen;

576− } else {

577− // Hooray, can just bump the fill

529+ // Hooray, can just bump the fill

578− *valPtr = buf;

530+ cl = buf;

579− newBuf = buf->info.buf;

580− newBuf->fill += appLen;

531+ cl->info.buf->fill += appLen;

581− }

582− *storePtr = newBuf->store + bufLen;

583 }

532 }

533+ return cl;

584}

534}

585

535

586−VAL idris_appendBuffer(VM* vm, VAL fst, VAL fstLen, VAL cnt, VAL sndLen, VAL snd) {

536+VAL idris_appendBuffer(VM* vm, VAL fst, VAL fstLen, VAL cnt, VAL sndLen, VAL sndOff, VAL snd) {

587 size_t firstLength = fstLen->info.bits64;

537 size_t firstLength = fstLen->info.bits64;

588 size_t secondLength = sndLen->info.bits64;

538 size_t secondLength = sndLen->info.bits64;

589 size_t count = cnt->info.bits64;

539 size_t count = cnt->info.bits64;

590− void* store;

540+ size_t offset = sndOff->info.bits64;

591− Closure *cl;

592− internal_prepare_append(vm, fst, firstLength, count * secondLength, &store, &cl);

541+ Closure* cl = internal_prepare_append(vm, fst, firstLength, count * secondLength);

593− internal_memset(store, GETTY(snd) == BUFOFFSET ?

542+ internal_memset(cl->info.buf->store + firstLength, snd->info.buf->store + offset, secondLength, count);

594− snd->info.buf_offset->buf->info.buf->store + snd->info.buf_offset->offset :

595− snd->info.buf->store

596− , secondLength, count);

597 return cl;

543 return cl;

598}

544}

599

545

600−VAL idris_peekBuffer(VM* vm, VAL src, VAL off) {

601− size_t offset = off->info.bits64;

602− if (offset == 0)

603− return src;

604− BufOffset b;

605− if (GETTY(src) == BUFOFFSET) {

606− b.buf = src->info.buf_offset->buf;

607− b.offset = src->info.buf_offset->offset + offset;

608− } else {

609− b.buf = src;

610− b.offset = offset;

611− }

612− return MKBUFOFFSET(vm, &b);

613−}

614−

615// Special cased because we can use memset

546// Special cased because we can use memset

616VAL idris_appendB8Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

547VAL idris_appendB8Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

617 size_t bufLen = len->info.bits64;

548 size_t bufLen = len->info.bits64;

618 size_t count = cnt->info.bits64;

549 size_t count = cnt->info.bits64;

619− void* store;

620− Closure* cl;

621− internal_prepare_append(vm, buf, bufLen, count, &store, &cl);

550+ Closure* cl = internal_prepare_append(vm, buf, bufLen, count);

622− memset(store, val->info.bits8, count);

551+ memset(cl->info.buf->store + bufLen, val->info.bits8, count);

623 return cl;

552 return cl;

624}

553}

625

554

626static VAL internal_append_bits(VM* vm, VAL buf, VAL bufLen, VAL cnt, const void* val, size_t val_len) {

555static VAL internal_append_bits(VM* vm, VAL buf, VAL bufLen, VAL cnt, const void* val, size_t val_len) {

627 size_t len = bufLen->info.bits64;

556 size_t len = bufLen->info.bits64;

628 size_t count = cnt->info.bits64;

557 size_t count = cnt->info.bits64;

629− void* store;

630− Closure* cl;

631− internal_prepare_append(vm, buf, len, count * val_len, &store, &cl);

558+ Closure* cl = internal_prepare_append(vm, buf, len, count * val_len);

632− internal_memset(store, val, val_len, count);

559+ internal_memset(cl->info.buf->store + len, val, val_len, count);

633 return cl;

560 return cl;

634}

561}

635

562

@@ -708,104 +635,78 @@ VAL idris_appendB64BE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val) {

708

635

709VAL idris_peekB8Native(VM* vm, VAL buf, VAL off) {

636VAL idris_peekB8Native(VM* vm, VAL buf, VAL off) {

710 size_t offset = off->info.bits64;

637 size_t offset = off->info.bits64;

711− uint8_t* val = GETTY(buf) == BUFOFFSET ?

712− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

713− buf->info.buf->store + offset;

638+ uint8_t *val = buf->info.buf->store + offset;

714 return MKB8(vm, *val);

639 return MKB8(vm, *val);

715}

640}

716

641

717VAL idris_peekB16Native(VM* vm, VAL buf, VAL off) {

642VAL idris_peekB16Native(VM* vm, VAL buf, VAL off) {

718 size_t offset = off->info.bits64;

643 size_t offset = off->info.bits64;

719− uint16_t* val = (uint16_t *) ((GETTY(buf) == BUFOFFSET) ?

720− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

721− buf->info.buf->store + offset);

644+ uint16_t *val = (uint16_t *) (buf->info.buf->store + offset);

722 return MKB16(vm, *val);

645 return MKB16(vm, *val);

723}

646}

724

647

725VAL idris_peekB16LE(VM* vm, VAL buf, VAL off) {

648VAL idris_peekB16LE(VM* vm, VAL buf, VAL off) {

726 size_t offset = off->info.bits64;

649 size_t offset = off->info.bits64;

727− unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

728− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

729− buf->info.buf->store + offset;

730− return MKB16(vm, ((uint16_t) val[0]) +

650+ return MKB16(vm, ((uint16_t) buf->info.buf->store[offset]) +

731− (((uint16_t) val[1]) << 8));

651+ (((uint16_t) buf->info.buf->store[offset + 1]) << 8));

732}

652}

733

653

734VAL idris_peekB16BE(VM* vm, VAL buf, VAL off) {

654VAL idris_peekB16BE(VM* vm, VAL buf, VAL off) {

735 size_t offset = off->info.bits64;

655 size_t offset = off->info.bits64;

736− unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

737− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

738− buf->info.buf->store + offset;

739− return MKB16(vm, ((uint16_t) val[1]) +

656+ return MKB16(vm, ((uint16_t) buf->info.buf->store[offset + 1]) +

740− (((uint16_t) val[0]) << 8));

657+ (((uint16_t) buf->info.buf->store[offset]) << 8));

741}

658}

742

659

743VAL idris_peekB32Native(VM* vm, VAL buf, VAL off) {

660VAL idris_peekB32Native(VM* vm, VAL buf, VAL off) {

744 size_t offset = off->info.bits64;

661 size_t offset = off->info.bits64;

745− uint32_t* val = (uint32_t *) ((GETTY(buf) == BUFOFFSET) ?

746− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

747− buf->info.buf->store + offset);

662+ uint32_t *val = (uint32_t *) (buf->info.buf->store + offset);

748 return MKB32(vm, *val);

663 return MKB32(vm, *val);

749}

664}

750

665

751VAL idris_peekB32LE(VM* vm, VAL buf, VAL off) {

666VAL idris_peekB32LE(VM* vm, VAL buf, VAL off) {

752 size_t offset = off->info.bits64;

667 size_t offset = off->info.bits64;

753− unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

754− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

755− buf->info.buf->store + offset;

756− return MKB32(vm, ((uint32_t) val[0]) +

668+ return MKB32(vm, ((uint32_t) buf->info.buf->store[offset]) +

757− (((uint32_t) val[1]) << 8) +

669+ (((uint32_t) buf->info.buf->store[offset + 1]) << 8) +

758− (((uint32_t) val[2]) << 16) +

670+ (((uint32_t) buf->info.buf->store[offset + 2]) << 16) +

759− (((uint32_t) val[3]) << 24));

671+ (((uint32_t) buf->info.buf->store[offset + 3]) << 24));

760}

672}

761

673

762VAL idris_peekB32BE(VM* vm, VAL buf, VAL off) {

674VAL idris_peekB32BE(VM* vm, VAL buf, VAL off) {

763 size_t offset = off->info.bits64;

675 size_t offset = off->info.bits64;

764− unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

765− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

766− buf->info.buf->store + offset;

767− return MKB32(vm, ((uint32_t) val[3]) +

676+ return MKB32(vm, ((uint32_t) buf->info.buf->store[offset + 3]) +

768− (((uint32_t) val[2]) << 8) +

677+ (((uint32_t) buf->info.buf->store[offset + 2]) << 8) +

769− (((uint32_t) val[1]) << 16) +

678+ (((uint32_t) buf->info.buf->store[offset + 1]) << 16) +

770− (((uint32_t) val[0]) << 24));

679+ (((uint32_t) buf->info.buf->store[offset]) << 24));

771}

680}

772

681

773VAL idris_peekB64Native(VM* vm, VAL buf, VAL off) {

682VAL idris_peekB64Native(VM* vm, VAL buf, VAL off) {

774 size_t offset = off->info.bits64;

683 size_t offset = off->info.bits64;

775− uint64_t* val = (uint64_t *) ((GETTY(buf) == BUFOFFSET) ?

776− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

777− buf->info.buf->store + offset);

684+ uint64_t *val = (uint64_t *) (buf->info.buf->store + offset);

778 return MKB64(vm, *val);

685 return MKB64(vm, *val);

779}

686}

780

687

781VAL idris_peekB64LE(VM* vm, VAL buf, VAL off) {

688VAL idris_peekB64LE(VM* vm, VAL buf, VAL off) {

782 size_t offset = off->info.bits64;

689 size_t offset = off->info.bits64;

783− unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

784− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

785− buf->info.buf->store + offset;

786− return MKB64(vm, ((uint64_t) val[0]) +

690+ return MKB64(vm, ((uint64_t) buf->info.buf->store[offset]) +

787− (((uint64_t) val[1]) << 8) +

691+ (((uint64_t) buf->info.buf->store[offset + 1]) << 8) +

788− (((uint64_t) val[2]) << 16) +

692+ (((uint64_t) buf->info.buf->store[offset + 2]) << 16) +

789− (((uint64_t) val[3]) << 24) +

693+ (((uint64_t) buf->info.buf->store[offset + 3]) << 24) +

790− (((uint64_t) val[4]) << 32) +

694+ (((uint64_t) buf->info.buf->store[offset + 4]) << 32) +

791− (((uint64_t) val[5]) << 40) +

695+ (((uint64_t) buf->info.buf->store[offset + 5]) << 40) +

792− (((uint64_t) val[6]) << 48) +

696+ (((uint64_t) buf->info.buf->store[offset + 6]) << 48) +

793− (((uint64_t) val[7]) << 56));

697+ (((uint64_t) buf->info.buf->store[offset + 7]) << 56));

794}

698}

795

699

796VAL idris_peekB64BE(VM* vm, VAL buf, VAL off) {

700VAL idris_peekB64BE(VM* vm, VAL buf, VAL off) {

797 size_t offset = off->info.bits64;

701 size_t offset = off->info.bits64;

798− unsigned char* val = (GETTY(buf) == BUFOFFSET) ?

799− buf->info.buf_offset->buf->info.buf->store + buf->info.buf_offset->offset + offset :

800− buf->info.buf->store + offset;

801− return MKB64(vm, ((uint64_t) val[7]) +

702+ return MKB64(vm, ((uint64_t) buf->info.buf->store[offset + 7]) +

802− (((uint64_t) val[6]) << 8) +

703+ (((uint64_t) buf->info.buf->store[offset + 6]) << 8) +

803− (((uint64_t) val[5]) << 16) +

704+ (((uint64_t) buf->info.buf->store[offset + 5]) << 16) +

804− (((uint64_t) val[4]) << 24) +

705+ (((uint64_t) buf->info.buf->store[offset + 4]) << 24) +

805− (((uint64_t) val[3]) << 32) +

706+ (((uint64_t) buf->info.buf->store[offset + 3]) << 32) +

806− (((uint64_t) val[2]) << 40) +

707+ (((uint64_t) buf->info.buf->store[offset + 2]) << 40) +

807− (((uint64_t) val[1]) << 48) +

708+ (((uint64_t) buf->info.buf->store[offset + 1]) << 48) +

808− (((uint64_t) val[0]) << 56));

709+ (((uint64_t) buf->info.buf->store[offset]) << 56));

809}

710}

810

711

811typedef struct {

712typedef struct {

@@ -888,18 +789,6 @@ VAL copyTo(VM* vm, VAL x) {

888 case BUFFER:

789 case BUFFER:

889 cl = MKBUFFERc(vm, x->info.buf);

790 cl = MKBUFFERc(vm, x->info.buf);

890 break;

791 break;

891− case BUFOFFSET:

892− // The underlying Buffer might already exist in the new heap

893− // but we can't do anything reasonable about it

894− if (x->info.buf_offset->offset == 0)

895− cl = MKBUFFERc(vm, x->info.buf_offset->buf->info.buf);

896− else {

897− // Could theoretically make this a bit more efficient

898− // by allocating the BufOffset and Buffer together

899− cl = MKBUFOFFSETc(vm, x->info.buf_offset);

900− cl->info.buf_offset->buf = MKBUFFERc(vm, x->info.buf_offset->buf->info.buf);

901− }

902− break;

903 case BIGINT:

792 case BIGINT:

904 cl = MKBIGMc(vm, x->info.ptr);

793 cl = MKBIGMc(vm, x->info.ptr);

905 break;

794 break;

rts/idris_rts.h+2−11

@@ -17,7 +17,7 @@

17typedef enum {

18 CON, INT, BIGINT, FLOAT, STRING, STROFFSET,

19 BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,

20− BUFFER, BUFOFFSET

20+ BUFFER

21} ClosureType;

23typedef struct Closure *VAL;

@@ -40,11 +40,6 @@ typedef struct {

40 unsigned char store[];

41} Buffer;

43−typedef struct {

44− VAL buf;

45− size_t offset;

46−} BufOffset;

47−

49typedef struct Closure {

44typedef struct Closure {

50// Use top 16 bits of ty for saying which heap value is in

45// Use top 16 bits of ty for saying which heap value is in

@@ -62,7 +57,6 @@ typedef struct Closure {

62 uint32_t bits32;

57 uint32_t bits32;

63 uint64_t bits64;

58 uint64_t bits64;

64 Buffer* buf;

59 Buffer* buf;

65− BufOffset* buf_offset;

66 } info;

60 } info;

67} Closure;

61} Closure;

@@ -180,7 +174,6 @@ VAL MKSTROFFc(VM* vm, StrOffset* off);

180VAL MKSTRc(VM* vm, char* str);

174VAL MKSTRc(VM* vm, char* str);

181VAL MKPTRc(VM* vm, void* ptr);

175VAL MKPTRc(VM* vm, void* ptr);

182VAL MKBUFFERc(VM* vm, Buffer* buf);

176VAL MKBUFFERc(VM* vm, Buffer* buf);

183−VAL MKBUFOFFSETc(VM* vm, BufOffset* off);

184

177

185char* GETSTROFF(VAL stroff);

178char* GETSTROFF(VAL stroff);

186

179

@@ -255,9 +248,7 @@ VAL idris_strRev(VM* vm, VAL str);

255

248

256// Buffer primitives

249// Buffer primitives

257VAL idris_allocate(VM* vm, VAL hint);

250VAL idris_allocate(VM* vm, VAL hint);

258−VAL idris_copy(VM* vm, VAL len, VAL src);

259−VAL idris_appendBuffer(VM* vm, VAL fst, VAL fstLen, VAL count, VAL sndLen, VAL snd);

251+VAL idris_appendBuffer(VM* vm, VAL fst, VAL fstLen, VAL cnt, VAL sndLen, VAL sndOff, VAL snd);

260−VAL idris_peekBuffer(VM* vm, VAL src, VAL off);

261VAL idris_appendB8Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

252VAL idris_appendB8Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

262VAL idris_appendB16Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

253VAL idris_appendB16Native(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

263VAL idris_appendB16LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

254VAL idris_appendB16LE(VM* vm, VAL buf, VAL len, VAL cnt, VAL val);

src/IRTS/CodegenC.hs+1−3

@@ -458,9 +458,7 @@ doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y

458doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

459

460doOp v LAllocate [x] = v ++ "idris_allocate(vm, " ++ creg x ++ ")"

461−doOp v LCopy [x, y] = v ++ "idris_copy(vm, " ++ creg x ++ "," ++ creg y ++ ")"

462−doOp v LAppendBuffer [a, b, c, d, e] = v ++ "idris_appendBuffer(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ "," ++ creg e ++ ")"

461+doOp v LAppendBuffer [a, b, c, d, e, f] = v ++ "idris_appendBuffer(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ "," ++ creg e ++ "," ++ creg f ++ ")"

463−doOp v LPeekBuffer [x, y] = v ++ "idris_peekBuffer(vm, " ++ creg x ++ "," ++ creg y ++ ")"

464doOp v (LAppend ity en) [a, b, c, d] = v ++ "idris_append" ++ intTyName ity ++ show en ++ "(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ ")"

462doOp v (LAppend ity en) [a, b, c, d] = v ++ "idris_append" ++ intTyName ity ++ show en ++ "(vm, " ++ creg a ++ "," ++ creg b ++ "," ++ creg c ++ "," ++ creg d ++ ")"

465doOp v (LPeek ity en) [x, y] = v ++ "idris_peek" ++ intTyName ity ++ show en ++ "(vm, " ++ creg x ++ "," ++ creg y ++ ")"

463doOp v (LPeek ity en) [x, y] = v ++ "idris_peek" ++ intTyName ity ++ show en ++ "(vm, " ++ creg x ++ "," ++ creg y ++ ")"

466

464

src/IRTS/Lang.hs−2

@@ -54,9 +54,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

55 -- Buffers

56 | LAllocate

57− | LCopy

58 | LAppendBuffer

57 | LAppendBuffer

59− | LPeekBuffer

60 -- Note that for Bits8 only Native endianness is actually used

58 -- Note that for Bits8 only Native endianness is actually used

61 -- and the user-exposed interface for Bits8 doesn't mention

59 -- and the user-exposed interface for Bits8 doesn't mention

62 -- endianness

60 -- endianness

src/Idris/Primitives.hs+2−6

@@ -176,12 +176,8 @@ primitives =

176 -- Buffers

177 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_cantreduce)

178 (1, LAllocate) total,

179− Prim (sUN "prim__copy") (ty [AType (ATInt (ITFixed IT64)), BufferType] BufferType) 2 (p_cantreduce)

180− (2, LCopy) partial,

181− Prim (sUN "prim__peekBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64))] BufferType) 2 (p_cantreduce)

182− (2, LPeekBuffer) partial,

183− Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 5 (p_cantreduce)

179+ Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 6 (p_cantreduce)

184− (5, LAppendBuffer) partial

180+ (6, LAppendBuffer) partial

185 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

181 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

186 ++ concatMap vecOps vecTypes

182 ++ concatMap vecOps vecTypes

187 ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes

183 ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes