Defining Constraints
This section describes in detail with examples on how to define constrains. This is basically more theory of what we have seen in last section.
keep| This states restrictions on the values generated for fields in the struct or its subtree, or describes required relationships between field values and other items in the struct or its subtree. Hard constraints are applied whenever the enclosing struct is generated. For any keep constraint in a generated struct, the generator either meets the constraint or issues a constraint contradiction message. If the keep constraint appears under a when construct, the constraint is considered only if the when condition is true. |
| This is a Hard constraint : What this means is, you can not have contradicting constrains on a variable. Say keep a > 10; keep a < 5; |
| Example - keep |
1 <'
2 struct packet {
3 payload : list of byte;
4 // Hard constraint the legal packet size
5 keep payload.size() < 512 and payload.size() > 64;
6 };
keep all of {}
| A keep constraint block is exactly equivalent to a keep constraint for each constraint Boolean expression in the block. The all of block can be used as a constraint Boolean expression itself. |
| Example - keep all of {} |
1 <'
2 type transaction_kind: [VERSION1, VERSION2, VERSION3];
3 struct transaction {
4 kind: transaction_kind;
5 address: uint;
6 length: uint;
7 data: list of byte;
8
9 keep kind in [VERSION1, VERSION2] => all of {
10 length < 24;
11 data[0] == 0x9a;
12 address in [0x100..0x200];
13 };
14 };
15
16 extend sys {
17 tran : transaction;
18 run() is also {
19 for { var i : uint = 0; i < 2; i = i + 1} do {
20 gen tran;
21 print tran using hex;
22 };
23 };
24 };
25 '>
Compiler Output
tran = transaction-@0: transaction
---------------------------------------------- @constrain_gen_ex10
0 kind: VERSION1
1 address: 0x100
2 length: 0xf
3 data: (14 items)
tran = transaction-@1: transaction
---------------------------------------------- @constrain_gen_ex10
0 kind: VERSION3
1 address: 0x99759a6
2 length: 0xadc7f029
3 data: (36 items)
keep stuct-list.is_all_iterations()
This causes a list of structs to have all legal, non-contradicting iterations of the fields specified in the field list. Fields not included in the field list are not iterated; their values can be constrained by other relevant constraints. The highest value always occupies the last element in the list.
| Note : The number of iterations in a list produced by list.is_all_iterations() is the product of the number of possible values in each field in the list. |
Example - keep stuct-list.is_all_iterations()1 <'
2 type p_kind: [tx, rx];
3 type p_protocol: [atm, eth];
4 struct packet {
5 kind: p_kind;
6 protocol: p_protocol;
7 len: int [0..4k];
8 };
9 extend sys {
10 packets: list of packet;
11 keep packets.is_all_iterations(.kind,.protocol);
12 run() is also {
13 for each (lpacket) in packets {
14 print lpacket using hex;
15 };
16 };
17 };
18 '>
Compiler Output
lpacket = packet-@0: packet
---------------------------------------------- @constrain_gen_ex11
0 kind: tx
1 protocol: atm
2 len: 0x74
lpacket = packet-@1: packet
---------------------------------------------- @constrain_gen_ex11
0 kind: rx
1 protocol: atm
2 len: 0x9a9
lpacket = packet-@2: packet
---------------------------------------------- @constrain_gen_ex11
0 kind: tx
1 protocol: eth
2 len: 0x800
lpacket = packet-@3: packet
---------------------------------------------- @constrain_gen_ex11
0 kind: rx
1 protocol: eth
2 len: 0xed4
Bạn Có Đam Mê Với Vi Mạch hay Nhúng - Bạn Muốn Trau Dồi Thêm Kĩ Năng
Mong Muốn Có Thêm Cơ Hội Trong Công Việc
Và Trở Thành Một Người Có Giá Trị Hơn
Mong Muốn Có Thêm Cơ Hội Trong Công Việc
Và Trở Thành Một Người Có Giá Trị Hơn
Bạn Chưa Biết Phương Thức Nào Nhanh Chóng Để Đạt Được Chúng
Hãy Để Chúng Tôi Hỗ Trợ Cho Bạn. SEMICON
