cn-pKVM-hyp-allocator/verify.sh at main · rems-project/cn-pKVM-hyp-allocator · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
#!/bin/bash

JOBS=${1:-1}

targets=(
  min_u32
  min_u64
  max_u64
  list_empty
  INIT_LIST_HEAD
  list_is_first
  list_is_last
  __list_del
  __list_del_entry
  list_del
  chunk_unmapped_size
  setup_first_chunk
  chunk_inc_map
  list_add
  __list_add
  chunk_get_next
  chunk_can_split
  chunk_hash_update
  chunk_hash_compute
  chunk_hash_validate
  chunk_addr_fixup
  chunk_get
  __chunk_next
  chunk_get_prev
  __chunk_prev
  LemmaNextChunk
  LemmaPrevChunk
  chunk_list_insert
  LemmaCreateNewChunk
  LemmaCreateNewChunkAux
  LemmaSplitAndNewChunk
  chunk_needs_mapping
  chunk_install
  get_free_chunk
  chunk_recycle
  hyp_alloc
  LemmaGetLastChunk
  LemmaLsegToChunkHdrs
  LemmaConcatCnChunkHdrsRev
  LemmaCnChunkHdrsRevToCnChunkHdrs
  LemmaCnChunkHdrsRevToCnHypAllocator
  LemmaPtrToU64
  LemmaU64ToPtr
  LemmaTurnU32sToU64
  LemmaTurnU64ToU32s
  hyp_alloc_init
  pkvm_alloc_private_va_range
  LemmaMergeChunk
  LemmaMergeArrays
  chunk_merge
  chunk_list_del
  hyp_free
  hyp_alloc_errno
  hyp_alloc_missing_donations
  chunk_destroyable
  chunk_reclaimable
  hyp_alloc_size
)

OPT="${OPT:-"-p 20"}"
run_test() {
  target="$1"
  start=$(date +%s.%N)

  if make ONLY="$target" cn-verify OPT="$OPT" > "verify-${target}.log" 2>&1  &&
     grep -q "\[1/1\]: $target -- pass" "verify-${target}.log"; then
    status="passed"
  else
    if grep -q "\[1/1\]: $target -- pass" "verify-${target}.log"; then
      status="failed verification"
    else
      status="failed"
    fi
  fi

  end=$(date +%s.%N)
  elapsed=$(echo "$end - $start" | bc)

  RED='\033[0;31m'
  GREEN='\033[0;32m'
  NC='\033[0m'

  if [[ $status == "passed" ]]; then
    echo -e "$target ${GREEN}$status${NC} (in ${elapsed}s)"
  else
    echo -e "$target ${RED}$status${NC} (in ${elapsed}s)"
  fi

  [[ $status != "passed" ]] && exit 1
}

date
git log -1 --format="%H"
cn --version
echo "option: --incremental-solving=false --disable-multiclause-predicate-unfolding --no-vip $OPT"

export -f run_test

printf "%s\n" "${targets[@]}" | xargs -n1 -P "$JOBS" bash -c 'run_test "$@"' _