| |
|
|
|
|
|
| |
|
|
| |
 |
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 };
You could download file constrain_gen_ex9.e here
|
| |
|
|
| |
|
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 '>
You could download file constrain_gen_ex10.e here
|
| |
|
|
| |
|
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 '>
You could download file constrain_gen_ex11.e here
|
| |
|
|
| |
|
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
|
| |
|
|
| |
|
keep soft
|
|
|
This suggests default values for fields or variables in the struct or its subtree, or describes suggested relationships between field values and other items in the struct or its subtree. The following restrictions apply. |
| |
|
|
|
|
- Soft constraints are order dependent and shall not be met if they conflict with hard constraints or soft constraints that have already been applied.
- The soft keyword cannot be used in compound Boolean expressions.
- Individual constraints inside a constraint block can be soft constraints.
- Because soft constraints only suggest default values, it is better not to use them to define architectural constraints.
|
| |
|
|
|
|
|
| |
|
|
| |
|
Example - keep soft
|
| |
|
|
|
|
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 // Set the default packet size
7 keep soft payload.size == 64;
8 };
You could download file constrain_gen_ex12.e here
|
| |
|
|
| |
|
keep soft select
|
|
|
Specifies the relative probability that a particular value or set of values is chosen from the current range of legal values. The current range is the range of values as reduced by hard constraints and by soft constraints that have already been applied. |
| |
|
|
|
|
A weighted value will be assigned with the probability of weight/(sum of all weights) |
| |
|
|
|
|
Weights are treated as integers. If you use an expression for a weight, take care to avoid a situation where the value of the expression is larger than the maximum integer size (MAX_INT). Like other soft constraints, keep soft select is order dependent and will not be met if it conflicts with hard constraints or soft constraints that have already been applied. |
| |
|
|
| |
|
Example - keep soft select
|
| |
|
|
|
|
1 <'
2 struct transaction {
3 address: uint;
4 keep soft address == select {
5 10: [0..49]; // 10 %
6 60: 50; // 60 %
7 30: [51..99];// 30 %
8 };
9 };
10
11 extend sys {
12 tra : transaction;
13 run() is also {
14 for {var i : uint = 0; i < 4; i = i +1} do {
15 gen tra;
16 print tra;
17 };
18 };
19 };
20 '>
You could download file constrain_gen_ex13.e here
|
| |
|
|
| |
|
Compiler Output
|
| |
|
|
|
|
tra = transaction-@0: transaction
---------------------------------------------- @constrain_gen_ex13
0 address: 50
tra = transaction-@1: transaction
---------------------------------------------- @constrain_gen_ex13
0 address: 50
tra = transaction-@2: transaction
---------------------------------------------- @constrain_gen_ex13
0 address: 50
tra = transaction-@3: transaction
---------------------------------------------- @constrain_gen_ex13
0 address: 53
|
| |
|
|
| |
|
keep gen before
|
|
|
Modify the generation order, This requires the generatable items specified in the first list to be generated before the items specified in the second list. This constraint can be used to influence the distribution of values by preventing soft value constraints from being consistently skipped. The following restrictions also apply. |
| |
|
|
|
|
- This constraint itself can cause constraint cycles. If a constraint cycle involving one of the fields in the keep gen ... before constraint exists and if the resolve_cycles generation configuration option is TRUE, the constraint can be ignored if the program cannot satisfy both it and other constraints that conflict with it.
- This constraint cannot appear on the left-hand side of a implication operator (=>).
|
| |
|
|
| |
|
Example - keep gen before
|
| |
|
|
|
|
1 <'
2 struct packet {
3 good: bool;
4 length: byte [1..24];
5 data [length]: list of byte;
6 crc: uint;
7 keep good => crc == crc_calc();
8 keep gen (length, data) before (crc);
9 keep soft good == TRUE;
10
11 crc_calc() : uint is {
12 result = pack(packing.low,length,data).crc_32(0,length);
13 };
14 };
15
16 extend sys {
17 p: list of packet;
18 keep soft p.size() == 4;
19 run() is also {
20 print p;
21 };
22 };
23 '>
You could download file constrain_gen_ex14.e here
|
| |
|
|
| |
|
Compiler Output
|
| |
|
|
|
|
p =
item type good length data crc
---------------------------------------------------------------------------
0. packet TRUE 6 (6 items) 3611186507
1. packet TRUE 23 (23 items) 962437978
2. packet TRUE 1 (1 items) 4233967285
3. packet TRUE 21 (21 items) 3009106740
|
| |
|
|
| |
|
keep soft gen before
|
|
|
This modifies the soft generation order by recommending the fields specified in the first field list be generated before the fields specified in the second field list. This soft generation order is second in priority to the hard generation order created by dependencies between parameters and keep gen before constraints. This constraint can be used to suggest a generation order which is later overridden in individual tests with a hard order constraint. This constraint cannot appear on the left-hand side of a implication operator (=>). |
| |
|
|
| |
|
Example - keep soft gen before
|
| |
|
|
|
|
1 <'
2 struct transaction {
3 address: uint;
4 length: uint [1..10];
5 keep length == 5 => address < 50;
6 keep soft gen (length) before (address);
7 };
8 '>
You could download file constrain_gen_ex15.e here
|
| |
|
|
| |
|
keep gen_before_subtypes()
|
|
|
To speed up generation of structs with multiple when subtypes, this type of constraint, called a subtype optimization constraint, causes the generator engine to wait until a when determinant value is generated for a specified field before it analyzes constraints and generates fields under the when subtype. |
| |
|
|
|
|
When no subtype optimization constraints are present in a struct, the generator analyzes all of the constraints and fields in the struct before it generates the struct, even those constraints and fields that are defined under when subtypes. When a subtype optimization constraint is present, the generator initially analyzes only the constraints and fields of the base struct type. When a subtype optimization when determinant is encountered, the generator analyzes the associated when subtype and then generates it. |
| |
|
|
| |
|
Example - keep gen_before_subtypes()
|
| |
|
|
|
|
1 <'
2 type format_t: [FMT_A, FMT_B, FMT_C];
3 struct instr_s {
4 intrpt: bool;
5 format: format_t;
6 keep gen_before_subtypes(format);
7 keep format == FMT_A => intrpt ! = FALSE;
8 when FMT_A'format instr_s {
9 a_intrp: bool;
10 keep intrpt ! = a_intrp;
11 keep gen (size) before (offset);
12 keep offset == 0x10;
13 };
14 when FMT_B'format instr_s {
15 b_intrp: bool;
16 keep intrpt == TRUE;
17 };
18 offset: int;
19 size: int;
20 };
21
22 extend sys {
23 inst : list of instr_s;
24 keep inst.size() == 4;
25 run() is also {
26 print inst using hex;
27 };
28 };
29 '>
You could download file constrain_gen_ex16.e here
|
| |
|
|
| |
|
Compiler Output
|
| |
|
|
|
|
inst =
item type intrpt format FMT_A'for* FMT_B'for* offset
---------------------------------------------------------------------------
0. instr_s TRUE FMT_B FALSE 0x84ce79e0
1. instr_s TRUE FMT_B FALSE 0x237340d
2. instr_s TRUE FMT_C 0x69352a90
3. instr_s TRUE FMT_B TRUE 0x3dfde23c
|
| |
|
|
| |
|
|
| |
|
|
|
|
|
| |
|
|
