| /* |

| * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) |

| * |

| * SPDX-License-Identifier: BSD-2-Clause |

| */ |

| |

| /* Framework for running experiments related to CNode size calculations. |

| * |

| * Rather than having a universal, hard coded size for CNodes, CAmkES infers |

| * the size of a CNode after doing cap allocation by calculating the minimum |

| * size it can be while still fitting its contained caps. This calculation |

| * needs to exist in two different places: in Python for the CAmkES |

| * implementation and in Isabelle/HOL for the label mapping verification. The |

| * Isabelle/HOL version is defined in a non-executable manner because this is |

| * more natural, but the Python version obviously needs to be executable. As a |

| * result, there can be some doubt that the two always return the same answer. |

| * |

| * The following program enumerates all valid inputs for both and ensures they |

| * match. You can use this as a sandbox for trying out modifications to either |

| * algorithm. If you're wondering why this is written in C, this was originally |

| * a Python program but did not run at sufficient speed to enumerate all inputs |

| * in a reasonable time. |

| * |

| * To compile: |

| * |

| * cc -O3 -W -Wall -Wextra -std=c11 cnode-size-playground.c -lm |

| */ |

| |

| #include <assert.h> |

| #include <math.h> |

| #include <stdio.h> |

| |

| /* This function is intended to match the semantics of |

| * python-capdl/capdl/Object.py:calculate_cnode_size |

| */ |

| static int calculate_cnode_size(int max_slot) { |

| assert(max_slot >= 0); |

| int s = max_slot; |

| if (s < 2) |

| s = 2; |

| double base = log2((double)s); |

| s = (int)floor(base) + 1; |

| return s; |

| } |

| |

| /* This function is intended to match the semantics of |

| * l4v/camkes/cdl-refine/Generator_CAMKES_CDL.thy:cnode_size_bits |

| */ |

| static int cnode_size_bits(int max_slot) { |

| int s = max_slot; |

| if (max_slot < 3) |

| s = 3; |

| for (int i = 0; i <= 28; i++) |

| if (1 << i > s) |

| return i; |

| return -1; |

| } |

| |

| int main(void) { |

| for (int i = 0; i < (1 << 28) - 1; i++) { |

| int size1 = calculate_cnode_size(i); |

| int size2 = cnode_size_bits(i); |

| if (size1 != size2) { |

| fprintf(stderr, "failed for %d\n" |

| " calculate_cnode_size(%d) == %d\n" |

| " cnode_size_bits(%d) == %d\n", |

| i, i, size1, i, size2); |

| return -1; |

| } |

| } |

| return 0; |

| } |