Wednesday 13 February 2008

About generation of do-not-generate fields

Say a parent struct is having two fields inside it. One is an ungenerated (with do-not-generate sign) child struct and another ungenerated field is of pre defined data types (like uint, bool etc.).

When this parent struct is generated

1) ungenerated field of pre defined data types will get their initial value (0 for scalars, NULL for structs, empty list for lists).

2) ungenerated field whose value is a range (such as [0..100]) gets the first value in the range.

3) ungenerated field of user defined data types (like sturcts) will not be allocated and none of the fields in it will be generated.

Take a look at following code.

<'
struct child_s
{
!a : uint (bits: 4);
b : uint (bits: 4);
};
struct top_s
{
!child : child_s;
!x : uint (bits: 3);
!y : uint (bits: 3);
keep x in [2..5];
};
extend sys
{
top : top_s;
};
'>

In this example, top_s struct has one ungenerated struct and two ungenerated fields of uint (bits: 3). When top is generated inside the sys

1) y will be generated and will get any random value between 0 and 7

2) x will be generated with value of 2 as it is a range bound ungenerated field.

3) child field will not be generated as it is defined as ungenerated struct. So, the fields a and b of child struct will not be generated as well.

2 comments:

Unknown said...
This comment has been removed by the author.
Anonymous said...

The following lines are wrong.

1) y will be generated and will get any random value between 0 and 7

2) x will be generated with value of 2 as it is a range bound ungenerated field.

3) child field will not be generated as it is defined as ungenerated struct. So, the fields a and b of child struct will not be generated as well.



The correct stuff is any field which has ! in front of it will not be generated at any time when either of the stuct is generated. So y will be 0, x will be 0 too and Child will be Null.

Interesting thing is if you have constarint for generatable field which depends on non-generatable field, the generatable field can also get default (0 incase of uint) value.


Like if there is z in above example,

struct top_s
{
!child : child_s;
!x : uint (bits: 3);
!y : uint (bits: 3);
keep x in [2..5];

z : uint(bits :3);
keep z == y;
};

"Z" will also get 0 value.

Hope it makes this clear.