impl/fs/bilby/quickcheck/fsm_example/alloc.ac

/*
 * Copyright 2016, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(NICTA_GPL)
 */

#define GEN_ALLOC(TYPE) \
$ty:(R (SysState, TYPE) SysState) $id:(new##TYPE)($ty:(SysState) ex) \
{ \
	$ty:(R (SysState, TYPE) SysState) ret; \
        ret.Success.p2 = kmalloc(sizeof(*ret.Success.p2)); \
 \
	if (ret.Success.p2 == NULL) { \
		ret.tag = TAG_ENUM_Error; \
		ret.Error = ex; \
	} else { \
                ret.tag = TAG_ENUM_Success; \
                ret.Success.p1 = ex; \
	} \
	return ret; \
} \
 \
$ty:(SysState) $id:(free##TYPE)($ty:((SysState, TYPE)) args) \
{ \
	kfree(args.p2); \
	return args.p1; \
}

GEN_ALLOC(FsState)
GEN_ALLOC(BilbyFsReaddirContext)
GEN_ALLOC(FsmState)
GEN_ALLOC(ObjSummary)
GEN_ALLOC(ObjDentry)
GEN_ALLOC(ObjDentarr)
GEN_ALLOC(ObjSuper)
GEN_ALLOC(ObjInode)
GEN_ALLOC(Obj)
GEN_ALLOC(MountState)
GEN_ALLOC(FsopState)
GEN_ALLOC(OstoreState)
GEN_ALLOC(UbiVolInfo)
GEN_ALLOC(UbiDevInfo)
GEN_ALLOC(VfsInode)
GEN_ALLOC(Buffer)
/*
$ty:(R (SysState, FsState') SysState) $id:(newFsState')($ty:(SysState) ex) 
{ 
	$ty:(R (SysState, FsState') SysState) ret; 
        ret.Success.p2 = kmalloc(sizeof(*ret.Success.p2)); 
 
	if (ret.Success.p2 == NULL) { 
		ret.tag = TAG_ENUM_Error; 
		ret.Error = ex; 
	} else { 
                ret.tag = TAG_ENUM_Success; 
                ret.Success.p1 = ex; 
	} 
	return ret; 
} 
*/
 
$ty:(SysState) $id:(freeFsState2)($ty:((SysState, FsState')) args) 
{ 
	kfree(args.p2); 
	return args.p1; 
}

#define GEN_PTYPE_ALLOC(TYPE, PARAMS) \
$ty:(R (SysState, TYPE PARAMS) SysState) $id:(new##TYPE)($ty:(SysState) ex) \
{ \
	$ty:(R (SysState, TYPE PARAMS) SysState) ret; \
        ret.Success.p2 = kmalloc(sizeof(*ret.Success.p2)); \
 \
	if (ret.Success.p2 == NULL) { \
		ret.tag = TAG_ENUM_Error; \
		ret.Error = ex; \
	} else { \
                ret.tag = TAG_ENUM_Success; \
                ret.Success.p1 = ex; \
	} \
	return ret; \
} \
 \
$ty:(SysState) $id:(free##TYPE)($ty:((SysState, TYPE PARAMS)) args) \
{ \
	kfree(args.p2); \
	return args.p1; \
}

GEN_PTYPE_ALLOC(RbtNode, k v)
GEN_PTYPE_ALLOC(ListNode, a)

$ty:(R (SysState, WordArray a) SysState) $id:wordarray_create($ty:((SysState, U32)) args) {
	$ty:(SysState) ex = args.p1;
	u32 size = args.p2;
	$ty:(R (SysState, WordArray a) SysState) ret;

	$ty:(WordArray a) array = kmalloc(sizeof(*array));

	if (array == NULL || !size) {
		ret.tag = TAG_ENUM_Error;
		ret.Error = ex;
	} else {
		array->values = kzalloc(size * sizeof (*(array->values)));
		if (array->values == NULL) {
			kfree(array);
			ret.tag = TAG_ENUM_Error;
			ret.Error = ex;
		} else {
			array->len = size;

			ret.tag = TAG_ENUM_Success;
			ret.Success.p1 = ex;
			ret.Success.p2 = array;
		}
	}
	return ret;
}

$ty:(SysState) $id:wordarray_free($ty:((SysState, WordArray a)) args)
{
	$ty:(WordArray a) array = args.p2;

	if (array->values)
		kfree(array->values);
	kfree(array);

	return args.p1;
}

$ty:(R (SysState, Array a) SysState) $id:array_create($ty:((SysState, U32)) args)
{
	$ty:(R ((SysState, Array a)) SysState) ret;
	$ty:(Array a) array = kmalloc(sizeof(*array));
	u32 size = args.p2;

	if (array == NULL || !size) {
		ret.tag = TAG_ENUM_Error;
		ret.Error = args.p1;
	} else {
		array->values = kzalloc(size * sizeof(*(array->values)));
		if (array->values == NULL) {
			kfree(array);
			ret.tag = TAG_ENUM_Error;
			ret.Error = args.p1;
		} else {
			array->len = size;

			ret.tag = TAG_ENUM_Success;
			ret.Success.p1 = args.p1;
			ret.Success.p2 = array;
		}
	}
	return ret;
}

$ty:(SysState) $id:array_free($ty:(ArrayFreeP a) args) {
        int i;

        if (args.arr->values) {
            for (i = 0; i < args.arr->len; i++) {
                $ty:((SysState, a)) fargs;

                fargs.p1 = args.ex;
                fargs.p2 = args.arr->values[i];
                
                if (fargs.p2)
                    (($spec:(FreeF a)) args.f) (fargs);
            }
            kfree(args.arr->values);
        }
        kfree(args.arr);
        return args.ex;
}

$ty:(RbtNode ObjId GimNode) $id:idx_to_gim_node($ty:(RbtNode ObjId ObjAddr) node)
{
    return ($ty:(RbtNode ObjId GimNode)) node;
}