Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Valentin Touzeau
lrusecurity
Commits
cc0398b3
Commit
cc0398b3
authored
Jan 22, 2019
by
Maeva Ramarjiaona
Browse files
starting to figure out how to connect my analysis with the rest
parent
dadf7271
Changes
7
Hide whitespace changes
Inline
Side-by-side
include/lrusecurity/features.h
View file @
cc0398b3
#ifndef LRU
MC
_FEATURES_H_
#define LRU
MC
_FEATURES_H_
#ifndef LRU
SECURITY
_FEATURES_H_
#define LRU
SECURITY
_FEATURES_H_
#include <string>
...
...
@@ -8,104 +8,22 @@
#include <otawa/proc/AbstractFeature.h>
#include <otawa/icat3/features.h>
namespace
lru
mc
{
namespace
lru
security
{
// Exist-Hit
extern
otawa
::
p
::
feature
EXIST_HIT_ANALYSIS_FEATURE
;
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_HIT_INIT
;
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_HIT_IN
;
// Exist-Miss
extern
otawa
::
p
::
feature
EXIST_MISS_ANALYSIS_FEATURE
;
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_MISS_INIT
;
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_MISS_IN
;
// Definitely Unknown
enum
class
DUCategory
{
NC
,
EH
,
EM
,
DU
};
extern
otawa
::
p
::
feature
DU_CATEGORY_FEATURE
;
extern
otawa
::
p
::
id
<
DUCategory
>
DU_CATEGORY
;
// Model Checking Refinement Category
enum
class
RefinementCategory
{
CLASSIFIED
,
AH_CANDIDATE
,
AM_CANDIDATE
,
AH_AM_CANDIDATE
};
extern
otawa
::
p
::
feature
REFINEMENT_CATEGORY_FEATURE
;
//hook: access
extern
otawa
::
p
::
id
<
RefinementCategory
>
REFINEMENT_CATEGORY
;
// MC Program Model Building
class
MCProgramModel
;
extern
otawa
::
p
::
feature
PROGRAM_MODEL_BUILDING_FEATURE
;
//hook: access
extern
otawa
::
p
::
id
<
MCProgramModel
*>
PROGRAM_MODEL
;
//hook: workspace
extern
otawa
::
p
::
id
<
MCProgramModel
*>
GLOBAL_MODEL
;
//hook: LBlockSet
extern
otawa
::
p
::
feature
SET_SLICING_PROGRAM_MODEL_FEATURE
;
extern
otawa
::
p
::
id
<
elm
::
AllocArray
<
MCProgramModel
*>
>
SET_SLICED_PROGRAM_MODEL
;
//hook: LBlock
extern
otawa
::
p
::
feature
LBLOCK_SLICING_PROGRAM_MODEL_FEATURE
;
extern
otawa
::
p
::
id
<
elm
::
AllocArray
<
elm
::
AllocArray
<
MCProgramModel
*>
>
>
LBLOCK_SLICED_PROGRAM_MODEL
;
// MC Program Model Slicing
enum
class
ProgramSlicing
{
SET_SLICING
,
CACHE_BLOCK_SLICING
,
ACCESS_SLICING
};
extern
otawa
::
p
::
id
<
ProgramSlicing
>
PROGRAM_SLICING
;
// MC Cache Model Building
enum
class
CacheModelKind
{
YOUNGER_SET
,
YOUNGER_SET_BOUNDED_BITVECTOR
,
YOUNGER_SET_BITVECTOR
,
YOUNGER_SET_CLOSED_BITVECTOR
,
MAP_BLOCK_AGE
,
QUEUE
};
extern
otawa
::
p
::
id
<
CacheModelKind
>
CACHE_MODEL_KIND
;
// Model Checking Analysis
extern
otawa
::
p
::
feature
MODEL_CHECKING_ANALYSIS_FEATURE
;
extern
otawa
::
p
::
id
<
elm
::
String
>
NUXMV_PATH
;
extern
otawa
::
p
::
id
<
elm
::
String
>
NUXMV_WORKSPACE_PATH
;
// Classification printing
extern
otawa
::
p
::
id
<
bool
>
CLASSIFICATION_TO_FILE
;
extern
otawa
::
p
::
id
<
elm
::
sys
::
Path
>
CLASSIFICATION_PATH
;
}
// namespace lru
mc
}
// namespace lru
security
namespace
otawa
{
template
<
>
void
from_string
(
const
elm
::
string
&
s
,
lrumc
::
CacheModelKind
&
v
);
template
<
>
void
from_string
(
const
elm
::
string
&
s
,
lrumc
::
ProgramSlicing
&
v
);
}
// namespace otawa
#endif // LRUMC_FEATURES_H
src/ACSSecurity.h
View file @
cc0398b3
...
...
@@ -10,6 +10,7 @@ namespace lrusecurity
public
class
ACSSecurity
:
class
otawa
::
icat3
::
ACS
{
public:
ACSSecurity
(
icat3
::
ACS
acs
);
otawa
::
Bag
<
icache
::
Access
>
_prev
;
}
...
...
src/Prev/ExistHitPrevAnalysis.h
View file @
cc0398b3
#ifndef LRU
MC
_EXIST_HIT_ANALYSIS_H_
#define LRU
MC
_EXIST_HIT_ANALYSIS_H_
#ifndef LRU
SECURITY
_EXIST_HIT_ANALYSIS_H_
#define LRU
SECURITY
_EXIST_HIT_ANALYSIS_H_
#include <otawa/proc/Processor.h>
#include <otawa/icat3/features.h>
#include <otawa/cfg/features.h>
namespace
lru
mc
namespace
lru
security
{
class
ExistHitAnalysis
:
public
otawa
::
Processor
class
ExistHit
Prev
Analysis
:
public
otawa
::
Processor
{
public:
static
otawa
::
p
::
declare
reg
;
...
...
@@ -32,31 +32,31 @@ private:
/**
* Perform the ACS analysis for the Exist-Hit domain. For cache block, it associates an upper bound on block age that holds on at least on path
* @par Properties
* @li @ref EXIST_HIT_IN
* @li @ref EXIST_HIT_
PREV_
IN
*
* @par Configuraiton
* @li @ref EXIST_HIT_INIT
* @li @ref EXIST_HIT_
PREV_
INIT
*
* @par Implementation
* @li @ref ExistHitAnalysis
* @li @ref ExistHit
Prev
Analysis
*
* @ingroup lru
mc
* @ingroup lru
security
*/
extern
otawa
::
p
::
feature
EXIST_HIT_ANALYSIS_FEATURE
;
extern
otawa
::
p
::
feature
EXIST_HIT_
PREV_
ANALYSIS_FEATURE
;
/**
* ACS for the Exist-Hit analysis at the entry of the corresponding block or edge.
*
* @par Feature
* @li @ref EXIST_HIT_ANALYSIS_FEATURE
* @li @ref EXIST_HIT_ANALYSIS_
PREV_
FEATURE
*
* @par Hooks
* @li @ref Block
* @li @ref Edge
*
* @ingroup lru
mc
* @ingroup lru
security
*/
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_HIT_IN
;
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_HIT_
PREV_
IN
;
/**
...
...
@@ -66,12 +66,12 @@ extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_IN;
* @li Feature configuration.
*
* @par Feature
* @li @ref EXIST_HIT_ANALYSIS_FEATURE
* @li @ref EXIST_HIT_ANALYSIS_
PREV_
FEATURE
*
* @ingroup lru
mc
* @ingroup lru
security
*/
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_HIT_INIT
;
extern
otawa
::
p
::
id
<
otawa
::
icat3
::
Container
<
otawa
::
icat3
::
ACS
>
>
EXIST_HIT_
PREV_
INIT
;
};
// namespace lru
mc
};
// namespace lru
security
#endif // LRU
MC
_EXIST_HIT_ANALYSIS_H_
#endif // LRU
SECURITY
_EXIST_HIT_ANALYSIS_H_
src/Prev/lrusecurity_ExistHitPrevAnalysis.cpp
View file @
cc0398b3
...
...
@@ -90,13 +90,13 @@ p::declare ExistHitPrevAnalysis::reg = p::init("lrusecurity::ExistHitPrevAnalysi
.
require
(
COLLECTED_CFG_FEATURE
)
.
require
(
icat3
::
MUST_PERS_ANALYSIS_FEATURE
)
.
require
(
icat3
::
CATEGORY_FEATURE
)
.
provide
(
EXIST_HIT_ANALYSIS_FEATURE
)
.
provide
(
EXIST_HIT_
PREV_
ANALYSIS_FEATURE
)
.
make
<
ExistHitPrevAnalysis
>
();
p
::
feature
EXIST_HIT_ANALYSIS_FEATURE
(
"lrusecurity::EXIST_HIT_ANALYSIS_FEATURE"
,
p
::
make
<
ExistHitPrevAnalysis
>
());
p
::
feature
EXIST_HIT_
PREV_
ANALYSIS_FEATURE
(
"lrusecurity::EXIST_HIT_
PREV_
ANALYSIS_FEATURE"
,
p
::
make
<
ExistHitPrevAnalysis
>
());
p
::
id
<
icat3
::
Container
<
icat3
::
ACS
>
>
EXIST_HIT_IN
(
"lrusecurity::EXIST_HIT_IN"
);
p
::
id
<
icat3
::
Container
<
icat3
::
ACS
>
>
EXIST_HIT_
PREV_
IN
(
"lrusecurity::EXIST_HIT_
PREV_
IN"
);
p
::
id
<
icat3
::
Container
<
icat3
::
ACS
>
>
EXIST_HIT_INIT
(
"lrusecurity::EXIST_HIT_INIT"
);
p
::
id
<
icat3
::
Container
<
icat3
::
ACS
>
>
EXIST_HIT_
PREV_
INIT
(
"lrusecurity::EXIST_HIT_
PREV_
INIT"
);
};
// namespace lrusecurity
src/ProcessorExample.h
deleted
100644 → 0
View file @
dadf7271
#ifndef LRUSECURITY_PROCESSOR_EXAMPLE_H_
#define LRUSECURITY_PROCESSOR_EXAMPLE_H_
#include <otawa/proc/Processor.h>
#include <otawa/proc/AbstractFeature.h>
namespace
lrusecurity
{
class
ProcessorExample
:
public
otawa
::
Processor
{
public:
static
otawa
::
p
::
declare
reg
;
ProcessorExample
(
otawa
::
p
::
declare
&
r
=
reg
);
protected:
void
configure
(
const
otawa
::
PropList
&
props
)
override
;
void
setup
(
otawa
::
WorkSpace
*
ws
)
override
;
void
processWorkSpace
(
otawa
::
WorkSpace
*
ws
)
override
;
void
destroy
(
otawa
::
WorkSpace
*
ws
)
override
;
private:
};
extern
otawa
::
p
::
feature
EXAMPLE_FEATURE
;
};
// namespace lrusecurity
#endif // LRUSECURITY_PROCESSOR_EXAMPLE_H_
src/lrusecurity_DUCatBuilder.cpp
View file @
cc0398b3
#ifndef LRUSECURITY_DU_CAT_BUILDER_H_
#define LRUSECURITY_DU_CAT_BUILDER_H_
#include <otawa/proc/BBProcessor.h>
#include <otawa/icat3/features.h>
#include <otawa/hard/Memory.h>
#include <lrumc/ACSManager.h>
#include <lrusecurity/features.h>
using
namespace
otawa
;
namespace
lrusecurity
{
class
DUCatBuilder
:
public
BBProcessor
{
public:
static
p
::
declare
reg
;
DUCatBuilder
(
void
)
:
BBProcessor
(
reg
),
_ways
(
0
),
_man
(
nullptr
)
{
}
protected:
virtual
void
setup
(
WorkSpace
*
ws
)
{
const
otawa
::
icat3
::
LBlockCollection
*
coll
=
icat3
::
LBLOCKS
(
ws
);
ASSERT
(
coll
);
_ways
=
coll
->
A
();
_man
=
new
ACSManager
(
ws
);
}
virtual
void
cleanup
(
WorkSpace
*
)
{
delete
_man
;
}
virtual
void
processBB
(
WorkSpace
*
,
CFG
*
,
Block
*
v
)
{
for
(
Block
::
EdgeIter
e
=
v
->
outs
();
e
;
e
++
)
{
if
(
logFor
(
LOG_BLOCK
))
log
<<
"
\t\t\t\t
process "
<<
*
e
<<
io
::
endl
;
if
(
v
->
isSynth
()
&&
v
->
toSynth
()
->
callee
())
_man
->
start
(
v
->
toSynth
()
->
callee
()
->
exit
());
else
_man
->
start
(
v
);
processAccesses
(
*
icache
::
ACCESSES
(
v
));
processAccesses
(
*
icache
::
ACCESSES
(
e
));
}
}
void
processAccesses
(
Bag
<
icache
::
Access
>&
accs
)
{
for
(
int
i
=
0
;
i
<
accs
.
count
();
i
++
)
{
otawa
::
icat3
::
LBlock
*
lb
=
icat3
::
LBLOCK
(
accs
[
i
]);
int
existHitAge
=
_man
->
existHitAge
(
lb
);
int
existMissAge
=
_man
->
existMissAge
(
lb
);
bool
eh
=
(
existHitAge
!=
_ways
);
bool
em
=
(
existMissAge
==
_ways
);
DUCategory
cat
;
if
(
eh
&&
em
)
cat
=
DUCategory
::
DU
;
else
if
(
eh
)
cat
=
DUCategory
::
EH
;
else
if
(
em
)
cat
=
DUCategory
::
EM
;
else
cat
=
DUCategory
::
NC
;
if
(
logFor
(
LOG_BLOCK
))
{
log
<<
"
\t\t\t\t\t
Access "
<<
accs
[
i
]
<<
" is "
;
switch
(
cat
)
{
case
DUCategory
::
DU
:
log
<<
"DU"
;
break
;
case
DUCategory
::
EH
:
log
<<
"EH"
;
break
;
case
DUCategory
::
EM
:
log
<<
"EM"
;
break
;
case
DUCategory
::
NC
:
log
<<
"NC"
;
break
;
}
log
<<
io
::
endl
;
}
DU_CATEGORY
(
accs
[
i
])
=
cat
;
_man
->
update
(
accs
[
i
]);
}
}
int
_ways
;
ACSManager
*
_man
;
};
p
::
declare
DUCatBuilder
::
reg
=
p
::
init
(
"lrusecurity::DUCatBuilder"
,
Version
(
1
,
0
,
0
))
.
extend
<
BBProcessor
>
()
.
make
<
DUCatBuilder
>
()
.
require
(
otawa
::
icat3
::
LBLOCKS_FEATURE
)
.
require
(
otawa
::
hard
::
MEMORY_FEATURE
)
.
require
(
lrusecurity
::
EXIST_HIT_ANALYSIS_FEATURE
)
.
require
(
lrusecurity
::
EXIST_MISS_ANALYSIS_FEATURE
)
.
provide
(
lrusecurity
::
DU_CATEGORY_FEATURE
);
/**
* This feature ensures that definitely unknown category information is stored on each
* @ref icache::Access found in the blocks and in the CFG of the current workspace.
* Such information is made of @ref DUCategory specifying the behaviour of the cache
* (EH -- Exist Hit, EM -- Exist Miss, DU -- Definitely Unknown (Exist Hit and Exist
* Miss), NC -- Not-classified).
*
* @par Properties
* @li @ref DU_CATEGORY
*
* @par Default implementation
* @li @ref DUCatBuilder
*
* @ingroup lrusecurity
*/
p
::
feature
DU_CATEGORY_FEATURE
(
"lrusecurity::DU_CATEGORY_FEATURE"
,
DUCatBuilder
::
reg
);
/**
* Defines the instruction cache Definitely Unknown category for the @ref icache::Access where
* this property is set.
*
* @par Hooks
* @li @ref icache::Access
*
* @par Features
* @li @ref DU_CATEGORY_FEATURE
*
* @ingroup lrusecurity
*/
p
::
id
<
DUCategory
>
DU_CATEGORY
(
"lrusecurity::DU_CATEGORY"
,
DUCategory
::
NC
);
}
// namespace lrusecurity
#endif // LRUSECURITY_DU_CAT_BUILDER_H_
src/lrusecurity_ProcessorExample.cpp
deleted
100644 → 0
View file @
dadf7271
#include "ProcessorExample.h"
#include <lrusecurity/features.h>
#include <otawa/icat3/features.h>
using
namespace
otawa
;
namespace
lrusecurity
{
ProcessorExample
::
ProcessorExample
(
p
::
declare
&
r
)
:
Processor
(
r
)
{
}
void
ProcessorExample
::
configure
(
const
PropList
&
props
)
{
Processor
::
configure
(
props
);
}
void
ProcessorExample
::
setup
(
WorkSpace
*
)
{
}
void
ProcessorExample
::
processWorkSpace
(
WorkSpace
*
)
{
}
void
ProcessorExample
::
destroy
(
WorkSpace
*
)
{
}
p
::
declare
ProcessorExample
::
reg
=
p
::
init
(
"lrusecurity::ProcessorExample"
,
Version
(
1
,
0
,
0
))
.
require
(
icat3
::
LBLOCKS_FEATURE
)
.
provide
(
EXAMPLE_FEATURE
)
.
make
<
ProcessorExample
>
();
p
::
feature
EXAMPLE_FEATURE
(
"lrusecurity::EXAMPLE_FEATURE"
,
p
::
make
<
ProcessorExample
>
());
p
::
id
<
int
>
EXAMPLE_PROPERTY
(
"lrusecurity::EXAMPLE_PROPERTY"
);
};
// namespace lrusecurity
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment