Skip to content

Commit 2ddef7b

Browse files
Copilotgebner
Copilot
and
gebner
authored
initial plan
Agent-Logs-Url: https://github.com/FStarLang/c2pulse/sessions/9442fd81-5e97-4ff4-a291-37a621de7e8f Co-authored-by: gebner <313929+gebner@users.noreply.github.com>
1 parent e3b33c3 commit 2ddef7b

2 files changed

Lines changed: 273 additions & 0 deletions

File tree

‎llvm.sh‎

Lines changed: 260 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,260 @@
1+
#!/bin/bash
2+
################################################################################
3+
# Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4+
# See https://llvm.org/LICENSE.txt for license information.
5+
# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6+
################################################################################
7+
#
8+
# This script will install the llvm toolchain on the different
9+
# Debian and Ubuntu versions
10+
11+
# This script is stored on:
12+
# https://github.com/opencollab/llvm-jenkins.debian.net/blob/master/llvm.sh
13+
14+
set -euxo pipefail
15+
16+
info() { printf "[info] %s\n" "$*"; }
17+
warn() { printf "[warn] %s\n" "$*" >&2; }
18+
# error MESSAGE [EXIT_CODE] — default exit code is 1
19+
error() {
20+
local msg="$1"
21+
local code="${2:-1}"
22+
printf "[error] %s\n" "$msg" >&2
23+
exit "$code"
24+
}
25+
26+
usage() {
27+
set +x
28+
echo "Usage: $0 [llvm_major_version] [all] [OPTIONS]" 1>&2
29+
echo -e "all\t\t\tInstall all packages." 1>&2
30+
echo -e "-n=code_name\t\tSpecifies the distro codename, for example bionic" 1>&2
31+
echo -e "-h\t\t\tPrints this help." 1>&2
32+
echo -e "-m=repo_base_url\tSpecifies the base URL from which to download." 1>&2
33+
exit 1;
34+
}
35+
36+
CURRENT_LLVM_STABLE=20
37+
BASE_URL="https://apt.llvm.org"
38+
39+
NEW_DEBIAN_DISTROS=("trixie" "forky" "unstable")
40+
# Set default values for commandline arguments
41+
# We default to the current stable branch of LLVM
42+
LLVM_VERSION=$CURRENT_LLVM_STABLE
43+
ALL=0
44+
DISTRO=$(lsb_release -is)
45+
VERSION_CODENAME=$(lsb_release -cs)
46+
VERSION=$(lsb_release -sr)
47+
UBUNTU_CODENAME=""
48+
CODENAME_FROM_ARGUMENTS=""
49+
# Obtain VERSION_CODENAME and UBUNTU_CODENAME (for Ubuntu and its derivatives)
50+
source /etc/os-release
51+
DISTRO=${DISTRO,,}
52+
53+
# Downloader abstraction: prefer wget, fall back to curl
54+
download_key() {
55+
local url="$1"
56+
if command -v wget &>/dev/null; then
57+
wget -qO- --retry-connrefused --waitretry=1 --tries=3 "$url"
58+
elif command -v curl &>/dev/null; then
59+
curl --proto '=https' --tlsv1.2 -sSf --retry 3 "$url"
60+
else
61+
error "Neither wget nor curl found. Install one and retry." 4
62+
fi
63+
}
64+
65+
check_url() {
66+
local url="$1"
67+
if command -v wget &>/dev/null; then
68+
wget -q --method=HEAD "$url" &>/dev/null
69+
elif command -v curl &>/dev/null; then
70+
curl --proto '=https' --tlsv1.2 -sSf --head --retry 2 "$url" >/dev/null 2>&1
71+
else
72+
return 1
73+
fi
74+
}
75+
76+
# Check if this is a new Debian distro
77+
is_new_debian=0
78+
if [[ "${DISTRO}" == "debian" ]]; then
79+
for new_distro in "${NEW_DEBIAN_DISTROS[@]}"; do
80+
if [[ "${VERSION_CODENAME}" == "${new_distro}" ]]; then
81+
is_new_debian=1
82+
break
83+
fi
84+
done
85+
fi
86+
87+
# Check for required tools
88+
needed_binaries=(lsb_release wget gpg)
89+
# add-apt-repository is not needed for newer Debian distros
90+
if [[ $is_new_debian -eq 0 ]]; then
91+
needed_binaries+=(add-apt-repository)
92+
fi
93+
94+
missing_binaries=()
95+
for binary in "${needed_binaries[@]}"; do
96+
if ! command -v "$binary" &>/dev/null; then
97+
if [[ "$binary" == "wget" ]] && command -v curl &>/dev/null; then
98+
continue
99+
fi
100+
missing_binaries+=("$binary")
101+
fi
102+
done
103+
104+
if [[ ${#missing_binaries[@]} -gt 0 ]] ; then
105+
error "Missing required tools: ${missing_binaries[*]}
106+
(hint: apt install lsb-release wget software-properties-common gnupg)
107+
curl is also supported as an alternative to wget" 4
108+
fi
109+
110+
case ${DISTRO} in
111+
debian)
112+
# Debian Forky has a workaround because of
113+
# https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1038383
114+
if [[ "${VERSION}" == "unstable" ]] || [[ "${VERSION}" == "testing" ]] || [[ "${VERSION_CODENAME}" == "forky" ]]; then
115+
CODENAME=unstable
116+
LINKNAME=
117+
else
118+
# "stable" Debian release
119+
CODENAME=${VERSION_CODENAME}
120+
LINKNAME=-${CODENAME}
121+
fi
122+
;;
123+
*)
124+
# ubuntu and its derivatives
125+
if [[ -n "${UBUNTU_CODENAME}" ]]; then
126+
CODENAME=${UBUNTU_CODENAME}
127+
if [[ -n "${CODENAME}" ]]; then
128+
LINKNAME=-${CODENAME}
129+
fi
130+
fi
131+
;;
132+
esac
133+
134+
# read optional command line arguments
135+
if [ "$#" -ge 1 ] && [ "${1::1}" != "-" ]; then
136+
if [ "$1" != "all" ]; then
137+
LLVM_VERSION=$1
138+
else
139+
# special case for ./llvm.sh all
140+
ALL=1
141+
fi
142+
OPTIND=2
143+
if [ "$#" -ge 2 ]; then
144+
if [ "$2" == "all" ]; then
145+
# Install all packages
146+
ALL=1
147+
OPTIND=3
148+
fi
149+
fi
150+
fi
151+
152+
while getopts ":hm:n:" arg; do
153+
case $arg in
154+
h)
155+
usage
156+
;;
157+
m)
158+
BASE_URL=${OPTARG}
159+
;;
160+
n)
161+
CODENAME=${OPTARG}
162+
if [[ "${CODENAME}" == "unstable" ]]; then
163+
# link name does not apply to unstable repository
164+
LINKNAME=
165+
else
166+
LINKNAME=-${CODENAME}
167+
fi
168+
CODENAME_FROM_ARGUMENTS="true"
169+
;;
170+
esac
171+
done
172+
173+
if [[ $EUID -ne 0 ]]; then
174+
error "This script must be run as root!"
175+
fi
176+
177+
declare -A LLVM_VERSION_PATTERNS
178+
LLVM_VERSION_PATTERNS[9]="-9"
179+
LLVM_VERSION_PATTERNS[10]="-10"
180+
LLVM_VERSION_PATTERNS[11]="-11"
181+
LLVM_VERSION_PATTERNS[12]="-12"
182+
LLVM_VERSION_PATTERNS[13]="-13"
183+
LLVM_VERSION_PATTERNS[14]="-14"
184+
LLVM_VERSION_PATTERNS[15]="-15"
185+
LLVM_VERSION_PATTERNS[16]="-16"
186+
LLVM_VERSION_PATTERNS[17]="-17"
187+
LLVM_VERSION_PATTERNS[18]="-18"
188+
LLVM_VERSION_PATTERNS[19]="-19"
189+
LLVM_VERSION_PATTERNS[20]="-20"
190+
LLVM_VERSION_PATTERNS[21]="-21"
191+
LLVM_VERSION_PATTERNS[22]="-22"
192+
LLVM_VERSION_PATTERNS[23]=""
193+
194+
if [ ! ${LLVM_VERSION_PATTERNS[$LLVM_VERSION]+_} ]; then
195+
error "This script does not support LLVM version $LLVM_VERSION" 3
196+
fi
197+
198+
LLVM_VERSION_STRING=${LLVM_VERSION_PATTERNS[$LLVM_VERSION]}
199+
200+
# join the repository name
201+
if [[ -n "${CODENAME}" ]]; then
202+
REPO_NAME="deb ${BASE_URL}/${CODENAME}/ llvm-toolchain${LINKNAME}${LLVM_VERSION_STRING} main"
203+
# check if the repository exists for the distro and version
204+
if ! check_url "${BASE_URL}/${CODENAME}"; then
205+
if [[ -n "${CODENAME_FROM_ARGUMENTS}" ]]; then
206+
error "Specified codename '${CODENAME}' is not supported by this script." 2
207+
else
208+
error "Distribution '${DISTRO}' in version '${VERSION}' is not supported by this script." 2
209+
fi
210+
fi
211+
fi
212+
213+
214+
# install everything
215+
216+
if [[ ! -f /etc/apt/trusted.gpg.d/apt.llvm.org.asc ]]; then
217+
GPG_KEY_URL="https://apt.llvm.org/llvm-snapshot.gpg.key"
218+
if ! check_url "$GPG_KEY_URL"; then
219+
error "GPG key not reachable at $GPG_KEY_URL" 2
220+
fi
221+
download_key "$GPG_KEY_URL" | tee /etc/apt/trusted.gpg.d/apt.llvm.org.asc
222+
fi
223+
224+
if [[ -z "`apt-key list 2> /dev/null | grep -i llvm`" ]]; then
225+
# Delete the key in the old format
226+
apt-key del AF4F7421 || true
227+
fi
228+
229+
230+
# Add repository based on distribution
231+
if [[ "${VERSION_CODENAME}" == "bookworm" ]]; then
232+
# add it twice to workaround:
233+
# https://github.com/llvm/llvm-project/issues/62475
234+
add-apt-repository -y "${REPO_NAME}"
235+
add-apt-repository -y "${REPO_NAME}"
236+
elif [[ $is_new_debian -eq 1 ]]; then
237+
# workaround missing add-apt-repository in newer Debian and use new source.list format
238+
SOURCES_FILE="/etc/apt/sources.list.d/http_apt_llvm_org_${CODENAME}_-${VERSION_CODENAME}.sources"
239+
TEXT_TO_ADD="Types: deb
240+
Architectures: amd64 arm64
241+
Signed-By: /etc/apt/trusted.gpg.d/apt.llvm.org.asc
242+
URIs: ${BASE_URL}/${CODENAME}/
243+
Suites: llvm-toolchain${LINKNAME}${LLVM_VERSION_STRING}
244+
Components: main"
245+
echo "$TEXT_TO_ADD" | tee -a "$SOURCES_FILE" > /dev/null
246+
else
247+
add-apt-repository -y "${REPO_NAME}"
248+
fi
249+
250+
apt-get update
251+
PKG="clang-$LLVM_VERSION lldb-$LLVM_VERSION lld-$LLVM_VERSION clangd-$LLVM_VERSION"
252+
if [[ $ALL -eq 1 ]]; then
253+
# same as in test-install.sh
254+
# No worries if we have dups
255+
PKG="$PKG clang-tidy-$LLVM_VERSION clang-format-$LLVM_VERSION clang-tools-$LLVM_VERSION llvm-$LLVM_VERSION-dev lld-$LLVM_VERSION lldb-$LLVM_VERSION llvm-$LLVM_VERSION-tools libomp-$LLVM_VERSION-dev libc++-$LLVM_VERSION-dev libc++abi-$LLVM_VERSION-dev libclang-common-$LLVM_VERSION-dev libclang-$LLVM_VERSION-dev libclang-cpp$LLVM_VERSION-dev liblldb-$LLVM_VERSION-dev libunwind-$LLVM_VERSION-dev"
256+
if test $LLVM_VERSION -gt 14; then
257+
PKG="$PKG libclang-rt-$LLVM_VERSION-dev libpolly-$LLVM_VERSION-dev"
258+
fi
259+
fi
260+
apt-get install -y $PKG

‎test/assert_order.c‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include "c2pulse.h"
2+
#include <assert.h>
3+
#include <stdint.h>
4+
5+
/* C assert is translated to Pulse assert (with_pure ...) */
6+
int32_t checked_add2(int32_t a, int32_t b)
7+
_requires(a >= 0 && a < 1000 && b >= 0 && b < 1000)
8+
_ensures(return == a + b)
9+
{
10+
int32_t result = a + b;
11+
assert(result >= 0);
12+
return result;
13+
}

0 commit comments

Comments
 (0)