Add some more tests (failing currently).
Chris Pressey
3 years ago

532 | 532 | |

533 | 533 | #### tables: range checking #### |

534 | 534 | |

535 | If a table has fewer than 256 entries, it cannot be read or written | |

536 | beyond the maximum number of entries it has. | |

535 | It is a static analysis error if it cannot be proven that a read or write | |

536 | to a table falls within the defined size of that table. | |

537 | ||

538 | (If a table has 256 entries, then there is never a problem, because a byte | |

539 | cannot index any entry outside of 0..255.) | |

540 | ||

541 | A SixtyPical implementation must be able to prove that the index is inside | |

542 | the range of the table in various ways. The simplest is to show that a | |

543 | constant value falls inside or outside the range of the table. | |

537 | 544 | |

538 | 545 | | byte table[32] many |

539 | 546 | | |

570 | 577 | | ld x, 32 |

571 | 578 | | ld a, 0 |

572 | 579 | | st a, many + x |

580 | | } | |

581 | ? RangeExceededError | |

582 | ||

583 | This applies to `copy` as well. | |

584 | ||

585 | | word one: 77 | |

586 | | word table[32] many | |

587 | | | |

588 | | routine main | |

589 | | inputs many, one | |

590 | | outputs many, one | |

591 | | trashes a, x, n, z | |

592 | | { | |

593 | | ld x, 31 | |

594 | | copy one, many + x | |

595 | | copy many + x, one | |

596 | | } | |

597 | = ok | |

598 | ||

599 | | word one: 77 | |

600 | | word table[32] many | |

601 | | | |

602 | | routine main | |

603 | | inputs many, one | |

604 | | outputs many, one | |

605 | | trashes a, x, n, z | |

606 | | { | |

607 | | ld x, 32 | |

608 | | copy many + x, one | |

609 | | } | |

610 | ? RangeExceededError | |

611 | ||

612 | | word one: 77 | |

613 | | word table[32] many | |

614 | | | |

615 | | routine main | |

616 | | inputs many, one | |

617 | | outputs many, one | |

618 | | trashes a, x, n, z | |

619 | | { | |

620 | | ld x, 32 | |

621 | | copy one, many + x | |

573 | 622 | | } |

574 | 623 | ? RangeExceededError |

575 | 624 |