Skip to content

Commit 2f8a9b1

Browse files
eupharinaresistor
authored andcommitted
[CHERI_CSA] CHERI API Modelling
1 parent 8e7a103 commit 2f8a9b1

File tree

3 files changed

+98
-0
lines changed

3 files changed

+98
-0
lines changed

clang/include/clang/StaticAnalyzer/Checkers/Checkers.td

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1794,6 +1794,10 @@ def UncheckedLocalVarsChecker : Checker<"UncheckedLocalVarsChecker">,
17941794

17951795
let ParentPackage = CHERI in {
17961796

1797+
def CheriAPIModelling : Checker<"CheriAPIModelling">,
1798+
HelpText<"Model CheriAPI">,
1799+
Documentation<NotDocumented>;
1800+
17971801
def ProvenanceSourceChecker
17981802
: Checker<"ProvenanceSource">,
17991803
HelpText<"Check expressions with ambiguous provenance source.">,
Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
//===-- AllocationChecker.cpp - Allocation Checker -*- C++ -*--------------===//
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+
//
9+
// Model CHERI API
10+
//
11+
//===----------------------------------------------------------------------===//
12+
13+
#include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
14+
#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
15+
#include "clang/StaticAnalyzer/Core/Checker.h"
16+
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
17+
#include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
18+
#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
19+
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
20+
#include <clang/StaticAnalyzer/Core/PathSensitive/CallDescription.h>
21+
22+
using namespace clang;
23+
using namespace ento;
24+
25+
// namespace {
26+
27+
class CheriAPIModelling : public Checker<eval::Call> {
28+
public:
29+
bool evalCall(const CallEvent &Call, CheckerContext &C) const;
30+
31+
typedef void (CheriAPIModelling::*FnCheck)(CheckerContext &,
32+
const CallExpr *) const;
33+
CallDescriptionMap<FnCheck> Callbacks = {
34+
{{CDM::SimpleFunc, {"cheri_address_set"}, 2},
35+
&CheriAPIModelling::evalAddrSet},
36+
{{CDM::SimpleFunc, {"cheri_bounds_set"}, 2},
37+
&CheriAPIModelling::evalBoundsSet},
38+
{{CDM::SimpleFunc, {"cheri_bounds_set_exact"}, 2},
39+
&CheriAPIModelling::evalBoundsSet},
40+
{{CDM::SimpleFunc, {"cheri_perms_and"}, 2},
41+
&CheriAPIModelling::evalBoundsSet},
42+
{{CDM::SimpleFunc, {"cheri_tag_clear"}, 1},
43+
&CheriAPIModelling::evalBoundsSet}
44+
45+
};
46+
47+
void evalBoundsSet(CheckerContext &C, const CallExpr *CE) const;
48+
void evalAddrSet(CheckerContext &C, const CallExpr *CE) const;
49+
};
50+
51+
//} // namespace
52+
53+
void CheriAPIModelling::evalBoundsSet(CheckerContext &C,
54+
const CallExpr *CE) const {
55+
auto State = C.getState();
56+
SVal Cap = C.getSVal(CE->getArg(0));
57+
State = State->BindExpr(CE, C.getLocationContext(), Cap);
58+
C.addTransition(State);
59+
}
60+
61+
void CheriAPIModelling::evalAddrSet(CheckerContext &C,
62+
const CallExpr *CE) const {
63+
auto State = C.getState();
64+
SVal Addr = C.getSVal(CE->getArg(1));
65+
State = State->BindExpr(CE, C.getLocationContext(), Addr);
66+
C.addTransition(State);
67+
}
68+
69+
bool CheriAPIModelling::evalCall(const CallEvent &Call,
70+
CheckerContext &C) const {
71+
const auto *CE = dyn_cast_or_null<CallExpr>(Call.getOriginExpr());
72+
if (!CE)
73+
return false;
74+
75+
const FnCheck *Handler = Callbacks.lookup(Call);
76+
if (!Handler)
77+
return false;
78+
79+
(this->**Handler)(C, CE);
80+
return true;
81+
}
82+
83+
//===----------------------------------------------------------------------===//
84+
// Checker registration.
85+
//===----------------------------------------------------------------------===//
86+
87+
void clang::ento::registerCheriAPIModelling(CheckerManager &Mgr) {
88+
Mgr.registerChecker<CheriAPIModelling>();
89+
}
90+
91+
bool clang::ento::shouldRegisterCheriAPIModelling(const CheckerManager &Mgr) {
92+
return true;
93+
}

clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ add_clang_library(clangStaticAnalyzerCheckers
2727
CheckerDocumentation.cpp
2828
CHERI/AllocationChecker.cpp
2929
CHERI/CapabilityCopyChecker.cpp
30+
CHERI/CheriAPIModelling.cpp
3031
CHERI/CHERIUtils.cpp
3132
CHERI/PointerSizeAssumptionsChecker.cpp
3233
CHERI/ProvenanceSourceChecker.cpp

0 commit comments

Comments
 (0)