From 4e9f94a59d856c1f57837bdf5c388c324a5e8b46 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 2 Aug 2022 18:26:25 +0200 Subject: [PATCH 1/7] Drop ARINC support --- scripts/old/airbus/bench.sh | 95 -- scripts/old/airbus/bisect.sh | 42 - scripts/spec/check.sh | 3 - spin/airbus.pml | 58 - spin/arinc.base.pml | 400 ------- spin/check.sh | 17 - spin/deadlock.pml | 103 -- spin/deadlock_provided.pml | 63 - spin/graph.sh | 6 - spin/inlineBench.pml | 1038 ----------------- spin/starvation_provided.pml | 53 - src/analyses/arinc.ml | 656 ----------- src/analyses/extract_arinc.ml | 410 ------- src/analyses/libraryFunctions.ml | 6 - src/analyses/mutexEventsAnalysis.ml | 9 - src/cdomains/arincDomain.ml | 74 -- src/dune | 8 +- src/main.camldoc | 2 - src/mainarinc.ml | 17 - src/util/arincUtil.ml | 411 ------- src/util/goblintutil.ml | 16 - src/util/options.schema.json | 42 - tests/regression/17-arinc/01-sema.c | 142 --- tests/regression/17-arinc/02-unique_proc.c | 94 -- tests/regression/17-arinc/03-preemt_lock.c | 92 -- tests/regression/17-arinc/04-sema-strcpy.c | 146 --- tests/regression/17-arinc/05-term-simple.c | 33 - tests/regression/17-arinc/06-term.c | 113 -- tests/regression/17-arinc/07-cond-var.c | 28 - tests/regression/17-arinc/08-multi-cond.c | 23 - tests/regression/17-arinc/09-cond-var-scope.c | 36 - tests/regression/17-arinc/10-term-phases.c | 11 - tests/regression/17-arinc/README.md | 2 + tests/regression/17-arinc/arinc_sema.spec | 14 - 34 files changed, 6 insertions(+), 4257 deletions(-) delete mode 100755 scripts/old/airbus/bench.sh delete mode 100755 scripts/old/airbus/bisect.sh delete mode 100644 spin/airbus.pml delete mode 100644 spin/arinc.base.pml delete mode 100755 spin/check.sh delete mode 100644 spin/deadlock.pml delete mode 100644 spin/deadlock_provided.pml delete mode 100755 spin/graph.sh delete mode 100644 spin/inlineBench.pml delete mode 100644 spin/starvation_provided.pml delete mode 100644 src/analyses/arinc.ml delete mode 100644 src/analyses/extract_arinc.ml delete mode 100644 src/cdomains/arincDomain.ml delete mode 100644 src/mainarinc.ml delete mode 100644 src/util/arincUtil.ml delete mode 100644 tests/regression/17-arinc/01-sema.c delete mode 100644 tests/regression/17-arinc/02-unique_proc.c delete mode 100644 tests/regression/17-arinc/03-preemt_lock.c delete mode 100644 tests/regression/17-arinc/04-sema-strcpy.c delete mode 100644 tests/regression/17-arinc/05-term-simple.c delete mode 100644 tests/regression/17-arinc/06-term.c delete mode 100644 tests/regression/17-arinc/07-cond-var.c delete mode 100644 tests/regression/17-arinc/08-multi-cond.c delete mode 100644 tests/regression/17-arinc/09-cond-var-scope.c delete mode 100644 tests/regression/17-arinc/10-term-phases.c create mode 100644 tests/regression/17-arinc/README.md delete mode 100644 tests/regression/17-arinc/arinc_sema.spec diff --git a/scripts/old/airbus/bench.sh b/scripts/old/airbus/bench.sh deleted file mode 100755 index 0236f2f261..0000000000 --- a/scripts/old/airbus/bench.sh +++ /dev/null @@ -1,95 +0,0 @@ -function header() { - echo - echo "##### $1 #####" -} -set -o errexit -set -o pipefail # otherwise tee will always succeed, even if goblint has a non-zero exit status -pedantic=false -export OCAMLRUNPARAM=b -export scrambled=true -ret=${1-"success"} -if [ $ret = "success" ]; then - options="--enable ana.arinc.assume_success" -else - options="--disable ana.arinc.assume_success" - ret="fail" -fi -analyzer=~/goblint/analyzer -inputs=~/Dropbox/airbus -input=unrolled_monit.c -conf=ab.conf -if [ `pwd` = $analyzer ]; then - echo "Do not run in $analyzer! Go somewhere else; the goblint binary will be copied." - exit 1 -fi -function git_dirty { - dir=${1-"`pwd`"}; - test -n "$(git -C $dir status --porcelain)" -} -if $pedantic && git_dirty "$analyzer"; then - echo "The repo $analyzer is not in a clean state. Abort!" - exit 1 -fi -commit=$(git -C $analyzer rev-parse --short HEAD) -date=$(git -C $analyzer show -s --pretty=format:"%ai" $commit | sed 's/ +.*//' | sed 's/ /_/g') -lastmod=$(find $analyzer/{src,scripts} -printf "%Ty-%Tm-%Td-%TT\n" | sort -nr | head -n 1 | cut -d. -f1) -result="result_${date}_${commit}_${lastmod}_${ret}" -if [ -e $result ]; then - echo "$result already exists!" - exit -fi -echo "results will be in $result" -mkdir -p $result && pushd $result -echo $result >> log - -mkdir -p result -header "Building & copying files from $analyzer" -pushd $analyzer -make nat && popd -cp -f $analyzer/goblint . -cp -f $analyzer/g2html.jar . -cp -f $analyzer/spin/arinc?base.pml result # copy everything before the long running stuff... -header "Copying input & config from $inputs" -cp -f $inputs/{$input,$conf} . -if [ "$2" = "init" ]; then - exit 0 -fi -# dbg="$dbg --enable dbg.slice.on --set dbg.slice.n 4" -goblint="./goblint --conf $conf --set ana.activated ['base','arinc'] --enable ana.arinc.export --disable ana.arinc.simplify $options" -header "Write effective config" -$goblint --writeconf all.conf -header "Starting goblint" -time=$(which gtime 2>&- || which time 2>&-) # brew's GNU time on OS X is called gtime... -echo "Using time command at $time (this needs to be GNU time since the shell builtin doesn't support -v)" -function trace(){ - cmd=`echo ${1#./} | cut -d' ' -f1` - tt="time.$cmd.txt" - $time -v -o $tt $* 2>&1 | tee trace.$cmd.txt - cat $tt - t=`ag "wall clock" $tt | cut -f2 | cut -c-45 --complement` - c=`head -n1 $tt | cut -c-22 --complement` - echo "$t $c" >> log -} -trace $goblint $input -dot="result/arinc.dot" -pml="result/arinc.pml" -echo "$dot has $(wc -l < $dot) lines!" | tee -a log -echo "$pml has $(wc -l < $pml) lines!" | tee -a log -# fdp -Tpng -O $dot -# gnome-open ${dot}.png - -pushd result -mv ../log . -header "Generating SPIN Verifier from Promela Code" -set +o errexit # we want to be able to abort this if it takes too long -trace spin -DPRIOS -a arinc.pml -v -set -o errexit -trace clang -DVECTORSZ=5000 -o pan pan.c # complained that VECTORSZ should be > 1280 -echo "Verify! If there are errors, this will generate a file arinc.pml.trail" -# -f for fair scheduling -trace ./pan -n -a -m200000 -w26 2>&1 || (echo "Verification failed! Do simulation guided by trail."; spin -g -l -p -r -s -t -X -u10000 arinc.pml) -cat trace.pan.txt >> log -mv log .. -popd # result -# popd # script dir -unset scrambled diff --git a/scripts/old/airbus/bisect.sh b/scripts/old/airbus/bisect.sh deleted file mode 100755 index 5aaf4ee95d..0000000000 --- a/scripts/old/airbus/bisect.sh +++ /dev/null @@ -1,42 +0,0 @@ -set -o errexit -set -o pipefail -if [ $# -eq 0 ]; then - echo "Usage: $0 " - echo "e.g. --since=2weeks or -n 3 for limiting to the last 3 commits. See git --help log" - exit 1 -fi -analyzer=~/analyzer -if [ `pwd` = $analyzer ]; then - echo "Do not run in $analyzer! Go to some working dir. Everything will be copied." - exit 1 -fi -# cp $analyzer/scripts/airbusFun.sh . -pushd $analyzer -branch=`git rev-parse --abbrev-ref HEAD` -if [ "$branch" = "HEAD" ]; then - echo "Currently in detached head state. Checkout a branch first!" - exit 1 -fi -echo "Current branch is $branch" -commits=$(git log $* --reverse --pretty=format:"%h") -if test -z "$commits"; then - echo "Found no commits! Try different search options..." - exit 1 -fi -echo "Will checkout the following commits in that order:" -echo -git log $* --reverse -echo -read -p "Press [Enter] to continue" -echo -for sha in $commits; do - echo "Checkout $sha" - git checkout -q $sha - popd - ~/Dropbox/airbus/airbusFun.sh success init - ~/Dropbox/airbus/airbusFun.sh fail init - pushd $analyzer -done -echo "Returning to newest commit from $branch" -git checkout -q $branch -popd diff --git a/scripts/spec/check.sh b/scripts/spec/check.sh index 9ce1806b6a..a69fac5007 100755 --- a/scripts/spec/check.sh +++ b/scripts/spec/check.sh @@ -7,9 +7,6 @@ debug=${debug-"true"} if [ $ana == "file" ]; then ana="file" opt="--set ana.file.optimistic true" -elif [ $ana == "arinc" ]; then - ana="arinc" - opt="--enable ana.arinc.export --trace arinc" else spec=$ana ana="spec" diff --git a/spin/airbus.pml b/spin/airbus.pml deleted file mode 100644 index d6a83a32e7..0000000000 --- a/spin/airbus.pml +++ /dev/null @@ -1,58 +0,0 @@ -// configuration -#define nproc 3 // number of processes -#define nsema 1 // number of semaphores -#define nevent 1 // number of events - -// setup arinc functions and resources -#include "arinc.base.pml" - -// init -init { - Start(0); - run arinc_init(0); // process with id 0 is the arinc init process! - (partitionMode == NORMAL); // blocks until mode is NORMAL - run monitor(); // checks system invariants - // activate processes - run a(1); - run b(2); - /* run acem(0); */ - /* run ctl_dd63(1); */ - /* run dd63(2); */ -} - -proctype arinc_init(byte id) provided canRun(0) { - CreateSemaphore(0, 1, 1, FIFO); // id, current count, max count - Start(1); - Start(2); - SetPartitionMode(NORMAL); -} -proctype a(byte id) priority 5 provided canRun(1) { WaitSignalSema(0); } -proctype b(byte id) priority 5 provided canRun(2) { WaitSignalSema(0); } - -/* // define processes */ -/* proctype acem(byte id) { // prio 60, per 600 */ -/* SetEvent(0); */ -/* do :: */ -/* WaitSignalSema(0); */ -/* od */ -/* } */ -/* // serv_nvm: prio 55, per 600 */ -/* // init prio 53, per inf */ -/* proctype ctl_dd63(byte id) { // prio 15, per 600 */ -/* SetEvent(0); */ -/* do :: */ -/* Resume(dd63_id); */ -/* WaitEvent(0); */ -/* ResetEvent(0); */ -/* Suspend(dd63_id); */ -/* od */ -/* } */ -/* proctype dd63(byte id) { // prio 10, per inf */ -/* printf("\ndd63 pid is %d\n\n", _pid); */ -/* Suspend(dd63_id); */ -/* do :: */ -/* WaitSignalSema(0); */ -/* SetEvent(0); */ -/* od */ -/* } */ - diff --git a/spin/arinc.base.pml b/spin/arinc.base.pml deleted file mode 100644 index 7cb4d24184..0000000000 --- a/spin/arinc.base.pml +++ /dev/null @@ -1,400 +0,0 @@ -// configuration defaults -#ifndef PREEMPTION -#define PREEMPTION 1 -#endif -#ifndef nbboard -#define nbboard 0 -#endif -#ifndef nsema -#define nsema 0 -#endif -#ifndef nevent -#define nevent 0 -#endif - -// arinc spin model -// constants -#define DOWN 0 // events -#define UP 1 -#define EMPTY 0 // blackboards -#define NONEMPTY 1 -// #define SUCCESS 0 // return codes -// #define ERROR 1 -mtype = { SUCCESS, ERROR } - -// partition -mtype = { IDLE, COLD_START, WARM_START, NORMAL } // partition modes -mtype partitionMode = COLD_START; -// processes -mtype = { NOTCREATED, STOPPED, SUSPENDED, WAITING, READY, RUNNING, DONE } // possible process states -// of all READY the scheduler will choose one and set it to RUNNING (with prios there will only be one choice, without it will choose non-determ.) -mtype status[nproc] = NOTCREATED; // initialize all processes as not created -byte lockLevel; // scheduling only takes place if this is 0 -byte exclusive; // id of process that has exclusive privilige to execute if lockLevel > 0 -byte nperiodicWait; // number of processes that did a PeriodicWait and still wait -byte ncrit; // number of processes in critical section -byte processes_created; -// resources -mtype = { NONE, BLACKBOARD, SEMA, EVENT, TIME } -typedef Wait { mtype resource; byte id; } -Wait waiting[nproc]; - -#if nbboard // blackboards -bool bboards[nbboard] = EMPTY; -byte bboards_created; -#endif - -#if nsema // semaphores -mtype = { FIFO, PRIO } // queuing discipline -byte semas[nsema]; -byte semas_max[nsema]; -chan semas_chan[nsema] = [nproc] of { byte } -byte semas_created; -#endif - -#if nevent // events -bool events[nevent] = DOWN; -/* chan events_chan[nevent] = [nroc] of { byte } */ -byte events_created; -#endif - -// manage function calls at runtime to avoid inlining -// each proctype has its own: stack, sp -inline mark(pc) { - sp++; - stack[sp] = pc; -} - -// helpers for scheduling etc. -#define oneIs(v) checkStatus(==, v, ||) -#define oneIsNot(v) checkStatus(!=, v, ||) -#define allAre(v) checkStatus(==, v, &&) -#define noneAre(v) checkStatus(!=, v, &&) - -// status: NOTCREATED, STOPPED, SUSPENDED, WAITING, READY, (RUNNING), DONE -// LTL formulas -#define notStarving(i) (always (status[i] == READY implies always eventually (status[i] == READY || status[i] == STOPPED || status[i] == DONE))) -ltl not_starving { allTasks(notStarving) } -// ltl not_starving { ! (eventually always oneIs(WAITING) || oneIs(SUSPENDED)) } -ltl not_waiting { ! (eventually always oneIs(WAITING)) } -ltl not_suspended { ! (eventually always oneIs(SUSPENDED)) } -ltl all_created { eventually always noneAre(NOTCREATED) } -// ltl created_then_ready { allAre(NOTCREATED U READY) } -// ltl all_ready { allAre(eventually READY) } -// periodic processes should never be done -// TODO: ltl periodic { always periodic_noneAre(DONE) } -// TODO: ltl nonperiodic { eventually nonperiodic_allAre(DONE) } -// starvation: process will always be READY but never RUNNING -// ltl pr { ! (eventually always oneIs(READY)) } - -byte tmp; - -#if PREEMPTION -#define preInit status[0] = READY -#else -#define preInit status[0] = RUNNING // we only use RUNNING for the custom scheduler -#endif -inline postInit() { - (partitionMode == NORMAL); // block spin init until arinc init sets mode - // at this point every resource should have been created! - // revised: this need not be the case on all paths! - // NB: the extracted model is not precise enough with callstack_length = 0 - // TODO problem is, that then some paths in other processes later on are invalid if not all resources are created - // e.g. P2 is not created but P1 calls Start(P2) - // -> assert that process is created or do nothing - assert(processes_created == nproc-1); // mainfun is not created - #if nbboard - assert(bboards_created == nbboard); - #endif - #if nsema - assert(semas_created == nsema); - #endif - #if nevent - assert(events_created == nevent); - #endif - printf("Done with postInit!\n"); -} -#define canRun(proc_id) ((status[proc_id] == READY || status[proc_id] == RUNNING) && (lockLevel == 0 || exclusive == proc_id) && (partitionMode == NORMAL || proc_id == 0)) -#define isRunning(proc_id) (status[proc_id] == RUNNING) -inline setReady(proc_id) { - printf("setReady: process %d will be ready (was waiting for %e %d)\n", proc_id, waiting[proc_id].resource, waiting[proc_id].id); - waiting[proc_id].resource = NONE; - status[proc_id] = READY; -} -inline setWaiting(resource_type, resource_id) { - printf("setWaiting: process %d will wait for %e %d\n", id, resource_type, resource_id); - waiting[id].resource = resource_type; // waiting for... - waiting[id].id = resource_id; - status[id] = WAITING; // update process status (provided clause will block immediately) -} -inline changeStatus(from, to) { - byte i; - for (i in status) { - if - :: status[i] == from -> status[i] = to - :: else -> skip - fi - } -} -inline periodicWake() { - byte i; - for (i in status) { - if - :: status[i] == WAITING && waiting[i].resource == TIME -> status[i] = READY; waiting[i].resource = NONE; nperiodicWait--; break - :: else -> skip - fi - } -} -// fallback to macro since inline doesn't support return values... -#define isWaiting(proc_id, resource_type, resource_id) status[proc_id] == WAITING && waiting[proc_id].resource == resource_type && waiting[proc_id].id == resource_id -inline removeWaiting(proc_id) { - #if nsema - // remove process from waiting queues for all semas - byte sema_id; - for (sema_id in semas) { - byte i; - // this takes every element out of the channel and appends it again if it is not proc_id?! should just use semas_chan[sema_id]?p. but that would block if it's not in the queue... - for (i : 1 .. len(semas_chan[sema_id])) { - byte p; - semas_chan[sema_id]?p; - if - :: p != proc_id -> semas_chan[sema_id]!p - :: p == proc_id -> skip - fi - } - } - #endif - waiting[proc_id].resource = NONE; -} - - -// ARINC functions collected by analysis -inline LockPreemption() { atomic { - lockLevel++; - exclusive = id; -} } -inline UnlockPreemption() { atomic { - if - :: lockLevel > 0 -> lockLevel--; - :: lockLevel <= 0 -> skip - fi -} } -inline SetPartitionMode(mode) { atomic { - printf("SetPartitionMode(%e)\n", mode); - partitionMode = mode; -} } -inline CreateProcess(proc_id, pri, per, cap) { atomic { - printf("CreateProcess: id %d, priority %d, period %d, capacity %d\n", proc_id, pri, per, cap); - assert(status[proc_id] == NOTCREATED); - status[proc_id] = STOPPED; - waiting[proc_id].resource = NONE; - processes_created++; -} } -inline CreateErrorHandler(proc_id) { atomic { - printf("CreateErrorHandler: id %d\n", proc_id); - assert(status[proc_id] == NOTCREATED); - status[proc_id] = STOPPED; - waiting[proc_id].resource = NONE; - processes_created++; -} } -inline Start(proc_id) { atomic { - assert(status[proc_id] != NOTCREATED); - removeWaiting(proc_id); - status[proc_id] = READY; - // TODO reset process if it is already running! - // maybe insert after every statement: if restart[id] -> goto start_p1 -} } -inline Stop(proc_id) { atomic { - assert(status[proc_id] != NOTCREATED); - removeWaiting(proc_id); - status[proc_id] = STOPPED; -} } -inline Suspend(proc_id) { atomic { - assert(status[proc_id] != NOTCREATED); - status[proc_id] = SUSPENDED; -} } -inline Resume(proc_id) { atomic { - assert(status[proc_id] != NOTCREATED); - if - :: status[proc_id] == SUSPENDED -> // only do something if process was really suspended - if - // if the process was waiting for something when it was suspended, change it back to waiting! - :: waiting[proc_id].resource != NONE -> - status[proc_id] = WAITING; - :: ! (waiting[proc_id].resource != NONE) -> // otherwise resume - status[proc_id] = READY; - fi - :: status[proc_id] != SUSPENDED -> skip - fi -} } -// blocking behavior of blackboards and events are very similar -inline CreateBlackboard(bb_id) { atomic { - printf("CreateBlackboard: id %d\n", bb_id); - bboards[bb_id] = NONEMPTY; - bboards_created++; -} } -inline DisplayBlackboard(bb_id) { atomic { - // filter processes waiting for bb_id - byte i; - for (i in status) { - if - :: isWaiting(i, BLACKBOARD, bb_id) -> - setReady(i); - // no break, since we want to wake all processes waiting for this BLACKBOARD - :: !(isWaiting(i, BLACKBOARD, bb_id)) -> skip - fi - } - bboards[bb_id] = NONEMPTY; -} } -inline ReadBlackboard(bb_id) { atomic { - if - :: bboards[bb_id] == EMPTY -> setWaiting(BLACKBOARD, bb_id); - :: bboards[bb_id] == NONEMPTY -> skip // nothing to do - fi -} } -inline ClearBlackboard(bb_id) { atomic { - bboards[bb_id] = EMPTY; -} } -inline CreateSemaphore(sema_id, cur, max, queuing) { atomic { - printf("CreateSemaphore: id %d, current %d, max %d, queuing %e\n", sema_id, cur, max, queuing); - assert(queuing == FIFO); // TODO - semas[sema_id] = cur; - semas_max[sema_id] = max; - semas_created++; -} } -// code uses 0/FIFO as queuing discipline -inline WaitSemaphore(sema_id) { atomic { - // TODO priority queuing - // FIFO queuing (channel needed for preserving order) - if - :: semas[sema_id] == 0 -> - printf("WaitSema will block: semas[%d] = %d\n", sema_id, semas[sema_id]); - if - :: full(semas_chan[sema_id]) -> // TODO can this happen? - printf("FAIL: WaitSema: queue is full\n"); - assert(false); - :: nfull(semas_chan[sema_id]) -> - printf("Process %d put into queue for sema %d\n", id, sema_id); - semas_chan[sema_id]!id; // put current process in queue - fi; - setWaiting(SEMA, sema_id); // blocks this process instantly - // doc says: if stmt in atomic blocks, the rest will still remain atomic once it becomes executable. atomicity is lost if one jumps out of the sequence (which might be the case with provided (...)). - // revised: atomicity is broken if a statement inside the atomic blocks, but can continue as non-atomic - // so, atomic is broken after setWaiting, but that's ok since we're done with WaitSemaphore anyway - :: semas[sema_id] > 0 -> - printf("WaitSema will go through: semas[%d] = %d\n", sema_id, semas[sema_id]); - semas[sema_id] = semas[sema_id] - 1; - :: semas[sema_id] < 0 -> - printf("FAIL: WaitSema: count<0: semas[%d] = %d\n", sema_id, semas[sema_id]); - assert(false); - fi -} } -inline SignalSemaphore(sema_id) { atomic { - // filter processes waiting for sema_id - if - // no processes waiting on this semaphore -> increase count until max - :: empty(semas_chan[sema_id]) -> - printf("SignalSema: empty queue\n"); - if - :: semas[sema_id] < semas_max[sema_id] -> semas[sema_id] = semas[sema_id] + 1; - :: !(semas[sema_id] < semas_max[sema_id]) -> skip - fi - // otherwise it stays the same, since we will wake up a waiting process - :: nempty(semas_chan[sema_id]) -> // else doesn't work here because !empty is disallowed... - printf("SignalSema: %d processes in queue for sema %d with count %d\n", len(semas_chan[sema_id]), sema_id, semas[sema_id]); - byte i; - // replace this loop by using semas_chan[sema_id]?i and waking up process i? what if it's not waiting? - for (i in status) { - printf("SignalSema: check if process %d is waiting. status[%d] = %e. waiting for %e %d\n", i, i, status[i], waiting[i].resource, waiting[i].id); - if - :: isWaiting(i, SEMA, sema_id) && semas_chan[sema_id]?[i] -> // process is waiting for this semaphore and is at the front of its queue TODO prio queues - printf("SignalSema: process %d is waking up process %d\n", id, i); - semas_chan[sema_id]?eval(i); // consume msg from queue - setReady(i); - break - :: !(isWaiting(i, SEMA, sema_id) && semas_chan[sema_id]?[i]) -> skip - fi - }; - fi -} } -inline CreateEvent(event_id) { atomic { - printf("CreateEvent: id %d\n", event_id); - events_created++; -} } -inline WaitEvent(event_id) { atomic { - if - :: events[event_id] == DOWN -> setWaiting(EVENT, event_id); - :: events[event_id] == UP -> skip // nothing to do - fi -} } -inline SetEvent(event_id) { atomic { - // filter processes waiting for event_id - byte i; - for (i in status) { - if - :: isWaiting(i, EVENT, event_id) -> - setReady(i); - // no break, since we want to wake all processes waiting for this event - :: !(isWaiting(i, EVENT, event_id)) -> skip - fi - } - events[event_id] = UP; -} } -inline ResetEvent(event_id) { atomic { - events[event_id] = DOWN; -} } -inline PeriodicWait() { atomic { - // TODO PRIOS & PREEMPTION - #if PREEMPTION - status[id] = READY; // could be scheduled again right away - #else - status[id] = WAITING; - waiting[id].resource = TIME; - nperiodicWait++; - #endif -} } -inline TimedWait(time) { atomic { - PeriodicWait(); // TODO is this okay? -} } - - -// verification helpers -inline WaitSignalSema(sema_id) { - WaitSemaphore(sema_id); - ncrit++; - printf("Process %d is now in critical section!\n", id); - //assert(ncrit == 1); // critical section - ncrit--; - SignalSemaphore(sema_id); -} -// monitor for invariants -proctype monitor() { - byte i; - // at most 1 process may be in a critical region - assert(ncrit == 0 || ncrit == 1); - #if PREEMPTION - assert(nperiodicWait <= nproc); - #endif - #if nsema - // each semaphore value must be between 0 and max - for(i in semas) { - assert(semas[i] >= 0 && semas[i] <= semas_max[i]); - } - #endif - // at every time at least one process should be READY or all should be DONE - // atomic { - // byte nready = 0; - // byte ndone = 0; - // for(i in status) { - // if - // :: status[i] == READY -> nready++; - // :: status[i] == DONE -> ndone++; - // :: !(status[i] == READY || status[i] == DONE) -> skip - // fi - // } - // if - // :: nready == 0 && ndone < nproc -> printf("Deadlock detected (no process is READY (%d) but not all are DONE (%d))!\n", nready, ndone); assert(false); - // :: !(nready == 0 && ndone < nproc) -> skip - // fi - // } -} diff --git a/spin/check.sh b/spin/check.sh deleted file mode 100755 index 93cf9e9f57..0000000000 --- a/spin/check.sh +++ /dev/null @@ -1,17 +0,0 @@ -pml=${1-"result/arinc.pml"} -claim=${2} -max_depth=800000 -max_steps=800000 -rm -f $pml.trail -rm -f trail.txt -spin -DPRIOS -a $pml && -clang -Wno-parentheses-equality -o pan pan.c && # use -DNOLTL to exclude LTL claims -# ./pan # checks for invalid end states (e.g. deadlocks), but only if there are no ltl claims inside! otherwise it selects the first claim! -# ./pan -E # ignores invalid end states -./pan -n -m$max_depth -a -N $claim # checks ltl claim pw (e.g. processes must not stay WAITING) -rm -f pan.* pan - -if [[ -e $pml.trail ]]; then - spin -g -l -p -r -s -t -X $pml > trail.txt - vim trail.txt -fi diff --git a/spin/deadlock.pml b/spin/deadlock.pml deleted file mode 100644 index 07a5b96958..0000000000 --- a/spin/deadlock.pml +++ /dev/null @@ -1,103 +0,0 @@ -// configuration -#define nproc 3 // number of processes -#define nsema 2 // number of semaphores -#define PREEMPTION 1 - -// macro to check the status of all processes (derived macros defined in base) -#define checkStatus(op1, v, op2) (status[0] op1 v op2 status[1] op1 v op2 status[2] op1 v) - -// setup arinc functions and resources -#include "arinc.base.pml" - -// init -init { - // preInit; - status[0] = RUNNING; - run mainfun(0); // creates resources - postInit(); // blocks until PartitionMode == NORMAL - run monitor(); - run scheduler(); - run a(1); - run b(2); -} - -ltl pw { ! (eventually always oneIs(WAITING)) } -ltl ps { ! (eventually always oneIs(SUSPENDED)) } -// starvation: process will always be READY but never RUNNING -ltl pr { ! (eventually always oneIs(READY)) } - -#define PRIO0 -#define PRIO1 -#define PRIO2 -#ifdef PRIOS -// here executability constraints arising from the priorities can be redefined for each process -// e.g. let a have a higher prio than b, then b can only run if a is not READY: -/* #define PRIO2 && status[1] != READY */ -#endif - - -proctype scheduler() provided (partitionMode == NORMAL && (PREEMPTION || noneAre(RUNNING))) { atomic { - // find one process that can run (chooses non-determ. if multiple could run) - byte p; - do :: - #if PREEMPTION - // we need to make sure that another process ran before the next scheduling takes place - (_last != _pid); - #endif - if // encode priority here :) - :: canRun(0) PRIO0 -> p = 0 - :: canRun(1) PRIO1 -> p = 1 - :: canRun(2) PRIO2 -> p = 2 - :: allAre(DONE) -> printf("All done :)\n"); break - :: else -> - if - :: nperiodicWait > 0 -> periodicWake() // we can still wake up some waiting processes - :: else -> printf("No process can run but not all are done :(\n"); break - fi - fi - printf("The scheduler selected process %d to be RUNNING!\n", p); - #if PREEMPTION - // there might be a process running -> set it to ready - changeStatus(RUNNING, READY); - #else - // no processes running - // but: if some process did a PeriodicWait, we have to wake it again at some point (non-determ., but at the latest when no other process can run (see else-case above)) - if - :: periodicWake() - :: skip - fi - #endif - status[p] = RUNNING; - od -} } - -proctype mainfun(byte id) provided isRunning(0) { - CreateSemaphore(0, 1, 1, FIFO); - CreateSemaphore(1, 1, 1, FIFO); - CreateProcess(1, 53, 4294967295, 4294967295); // a (prio 53, period ∞, capacity ∞) - CreateProcess(2, 53, 4294967295, 4294967295); // a (prio 53, period ∞, capacity ∞) - Start(1); - Start(2); - SetPartitionMode(NORMAL); - status[id] = DONE; -} - -proctype a(byte id) provided isRunning(1) { - WaitSemaphore(0); - // PeriodicWait(); // needed for deadlock if no PREEMPTION - WaitSemaphore(1); - printf("Process a has both locks!\n"); - SignalSemaphore(1); - SignalSemaphore(0); - status[id] = DONE; -} - -proctype b(byte id) provided isRunning(2) { - WaitSemaphore(1); - WaitSemaphore(0); - printf("Process b has both locks!\n"); - SignalSemaphore(0); - SignalSemaphore(1); - status[id] = DONE; -} - diff --git a/spin/deadlock_provided.pml b/spin/deadlock_provided.pml deleted file mode 100644 index 45a72cc258..0000000000 --- a/spin/deadlock_provided.pml +++ /dev/null @@ -1,63 +0,0 @@ -// configuration -#define nproc 3 // number of processes -#define nsema 2 // number of semaphores - -// macro to check the status of all processes (derived macros defined in base) -#define checkStatus(op1, v, op2) (status[0] op1 v op2 status[1] op1 v op2 status[2] op1 v) - -// setup arinc functions and resources -#include "arinc.base.pml" - -// init -init { - // preInit; - status[0] = READY; - run mainfun(0); // creates resources - postInit(); // blocks until PartitionMode == NORMAL - run monitor(); - run a(1); - run b(2); -} - -ltl pw { ! (eventually always oneIs(WAITING)) } -ltl ps { ! (eventually always oneIs(SUSPENDED)) } -ltl pr { ! (eventually always oneIs(READY)) } - -#define PRIO0 -#define PRIO1 -#define PRIO2 -#ifdef PRIOS -// here executability constraints arising from the priorities can be redefined for each process -// e.g. let a have a higher prio than b, then b can only run if a is not READY: -/* #define PRIO2 && status[1] != READY */ -#endif - -proctype mainfun(byte id) provided (canRun(0) PRIO0) { - CreateSemaphore(0, 1, 1, FIFO); - CreateSemaphore(1, 1, 1, FIFO); - CreateProcess(1, 53, 4294967295, 4294967295); // a (prio 53, period ∞, capacity ∞) - CreateProcess(2, 53, 4294967295, 4294967295); // a (prio 53, period ∞, capacity ∞) - Start(1); - Start(2); - SetPartitionMode(NORMAL); - status[id] = DONE; -} - -proctype a(byte id) provided (canRun(1) PRIO1) { - WaitSemaphore(0); - WaitSemaphore(1); - printf("Process a has both locks!\n"); - SignalSemaphore(1); - SignalSemaphore(0); - status[id] = DONE; -} - -proctype b(byte id) provided (canRun(2) PRIO2) { - WaitSemaphore(1); - WaitSemaphore(0); - printf("Process b has both locks!\n"); - SignalSemaphore(0); - SignalSemaphore(1); - status[id] = DONE; -} - diff --git a/spin/graph.sh b/spin/graph.sh deleted file mode 100755 index e8360aa821..0000000000 --- a/spin/graph.sh +++ /dev/null @@ -1,6 +0,0 @@ -spin -a ${1-"airbus.pml"} -cc -o pan pan.c -rm -f pan.dot pan.svg -./pan -D | dot | gvpack -array_u > pan.dot -dot -Tsvg pan.dot > pan.svg -open -a Safari pan.svg \ No newline at end of file diff --git a/spin/inlineBench.pml b/spin/inlineBench.pml deleted file mode 100644 index f5a0eadc85..0000000000 --- a/spin/inlineBench.pml +++ /dev/null @@ -1,1038 +0,0 @@ -#define nproc 10 -mtype = { NOTCREATED, STOPPED, SUSPENDED, WAITING, READY, RUNNING, DONE } // possible process states -mtype status[nproc] = NOTCREATED; // initialize all processes as not created -byte tmp; - -inline doA() { - select (tmp : 0..4); - status[tmp] = RUNNING; -} - -inline doB() { - select (tmp : 5..9); - status[tmp] = WAITING; -} - -inline doStuff() { atomic { - status[tmp] = STOPPED; - if - :: doA(); - :: doB(); - fi - status[tmp] = DONE; - /* if */ - /* :: doA(); */ - /* :: doB(); */ - /* fi */ - /* if */ - /* :: doA(); */ - /* :: doB(); */ - /* fi */ - /* if */ - /* :: doA(); */ - /* :: doB(); */ - /* fi */ -} } - -active proctype a() { - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); - doStuff(); -} diff --git a/spin/starvation_provided.pml b/spin/starvation_provided.pml deleted file mode 100644 index dd228f6d46..0000000000 --- a/spin/starvation_provided.pml +++ /dev/null @@ -1,53 +0,0 @@ -// configuration -#define nproc 3 // number of processes - -// macro to check the status of all processes (derived macros defined in base) -#define checkStatus(op1, v, op2) (status[0] op1 v op2 status[1] op1 v op2 status[2] op1 v) - -#include "arinc.base.pml" - -// init -init { - // preInit; - status[0] = READY; - run mainfun(0); // creates resources - postInit(); // blocks until PartitionMode == NORMAL - run monitor(); - run a(1); - run b(2); -} - -ltl pw { ! (eventually always oneIs(WAITING)) } -ltl ps { ! (eventually always oneIs(SUSPENDED)) } -// if a keeps running, b will starve and never finish -ltl starve2 { ! (eventually always (status[2] == READY)) } -ltl starve2d { eventually (status[2] == DONE) } - -#define PRIO0 -#define PRIO1 -#define PRIO2 -#ifdef PRIOS -// here executability constraints arising from the priorities can be redefined for each process -// e.g. let a have a higher prio than b, then b can only run if a is not READY: -/* #define PRIO2 && status[1] != READY */ -#endif - -proctype mainfun(byte id) provided (canRun(0) PRIO0) { - CreateProcess(1, 53, 4294967295, 4294967295); // a (prio 53, period ∞, capacity ∞) - CreateProcess(2, 53, 4294967295, 4294967295); // a (prio 53, period ∞, capacity ∞) - Start(1); - Start(2); - SetPartitionMode(NORMAL); - status[id] = DONE; -} - -proctype a(byte id) provided (canRun(1) PRIO1) { - foo: PeriodicWait(); goto foo - status[id] = DONE; -} - -proctype b(byte id) provided (canRun(2) PRIO2) { - PeriodicWait(); - status[id] = DONE; -} - diff --git a/src/analyses/arinc.ml b/src/analyses/arinc.ml deleted file mode 100644 index db5d8caadd..0000000000 --- a/src/analyses/arinc.ml +++ /dev/null @@ -1,656 +0,0 @@ -(** Tracking of arinc processes and their actions. Output to console, graphviz and promela. *) - -open Prelude.Ana -open Analyses - -module BI = IntOps.BigIntOps - -module Functions = struct - let prefix = "LAP_Se_" - (* ARINC functions copied from stdapi.c *) - let with_timeout = List.map ((^) prefix) ["SuspendSelf"; "ReadBlackboard"; "WaitSemaphore"; "WaitEvent"] - let wout_timeout = List.map ((^) prefix) ["TimedWait";"PeriodicWait";"GetTime";"ReplenishAperiodic";"CreateProcess";"SetPriority";"Suspend";"Resume";"StopSelf";"Stop";"Start";"DelayedStart";"LockPreemption";"UnlockPreemption";"GetMyId";"GetProcessId";"GetProcessStatus";"GetPartitionStatus";"SetPartitionMode";"GetPartitionStartCondition";"CreateLogBook";"ReadLogBook";"WriteLogBook";"ClearLogBook";"GetLogbookId";"GetLogBookStatus";"CreateSamplingPort";"WriteSamplingMessage";"ReadSamplingMessage";"GetSamplingPortId";"GetSamplingPortStatus";"CreateQueuingPort";"SendQueuingMessage";"ReceiveQueuingMessage";"GetQueuingPortId";"GetQueuingPortStatus";"CreateBuffer";"SendBuffer";"ReceiveBuffer";"GetBufferId";"GetBufferStatus";"CreateBlackboard";"DisplayBlackboard";"ClearBlackboard";"GetBlackboardId";"GetBlackboardStatus";"CreateSemaphore";"SignalSemaphore";"GetSemaphoreId";"GetSemaphoreStatus";"CreateEvent";"SetEvent";"ResetEvent";"GetEventId";"GetEventStatus";"CreateErrorHandler";"GetErrorStatus";"RaiseApplicationError"] - (* functions from string.h which are implemented in the scrambled code *) - (* this is needed since strcpy is used for some process names, which will be top otherwise *) - let others = [ - "F59" (* strcpy *); "F60" (* strncpy *); "F63" (* memcpy *); "F1" (* memset *); - (* "F61"; "F62" (* these are optional. add them to speed up the analysis. *) *) - ] - let arinc_special = with_timeout @ wout_timeout - let special = arinc_special @ others - open ArincUtil - (* possible return code classes *) - let ret_success = [NO_ERROR; NO_ACTION] - let ret_error = [NOT_AVAILABLE; INVALID_PARAM; INVALID_CONFIG; INVALID_MODE; TIMED_OUT] - let ret_any = ret_success @ ret_error - let ret_no_timeout = List.remove ret_any TIMED_OUT - (* abstract value for return codes *) - (* TODO: Check whether Cil.IInt is correct here *) - let vd ret = `Int (ValueDomain.ID.(List.map (of_int Cil.IInt % BI.of_int % return_code_to_enum) ret |> List.fold_left join (bot_of IInt))) (* ana.int.enums should be enabled *) - let effects fname args = - if not (List.mem fname arinc_special) || List.is_empty args then None - else - match List.last args with - | AddrOf lv -> - Some ( - let ret = if GobConfig.get_bool "ana.arinc.assume_success" then ret_success else if List.mem fname with_timeout then ret_any else ret_no_timeout in - let v = vd ret in - M.debug ~category:Analyzer "effect of %s: set %a to %a" fname d_lval lv ValueDomain.Compound.pretty v; - [(lv, v)] - ) - | _ -> None -end - -module Spec : Analyses.MCPSpec = -struct - [@@@warning "-unused-value-declaration"] (* some functions are only used by commented out code *) - - include Analyses.DefaultSpec - - let name () = "arinc" - - let init marshal = - LibraryFunctions.add_lib_funs Functions.special; - LibraryFunctionEffects.add_effects Functions.effects - - (* ARINC types and Hashtables for collecting CFG *) - type id = varinfo - type resource = ArincUtil.resource - (* lookup/generate id from resource type and name (needed for LAP_Se_GetXId functions; specified by LAP_Se_CreateX functions during init) *) - (* map from tuple (resource, name) to varinfo (need to be saved b/c makeGlobalVar x t <> makeGlobalVar x t) *) - let resources = Hashtbl.create 13 - let get_id (resource,name as k:resource*string) : id = - try Hashtbl.find resources k - with Not_found -> - let vname = ArincUtil.show_resource resource^":"^name in - let v = Goblintutil.create_var (makeGlobalVar vname voidPtrType) in - Hashtbl.replace resources k v; - v - let get_by_id (id:id) : (resource*string) option = - Hashtbl.filter ((=) id) resources |> Hashtbl.keys |> Enum.get - - (* map process name to integer used in Pid domain *) - let pnames = Hashtbl.create 13 - let _ = Hashtbl.add pnames "mainfun" 0L - let get_by_pid pid = - Hashtbl.filter ((=) pid) pnames |> Hashtbl.keys |> Enum.get - let get_pid pname = - try Hashtbl.find pnames pname - with Not_found -> - let ids = Hashtbl.values pnames in - let id = if Enum.is_empty ids then 1L else Int64.succ (Enum.arg_max identity ids) in - Hashtbl.replace pnames pname id; - id - - - (* Domains *) - include ArincDomain - - module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (ArincDomain.D)) (* set of created tasks to spawn when going multithreaded *) - module G = Tasks - module C = D - module V = Printable.UnitConf (struct let name = "tasks" end) - - let context fd d = { d with pred = Pred.bot (); ctx = Ctx.bot () } - - (* function for creating a new intermediate node (will generate a new sid every time!) *) - let mkDummyNode ?loc line = - let loc = { (loc |? !Tracing.current_loc) with line = line } in - MyCFG.Statement { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc, locUnknown)) with sid = new_sid () } - (* table from sum type to negative line number for new intermediate node (-1 to -4 have special meanings) *) - type tmpNodeUse = Branch of stmt | Combine of lval - module NodeTbl = ArincUtil.SymTbl (struct type k = tmpNodeUse type v = MyCFG.node let getNew xs = mkDummyNode @@ -5 - (List.length (List.of_enum xs)) end) - (* context hash to differentiate function calls *) - module CtxTbl = ArincUtil.SymTbl (struct type k = int type v = int let getNew xs = if Enum.is_empty xs then 0 else (Enum.arg_max identity xs)+1 end) (* generative functor *) - let fname_ctx ctx f = f.vname ^ "_" ^ (match Ctx.to_int ctx with Some i -> i |> i64_to_int |> CtxTbl.get |> string_of_int | None -> "TOP") - - let is_single ctx = - not (ThreadFlag.is_multi (Analyses.ask_of_ctx ctx)) - let is_mainfun name = List.mem name (GobConfig.get_string_list "mainfun") - - type env = { d: D.t; node: MyCFG.node; fundec: fundec; pname: string; procid: ArincUtil.id; id: ArincUtil.id } - let get_env ctx = - let open ArincUtil in let _ = 42 in - let d = ctx.local in - let node = Option.get !MyCFG.current_node in - (* determine if we are at the root of a process or in some called function *) - let fundec = Node.find_fundec node in - let curpid = match Pid.to_int d.pid with Some i -> i | None -> failwith @@ "get_env: Pid.to_int = None inside function "^fundec.svar.vname^". State: " ^ D.show d in - let pname = match get_by_pid curpid with Some s -> s | None -> failwith @@ "get_env: no processname for pid in Hashtbl!" in - let procid = Process, pname in - let pfuns = funs_for_process (Process,pname) in - let id = if List.exists ((=) fundec.svar) pfuns || is_mainfun fundec.svar.vname then Process, pname else Function, fname_ctx d.ctx fundec.svar in - { d; node; fundec; pname; procid; id } - let add_edges ?r ?dst ?d env action = - Pred.iter (fun node -> ArincUtil.add_edge env.id (node, action, r, Node.location (dst |? env.node))) (d |? env.d).pred - let add_actions env xs = - (* add edges for all predecessor nodes (from pred. node to env.node) *) - List.iter (fun (action,r) -> match r with Some r -> add_edges ~r env action | None -> add_edges env action) xs; - (* update domain by replacing the set of pred. nodes with the current node *) - if List.is_empty xs then env.d else D.pred (const @@ Pred.of_node env.node) env.d - (* is exp of the return code type (pointers are not considered!) *) - let is_return_code_type exp = Cilfacade.typeOf exp |> unrollTypeDeep |> function - | TEnum(ei, _) when ei.ename = "T13" -> true - | _ -> false - let return_code_is_success z = Cilint.is_zero_cilint z || Cilint.compare_cilint z Cilint.one_cilint = 0 - let str_return_code i = if return_code_is_success i then "SUCCESS" else "ERROR" - let str_return_dlval (v,o as dlval) = - sprint d_lval (Lval.CilLval.to_lval dlval) ^ "_" ^ string_of_int v.vdecl.line |> - Str.global_replace (Str.regexp "[^a-zA-Z0-9]") "_" - let add_return_dlval env kind dlval = - ArincUtil.add_return_var env.procid kind (str_return_dlval dlval) - let dummy_global_dlval = { dummyFunDec.svar with vname = "Gret" }, `NoOffset - let global_dlval dlval fname = - if Lval.CilLval.class_tag dlval = `Global then ( - M.debug ~category:Analyzer "WARN: %s: use of global lval: %s" fname (str_return_dlval dlval); - if GobConfig.get_bool "ana.arinc.merge_globals" then dummy_global_dlval else dlval - ) else dlval - let mayPointTo ctx exp = - match ctx.ask (Queries.MayPointTo exp) with - | a when not (Queries.LS.is_top a) && Queries.LS.cardinal a > 0 -> - let top_elt = (dummyFunDec.svar, `NoOffset) in - let a' = if Queries.LS.mem top_elt a then ( - M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *) - Queries.LS.remove top_elt a - ) else a - in - Queries.LS.elements a' - | v -> - M.info ~category:Unsound "mayPointTo: query result for %a is %a, ignoring it" d_exp exp Queries.LS.pretty v; - (*failwith "mayPointTo"*) - [] - let iterMayPointTo ctx exp f = mayPointTo ctx exp |> List.iter f - - - (* transfer functions *) - let assign ctx (lval:lval) (rval:exp) : D.t = - (* if the lhs is (or points to) a return code variable, then: - if the rhs is a constant or another return code, output an assignment edge - else output edge that non-det. sets the lhs to a value from the range *) - (* things to note: - 1. is_return_code_type must be checked on the result of mayPointTo and not on lval! otherwise we have problems with pointers - 2. Cilfacade.typeOf throws an exception because the base type of a query result from goblint is not an array but is accessed with an index TODO why is this? ignored casts? - 3. mayPointTo also returns pointers if there's a top element in the set (outputs warning), so that we don't miss anything *) - if GobConfig.get_bool "ana.arinc.assume_success" then ctx.local else - (* OPT: this matching is just for speed up to avoid querying on every assign *) - match lval with Var _, _ when not @@ is_return_code_type (Lval lval) -> ctx.local | _ -> - (* TODO why is it that current_node can be None here, but not in other transfer functions? *) - if not @@ Option.is_some !MyCFG.current_node then (M.info ~category:Unsound ~tags:[Category Analyzer] "assign: MyCFG.current_node not set :("; ctx.local) else - if D.is_bot1 ctx.local then ctx.local else - let env = get_env ctx in - let edges_added = ref false in - let f dlval = - (* M.debug @@ "assign: MayPointTo " ^ sprint d_plainlval lval ^ ": " ^ sprint d_plainexp (Lval.CilLval.to_exp dlval); *) - let is_ret_type = try is_return_code_type @@ Lval.CilLval.to_exp dlval with Cilfacade.TypeOfError Index_NonArray -> M.debug ~category:Imprecise "assign: Cilfacade.typeOf %a threw exception Errormsg.Error \"Bug: typeOffset: Index on a non-array\". Will assume this is a return type to remain sound." d_exp (Lval.CilLval.to_exp dlval); true in - if (not is_ret_type) || Lval.CilLval.has_index dlval then () else - let dlval = global_dlval dlval "assign" in - edges_added := true; - add_return_dlval env `Write dlval; - let add_one str_rhs = add_edges env @@ ArincUtil.Assign (str_return_dlval dlval, str_rhs) in - let add_top () = add_edges ~r:(str_return_dlval dlval) env @@ ArincUtil.Nop in - match stripCasts rval with - | Const CInt(i,_,_) -> add_one @@ str_return_code i - (* | Lval rlval -> - iterMayPointTo ctx (AddrOf rlval) (fun rdlval -> add_return_dlval env `Read rdlval; add_one @@ str_return_dlval rdlval) *) - | _ -> add_top () - in - iterMayPointTo ctx (AddrOf lval) f; - if !edges_added then D.pred (const @@ Pred.of_node env.node) env.d else env.d - - let branch ctx (exp:exp) (tv:bool) : D.t = - (* ignore(printf "if %a = %B (line %i)\n" d_plainexp exp tv (!Tracing.current_loc).line); *) - (* only if we don't assume success, we need to consider branching on return codes *) - if D.is_bot1 ctx.local then ctx.local else (* TODO how can it be that everything is bot here, except pred? *) - let env = get_env ctx in - if GobConfig.get_bool "ana.arinc.assume_success" then ctx.local else - let check a b tv = - (* we are interested in a comparison between some lval lval (which has the type of the return code enum) and a value of that enum (which gets converted to an Int by CIL) *) - match a, b with - | Lval lval, Const CInt(i,_,_) - | Const CInt(i,_,_), Lval lval when is_return_code_type (Lval lval) -> - (* let success = return_code_is_success i = tv in (* both must be true or false *) *) - (* ignore(printf "if %s: %a = %B (line %i)\n" (if success then "success" else "error") d_plainexp exp tv (!Tracing.current_loc).line); *) - (match env.node with - | MyCFG.Statement({ skind = If(e, bt, bf, loc, eloc); _ } as stmt) -> - (* 1. write out edges to predecessors, 2. set predecessors to current node, 3. write edge to the first node of the taken branch and set it as predecessor *) - (* the then-block always has some stmts, but the else-block might be empty! in this case we use the successors of the if instead. *) - let then_node = NodeTbl.get @@ Branch (List.hd bt.bstmts) in - let else_stmts = if List.is_empty bf.bstmts then stmt.succs else bf.bstmts in - let else_node = NodeTbl.get @@ Branch (List.hd else_stmts) in - let dst_node = if tv then then_node else else_node in - let d_if = if List.compare_length_with stmt.preds 1 > 0 then ( (* seems like this never happens *) - M.debug ~category:Analyzer "WARN: branch: If has more than 1 predecessor, will insert Nop edges!"; - add_edges env ArincUtil.Nop; - { ctx.local with pred = Pred.of_node env.node } - ) else ctx.local - in - (* now we have to add Pos/Neg-edges (depending on tv) for everything v may point to *) - let f dlval = - if Lval.CilLval.has_index dlval then () else - let dlval = global_dlval dlval "branch" in - let str_dlval = str_return_dlval dlval in - let cond = str_dlval ^ " == " ^ str_return_code i in - let cond = if tv then cond else "!(" ^ cond ^ ")" in - let cond = if dlval = dummy_global_dlval || String.exists str_dlval "int___unknown" then "true" else cond in (* we don't know the index of the array -> assume that branch could always be taken *) - add_edges ~dst:dst_node ~d:d_if env (ArincUtil.Cond (str_dlval, cond)); - add_return_dlval env `Read dlval - in - iterMayPointTo ctx (AddrOf lval) f; - { ctx.local with pred = Pred.of_node dst_node } - | _ -> failwith "branch: current_node is not an If") (* this should never happen since CIL transforms switch *) - | _ -> ctx.local - in - match exp with - (* TODO limit to BinOp Eq/Ne? Could also be other type of expression! *) - | BinOp(Eq, a, b, _) -> check (stripCasts a) (stripCasts b) tv - | BinOp(Ne, a, b, _) -> check (stripCasts a) (stripCasts b) (not tv) - | _ -> ctx.local - - let body ctx (f:fundec) : D.t = (* enter is not called for spawned processes -> initialize them here *) - (* M.debug ~category:Analyzer @@ "BODY " ^ f.svar.vname ^" @ "^ string_of_int (!Tracing.current_loc).line; *) - (* if not (is_single ctx || !Goblintutil.global_initialization || fst (ctx.global part_mode_var)) then raise Analyses.Deadcode; *) - let module BaseMain = (val Base.get_main ()) in - let base_context = BaseMain.context_cpa f @@ Obj.obj @@ ctx.presub "base" in - let context_hash = Hashtbl.hash (base_context, ctx.local.pid) in - { ctx.local with ctx = Ctx.of_int (Int64.of_int context_hash) } - - let return ctx (exp:exp option) (f:fundec) : D.t = - ctx.local - - let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = (* on function calls (also for main); not called for spawned processes *) - let d_caller = ctx.local in - let d_callee = if D.is_bot ctx.local then ctx.local else { ctx.local with pred = Pred.of_node (MyCFG.Function f); ctx = Ctx.top () } in (* set predecessor set to start node of function *) - [d_caller, d_callee] - - let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t = - if D.is_bot1 ctx.local || D.is_bot1 au then ctx.local else - let env = get_env ctx in - let d_caller = ctx.local in - let d_callee = au in - (* check if the callee has some relevant edges, i.e. advanced from the entry point. if not, we generate no edge for the call and keep the predecessors from the caller *) - if Pred.is_bot d_callee.pred then failwith "d_callee.pred is bot!"; (* set should never be empty *) - if Pred.equal d_callee.pred (Pred.of_node (MyCFG.Function f)) then - { d_callee with pred = d_caller.pred; ctx = d_caller.ctx } - else ( - (* write out edges with call to f coming from all predecessor nodes of the caller *) - (* if Option.is_some !last_ctx_hash && current_ctx_hash () = string_of_int (Option.get !last_ctx_hash) then *) - if Ctx.is_int d_callee.ctx then ( - (* before doing the call we need to assign call-by-value return code parameters - we only need to take care of them and not AddrOf args since those are found by query *) - (* TODO optimally we would track if the caller_exp was used as a return code in an ARINC call before; - as a first step we should check if its value is top (if it's set to some value and not invalidated by a call, then we are not interested in creating branches for it) *) - let check (callee_var,caller_exp) = match stripCasts caller_exp with - | Lval lval when is_return_code_type (Lval (var callee_var)) -> Some (callee_var, lval) - | _ -> None - in - let rargs = List.combine f.sformals args |> List.filter_map check in - let assign pred dst_node callee_var caller_dlval = - let caller_dlval = global_dlval caller_dlval "combine" in - let callee_dlval = callee_var, `NoOffset in - (* add edge to an intermediate node that assigns the caller return code to the one of the function params *) - add_edges ~dst:dst_node ~d:{ d_caller with pred = pred } env (ArincUtil.Assign (str_return_dlval callee_dlval, str_return_dlval caller_dlval)); - (* we also need to add the callee param as a `Write lval so that we see that it is written to *) - add_return_dlval env `Write callee_dlval; - (* also add the caller param because it is read *) - add_return_dlval env `Read caller_dlval; - in - (* we need to assign all lvals each caller arg may point to *) - let last_pred = if GobConfig.get_bool "ana.arinc.assume_success" then d_caller.pred else List.fold_left (fun pred (callee_var,caller_lval) -> let dst_node = NodeTbl.get (Combine caller_lval) in iterMayPointTo ctx (AddrOf caller_lval) (assign pred dst_node callee_var); Pred.of_node dst_node) d_caller.pred rargs in - add_edges ~d:{ d_caller with pred = last_pred } env (ArincUtil.Call (fname_ctx d_callee.ctx f.svar)) - ); - (* set current node as new predecessor, since something interesting happend during the call *) - { d_callee with pred = Pred.of_node env.node; ctx = d_caller.ctx } - ) - - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = - let open ArincUtil in let _ = 42 in (* sublime's syntax highlighter gets confused without the second let... *) - let d : D.t = ctx.local in - if D.is_bot1 d then d else - let env = get_env ctx in - let is_arinc_fun = startsWith Functions.prefix f.vname in - let is_creating_fun = startsWith (Functions.prefix^"Create") f.vname in - if M.tracing && is_arinc_fun then ( - M.tracel "arinc" "found %s(%a) in %s" f.vname (Pretty.d_list ", " d_exp) arglist env.fundec.svar.vname - ); - let is_error_handler = env.pname = pname_ErrorHandler in - let eval_int exp = - match ctx.ask (Queries.EvalInt exp) with - | x when Queries.ID.is_int x -> Option.get @@ Queries.ID.to_int x - | _ -> failwith @@ "Could not evaluate int-argument "^sprint d_plainexp exp^" in "^f.vname - in - let eval_str exp = - match ctx.ask (Queries.EvalStr exp) with - | `Lifted s -> s - | _ -> failwith @@ "Could not evaluate string-argument "^sprint d_plainexp exp^" in "^f.vname - in - let eval_id exp = mayPointTo ctx exp |> List.map (Option.get % get_by_id % fst) in - let assign_id exp id = - match exp with - (* call assign for all analyses (we only need base)! *) - | AddrOf lval -> ctx.emit (Assign {lval; exp = mkAddrOf @@ var id}) - (* TODO not needed for the given code, but we could use Queries.MayPointTo exp in this case *) - | _ -> failwith @@ "Could not assign id. Expected &id. Found "^sprint d_exp exp - in - let assign_id_by_name resource_type name id = - assign_id id (get_id (resource_type, eval_str name)) - in - let arglist = List.map (stripCasts%(constFold false)) arglist in - (* if assume_success we set the return code and don't need to do anything else - otherwise we need to invalidate the return code (TODO maybe not top but sth more precise) and include the return code variable for all arinc calls (so that it can be set non-deterministically in promela) *) - let add_actions actions = - if is_arinc_fun && not @@ List.is_empty arglist then - let r = List.last arglist in - if GobConfig.get_bool "ana.arinc.assume_success" then ( - add_actions env @@ List.map (fun action -> action, None) actions - ) else ( - let xs = mayPointTo ctx r in - (* warn about wrong type (r should always be a return code) and setting globals! *) - let f dlval = - let dlval = global_dlval dlval "special" in - if not @@ is_return_code_type @@ Lval.CilLval.to_exp dlval - then (M.debug ~category:Analyzer "WARN: last argument in arinc function may point to something other than a return code: %s" (str_return_dlval dlval); None) - else (add_return_dlval env `Write dlval; Some (str_return_dlval dlval)) - in - (* add actions for all lvals r may point to *) - let rets = List.map Option.some @@ List.filter_map f xs in - add_actions env @@ List.cartesian_product actions rets - ) - else (* no args *) - add_actions env @@ List.map (fun action -> action,None) actions - in - let add_action action = add_actions [action] in - (* - let assert_ptr e = match unrollType (Cilfacade.typeOf e) with - | TPtr _ -> () - | _ -> failwith @@ f.vname ^ " expects arguments to be some pointer, but got "^sprint d_exp e^" which is "^sprint d_plainexp e - in - *) - let todo () = if false then failwith @@ f.vname^": Not implemented yet!" else add_action Nop in - match f.vname, arglist with - | _ when is_arinc_fun && is_creating_fun && not(mode_is_init d.pmo) -> - failwith @@ f.vname^" is only allowed in partition mode COLD_START or WARM_START" - (* Preemption *) - | "LAP_Se_LockPreemption", [lock_level; r] when not is_error_handler -> - add_action LockPreemption - |> D.pre (PrE.add (PrE.of_int 1L)) - | "LAP_Se_UnlockPreemption", [lock_level; r] when not is_error_handler -> - add_action UnlockPreemption - |> D.pre (PrE.sub (PrE.of_int 1L)) - (* Partition *) - | "LAP_Se_SetPartitionMode", [mode; r] -> begin - match ctx.ask (Queries.EvalInt mode) with - | x when Queries.ID.is_int x -> - let i = Option.get @@ Queries.ID.to_int x in - let pm = partition_mode_of_enum @@ BI.to_int i in - if M.tracing then M.tracel "arinc" "setting partition mode to %Ld (%s)\n" (BI.to_int64 i) (show_partition_mode_opt pm); - if mode_is_multi (Pmo.of_int (BI.to_int64 i)) then ( - let tasks = ctx.global () in - ignore @@ printf "arinc: SetPartitionMode NORMAL: spawning %i processes!\n" (Tasks.cardinal tasks); - Tasks.iter (fun (fs,f_d) -> Queries.LS.iter (fun f -> ctx.spawn None (fst f) []) fs) tasks; - ); - add_action (SetPartitionMode pm) - |> D.pmo (const @@ Pmo.of_int (BI.to_int64 i)) - | _ -> D.top () - end - | "LAP_Se_GetPartitionStatus", [status; r] -> todo () (* != mode *) - | "LAP_Se_GetPartitionStartCondition", [start_condition; r] -> todo () - (* treat functions from string.h as extern if they are added at the end of libraryFunctions.ml *) - (* - | "F59", [dst; src] (* strcpy: stops at \000 in src *) - | "F60", [dst; src; _] (* strncpy: stops at \000 in src or if len has been copied. if src ends before len, dst is padded with zeros. TODO len *) - (* | "F61", [str1; str2] (* strcmp: compares chars until they differ or \000 is reached. returns c1 - c2 *) *) - (* | "F62", [dst; src; len] (* strncmp *) *) - (* | "F63", [dst; src; len] (* memcpy *) *) - -> - M.debug ~category:Analyzer @@ "strcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^")"; - (*debugMayPointTo ctx dst;*) - assert_ptr dst; assert_ptr src; - (* let dst_lval = mkMem ~addr:dst ~off:NoOffset in *) - (* let src_expr = Lval (mkMem ~addr:src ~off:NoOffset) in *) - begin match ctx.ask (Queries.MayPointTo dst) with - | ls -> - ignore @@ Pretty.printf "strcpy %a points to %a\n" d_exp dst Queries.LS.pretty ls; - Queries.LS.iter (fun (v,o) -> ctx.assign ~name:"base" (Var v, Lval.CilLval.to_ciloffs o) src) ls - | _ -> M.debug ~category:Analyzer @@ "strcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^"): dst may point to anything!"; - end; - d - | "F63" , [dst; src; len] (* memcpy *) - -> - M.debug ~category:Analyzer @@ "memcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^")"; - (match ctx.ask (Queries.EvalInt len) with - | `Int i -> - (* - let len = i64_to_int @@ eval_int len in - for i = 0 to len-1 do - let dst_lval = mkMem ~addr:dst ~off:(Index (integer i, NoOffset)) in - let src_lval = mkMem ~addr:src ~off:(Index (integer i, NoOffset)) in - ctx.assign ~name:"base" dst_lval (Lval src_lval); - done; - *) - assert_ptr dst; assert_ptr src; - let dst_lval = mkMem ~addr:dst ~off:NoOffset in - let src_lval = mkMem ~addr:src ~off:NoOffset in - ctx.assign ~name:"base" dst_lval (Lval src_lval); (* this is only ok because we use ArrayDomain.Trivial per default, i.e., there's no difference between the first element or the whole array *) - | v -> M.debug ~category:Analyzer @@ "F63/memcpy: don't know length: " ^ sprint Queries.Result.pretty v; - let lval = mkMem ~addr:dst ~off:NoOffset in - ctx.assign ~name:"base" lval MyCFG.unknown_exp - ); - M.debug @@ "done with memcpy/"^f.vname; - d - | "F1" , [dst; data; len] (* memset: write char to dst len times *) - -> - (match ctx.ask (Queries.EvalInt len) with - | `Int i -> - (* - let len = i64_to_int @@ eval_int len in - for i = 0 to len-1 do - let lval = mkMem ~addr:dst ~off:(Index (integer i, NoOffset)) in - ctx.assign ~name:"base" lval data; - done; - *) - let dst_lval = mkMem ~addr:dst ~off:NoOffset in - ctx.assign ~name:"base" dst_lval data; (* this is only ok because we use ArrayDomain.Trivial per default, i.e., there's no difference between the first element or the whole array *) - | v -> M.debug ~category:Analyzer @@ "F1/memset: don't know length: " ^ sprint Queries.Result.pretty v; - let lval = mkMem ~addr:dst ~off:NoOffset in - ctx.assign ~name:"base" lval MyCFG.unknown_exp - ); - d - *) - (* Processes *) - | "LAP_Se_CreateProcess", [AddrOf attr; pid; r] -> - let cm = match unrollType (Cilfacade.typeOfLval attr) with - | TComp (c,_) -> c - | _ -> failwith "type-error: first argument of LAP_Se_CreateProcess not a struct." - in - let struct_fail f x = - f @@ "LAP_Se_CreateProcess: problem with first argument: " ^ - begin match x with - | `Field ofs -> "cannot access field " ^ ofs - | `Result (name, entry_point, pri, per, cap) -> - "struct PROCESS_ATTRIBUTE_TYPE needs all of the following fields (with result): NAME ("^name^"), ENTRY_POINT ("^entry_point^"), BASE_PRIORITY ("^pri^"), PERIOD ("^per^"), TIME_CAPACITY ("^cap^")" - end ^ ". Running scrambled: "^string_of_bool Goblintutil.scrambled - in - let field ofs = - try Lval (addOffsetLval (Field (getCompField cm ofs, NoOffset)) attr) - with Not_found -> struct_fail failwith (`Field ofs) - in - let name = ctx.ask (Queries.EvalStr (field Goblintutil.arinc_name)) in - let entry_point = ctx.ask (Queries.ReachableFrom (AddrOf attr)) in - let pri = ctx.ask (Queries.EvalInt (field Goblintutil.arinc_base_priority)) in - let per = ctx.ask (Queries.EvalInt (field Goblintutil.arinc_period)) in - let cap = ctx.ask (Queries.EvalInt (field Goblintutil.arinc_time_capacity)) in - begin match name, entry_point, pri, per, cap with - | `Lifted name, ls, pri, per, cap when not (Queries.LS.is_top ls) - && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) && Queries.ID.is_int pri && Queries.ID.is_int per && Queries.ID.is_int cap -> - let pri = BI.to_int64 (Option.get @@ Queries.ID.to_int pri) in - let per = BI.to_int64 (Option.get @@ Queries.ID.to_int per) in - let cap = BI.to_int64 (Option.get @@ Queries.ID.to_int cap) in - let funs_ls = Queries.LS.filter (fun (v,o) -> let lval = Var v, Lval.CilLval.to_ciloffs o in isFunctionType (Cilfacade.typeOfLval lval)) ls in (* do we need this? what happens if we spawn a variable that's not a function? shouldn't this check be in spawn? *) - if M.tracing then M.tracel "arinc" "starting a thread %a with priority '%Ld' \n" Queries.LS.pretty funs_ls pri; - let funs = funs_ls |> Queries.LS.elements |> List.map fst |> List.unique in - let f_d = { pid = Pid.of_int (get_pid name); pri = Pri.of_int pri; per = Per.of_int per; cap = Cap.of_int cap; pmo = Pmo.of_int 3L; pre = PrE.top (); pred = Pred.of_loc f.vdecl; ctx = Ctx.top () } in - let tasks = Tasks.add (funs_ls, f_d) (ctx.global ()) in - ctx.sideg () tasks; - let pid' = Process, name in - assign_id pid (get_id pid'); - add_actions (List.map (fun f -> CreateProcess Action.({ pid = pid'; f; pri; per; cap })) funs) - | _ -> let f (type a) (x: a Queries.result) = "TODO" in struct_fail (M.debug ~category:Analyzer "%s") (`Result (f name, f entry_point, f pri, f per, f cap)); d (* TODO: f*) - end - | "LAP_Se_GetProcessId", [name; pid; r] -> - assign_id_by_name Process name pid; d - | "LAP_Se_GetProcessStatus", [pid; status; r] -> todo () - | "LAP_Se_GetMyId", [pid; r] -> - assign_id pid (get_id env.procid); d - | "LAP_Se_Start", [pid; r] -> - (* at least one process should be started in main *) - add_actions @@ List.map (fun pid -> Start pid) (eval_id pid) - | "LAP_Se_DelayedStart", [pid; delay; r] -> todo () - | "LAP_Se_Stop", [pid; r] -> - add_actions @@ List.map (fun pid -> Stop pid) (eval_id pid) - | "LAP_Se_StopSelf", [] -> - if mode_is_init d.pmo then failwith @@ "The behavior of " ^ f.vname ^ " is not defined in WARM_START/COLD_START!"; - add_action (Stop env.procid) - | "LAP_Se_Suspend", [pid; r] -> - add_actions @@ List.map (fun pid -> Suspend pid) (eval_id pid) - | "LAP_Se_SuspendSelf", [timeout; r] -> - let t = BI.to_int64 (eval_int timeout) in - add_action (SuspendSelf (env.procid, t)) - | "LAP_Se_Resume", [pid; r] -> - add_actions @@ List.map (fun pid -> Resume pid) (eval_id pid) - (* Logbook - not used *) - | "LAP_Se_CreateLogBook", [name; max_size; max_logged; max_in_progress; lbid; r] -> todo () - | "LAP_Se_ReadLogBook", _ -> todo () - | "LAP_Se_WriteLogBook", _ -> todo () - | "LAP_Se_ClearLogBook", _ -> todo () - | "LAP_Se_GetLogBookId", _ -> todo () - | "LAP_Se_GetLogBookStatus", _ -> todo () - (* SamplingPort - inter-partition *) - | "LAP_Se_CreateSamplingPort", [name; max_size; dir; period; spid; r] -> todo () - | "LAP_Se_WriteSamplingMessage", _ -> todo () - | "LAP_Se_ReadSamplingMessage", _ -> todo () - | "LAP_Se_GetSamplingPortId", _ -> todo () - | "LAP_Se_GetSamplingPortStatus", _ -> todo () - (* QueuingPort - inter-partition *) - | "LAP_Se_CreateQueuingPort", [name; max_size; max_range; dir; queuing; qpid; r] -> todo () - | "LAP_Se_SendQueuingMessage", _ -> todo () - | "LAP_Se_ReceiveQueuingMessage", _ -> todo () - | "LAP_Se_GetQueuingPortId", _ -> todo () - | "LAP_Se_GetQueuingPortStatus", _ -> todo () - (* Buffer - not used *) - | "LAP_Se_CreateBuffer", [name; max_size; max_range; queuing; buid; r] -> todo () - | "LAP_Se_SendBuffer", _ -> todo () - | "LAP_Se_ReceiveBuffer", _ -> todo () - | "LAP_Se_GetBufferId", _ -> todo () - | "LAP_Se_GetBufferStatus", _ -> todo () - (* Blackboard *) - | "LAP_Se_CreateBlackboard", [name; max_size; bbid; r] -> - let bbid' = Blackboard, eval_str name in - assign_id bbid (get_id bbid'); - add_action (CreateBlackboard bbid') - | "LAP_Se_DisplayBlackboard", [bbid; msg_addr; len; r] -> - add_actions @@ List.map (fun id -> DisplayBlackboard id) (eval_id bbid) - | "LAP_Se_ReadBlackboard", [bbid; timeout; msg_addr; len; r] -> - let t = BI.to_int64 (eval_int timeout) in - add_actions @@ List.map (fun id -> ReadBlackboard (id, t)) (eval_id bbid) - | "LAP_Se_ClearBlackboard", [bbid; r] -> - add_actions @@ List.map (fun id -> ClearBlackboard id) (eval_id bbid) - | "LAP_Se_GetBlackboardId", [name; bbid; r] -> - assign_id_by_name Blackboard name bbid; d - | "LAP_Se_GetBlackboardStatus", _ -> todo () - (* Semaphores *) - | "LAP_Se_CreateSemaphore", [name; cur; max; queuing; sid; r] -> - (* create resource for name *) - let sid' = Semaphore, eval_str name in - assign_id sid (get_id sid'); - add_action (CreateSemaphore Action.({ sid = sid'; cur = (BI.to_int64 (eval_int cur)); max = (BI.to_int64 (eval_int max)); queuing = (BI.to_int64 (eval_int queuing)) })) - | "LAP_Se_WaitSemaphore", [sid; timeout; r] -> (* TODO timeout *) - let t = BI.to_int64 (eval_int timeout) in - add_actions @@ List.map (fun id -> WaitSemaphore (id, t)) (eval_id sid) - | "LAP_Se_SignalSemaphore", [sid; r] -> - add_actions @@ List.map (fun id -> SignalSemaphore id) (eval_id sid) - | "LAP_Se_GetSemaphoreId", [name; sid; r] -> - assign_id_by_name Semaphore name sid; d - | "LAP_Se_GetSemaphoreStatus", [sid; status; r] -> todo () - (* Events (down after create/reset, up after set) *) - | "LAP_Se_CreateEvent", [name; eid; r] -> - let eid' = Event, eval_str name in - assign_id eid (get_id eid'); - add_action (CreateEvent eid') - | "LAP_Se_SetEvent", [eid; r] -> - add_actions @@ List.map (fun id -> SetEvent id) (eval_id eid) - | "LAP_Se_ResetEvent", [eid; r] -> - add_actions @@ List.map (fun id -> ResetEvent id) (eval_id eid) - | "LAP_Se_WaitEvent", [eid; timeout; r] -> (* TODO timeout *) - let t = BI.to_int64 (eval_int timeout) in - add_actions @@ List.map (fun id -> WaitEvent (id, t)) (eval_id eid) - | "LAP_Se_GetEventId", [name; eid; r] -> - assign_id_by_name Event name eid; d - | "LAP_Se_GetEventStatus", [eid; status; r] -> todo () - (* Time *) - | "LAP_Se_GetTime", [time; r] -> todo () - | "LAP_Se_TimedWait", [delay; r] -> - add_action (TimedWait (BI.to_int64 (eval_int delay))) - | "LAP_Se_PeriodicWait", [r] -> - add_action PeriodicWait - (* Errors *) - | "LAP_Se_CreateErrorHandler", [entry_point; stack_size; r] -> - begin match ctx.ask (Queries.ReachableFrom (entry_point)) with - | ls when not (Queries.LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) -> - let pid = get_pid pname_ErrorHandler in - let funs_ls = Queries.LS.filter (fun (v,o) -> let lval = Var v, Lval.CilLval.to_ciloffs o in isFunctionType (Cilfacade.typeOfLval lval)) ls in - let funs = funs_ls |> Queries.LS.elements |> List.map fst |> List.unique in - let f_d = { pid = Pid.of_int pid; pri = Pri.of_int infinity; per = Per.of_int infinity; cap = Cap.of_int infinity; pmo = Pmo.of_int 3L; pre = PrE.top (); pred = Pred.of_loc f.vdecl; ctx = Ctx.top () } in - let tasks = Tasks.add (funs_ls, f_d) (ctx.global ()) in - ctx.sideg () tasks; - add_actions (List.map (fun f -> CreateErrorHandler ((Process, pname_ErrorHandler), f)) funs) - | _ -> failwith @@ "CreateErrorHandler: could not find out which functions are reachable from first argument!" - end - | "LAP_Se_GetErrorStatus", [status; r] -> todo () - | "LAP_Se_RaiseApplicationError", [error_code; message_addr; length; r] -> todo () - (* Not allowed: change configured schedule *) - | "LAP_Se_SetPriority", [pid; prio; r] -> todo () - | "LAP_Se_Replenish", [budget; r] -> todo () (* name used in docs *) - | "LAP_Se_ReplenishAperiodic", [budget; r] -> todo () (* name used in stdapi.c *) - | _ when is_arinc_fun -> failwith @@ "Function "^f.vname^" not handled!" - | _ -> d - - let query ctx (type a) (q: a Queries.t): a Queries.result = - (* let d = ctx.local in *) - match q with - (* had this query but nobody asked for it *) - (* | Queries.Priority _ -> - if Pri.is_int d.pri then Queries.ID.of_int IInt @@ BI.of_int64 @@ Option.get @@ Pri.to_int d.pri (* TODO: what ikind to use for priorities? *) - else if Pri.is_top d.pri then Queries.Result.top q else Queries.Result.bot q (* TODO: remove bot *) *) - (* | Queries.MayBePublic _ -> *) - (* `Bool ((PrE.to_int d.pre = Some 0L || PrE.to_int d.pre = None) && (not (mode_is_init d.pmo))) *) - | _ -> Queries.Result.top q - - let finalize () = - ArincUtil.print_actions (); - if Sys.file_exists "result" then ArincUtil.marshal @@ open_out_bin @@ "result/arinc.out"; - if GobConfig.get_bool "ana.arinc.simplify" then ArincUtil.simplify (); - if GobConfig.get_bool "ana.arinc.export" then ( - ArincUtil.save_dot_graph (); - ArincUtil.save_promela_model () - ); - if GobConfig.get_bool "ana.arinc.validate" then ArincUtil.validate () - - let startstate v = { pid = Pid.of_int 0L; pri = Pri.top (); per = Per.top (); cap = Cap.top (); pmo = Pmo.of_int 1L; pre = PrE.of_int 0L; pred = Pred.of_node (MyCFG.Function (emptyFunction "main")); ctx = Ctx.top () } - let exitstate v = D.bot () - - let threadenter ctx lval f args = - let d : D.t = ctx.local in - let tasks = ctx.global () in - (* TODO: optimize finding *) - let tasks_f = Tasks.filter (fun (fs,f_d) -> - Queries.LS.exists (fun (ls_f, _) -> ls_f = f) fs - ) tasks - in - let f_d = snd (Tasks.choose tasks_f) in - [{ f_d with pre = d.pre }] - - let threadspawn ctx lval f args fctx = ctx.local -end - -let _ = - MCP.register_analysis ~dep:["base"] (module Spec : MCPSpec) diff --git a/src/analyses/extract_arinc.ml b/src/analyses/extract_arinc.ml deleted file mode 100644 index 1275761c98..0000000000 --- a/src/analyses/extract_arinc.ml +++ /dev/null @@ -1,410 +0,0 @@ -(** Extract function calls and variables. *) - -open Prelude.Ana -open Analyses -module OList = List (* TODO get rid of *) -open BatteriesExceptionless - -module M = Messages - -module Spec = -struct - include Analyses.DefaultSpec - - let name () = "extract_arinc" - - let init () = - LibraryFunctions.add_lib_funs (Pml.special_funs ()) - - (* domains *) - (* Process ID *) - module Pid = IntDomain.Flattened - (* context hash for function calls *) - module Ctx = IntDomain.Flattened - (* set of predecessor nodes *) - module Pred = struct - include SetDomain.Make (Basetype.ExtractLocation) - let of_loc = singleton - let of_node = of_loc % Node.location - let of_current_node () = of_node @@ Option.get !MyCFG.current_node - let string_of_elt = Basetype.ExtractLocation.show - end - module D = Lattice.Prod3 (Pid) (Ctx) (Pred) - module C = D - module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (D)) (* set of created tasks to spawn when going multithreaded *) - module G = Tasks - module V = Printable.UnitConf (struct let name = "tasks" end) - - type pname = string (* process name *) - type fname = string (* function name *) - type id = pname * fname - type node = Cil.location - type action = Call of fname | Sys of string - type edge = node * action * node - - let extracted : (id, edge Set.t) Hashtbl.t = Hashtbl.create 123 - - let add_edge pid edge = - Hashtbl.modify_def Set.empty pid (Set.add edge) extracted - let get_edges pid = - Hashtbl.find_default extracted pid Set.empty - - (* tables for code generation *) - module SymTbl (G : sig type k end) = struct (* generate int id *) - let h : (G.k, 'v) Hashtbl.t = Hashtbl.create 13 - let get k = - Option.default_delayed (fun () -> - let v = List.length @@ List.of_enum @@ Hashtbl.keys h in - Hashtbl.replace h k v; - v) (Hashtbl.find h k) - let inv v = Hashtbl.enum h |> List.of_enum |> List.assoc_inv v - let to_list () = Hashtbl.enum h |> List.of_enum - end - - module Pids = SymTbl (struct type k = pname end) (* process name -> int id *) (* TODO remove and use Res instead? *) - module FunTbl = SymTbl (struct type k = fname*string end) (* function call (fname, target_label) -> int id *) - - module H (G : sig type k type v end) = struct - let h : (G.k, G.v) Hashtbl.t = Hashtbl.create 13 - let add k v = Hashtbl.replace h k v - let get k = Hashtbl.find h k - let inv v = Hashtbl.enum h |> List.of_enum |> List.assoc_inv v - end - - module Prios = H (struct type k = pname type v = int64 end) (* process name -> prio *) - module Pfuns = H (struct type k = pname type v = fname end) (* process name -> function name *) - - module Res = struct (* (resource_kind, resource_name) -> (varinfo_id, int_id) *) - let resources = Hashtbl.create 13 - let get (resource,name as k) = - Option.default_delayed (fun () -> - let vname = resource^":"^name in - let v = Goblintutil.create_var (makeGlobalVar vname voidPtrType) in - let i = Hashtbl.keys resources |> List.of_enum |> List.filter (fun x -> fst x = resource) |> List.length in - Hashtbl.replace resources k (v,i); - v,i) (Hashtbl.find resources k) - let inv_by f k = - Hashtbl.filter (fun k' -> f k' = k) resources |> Hashtbl.keys |> Enum.get - let inv_v = inv_by fst - let inv_i = inv_by snd - let i_by_v v = snd (get (Option.get_exn (inv_v v) (Invalid_argument ("No resource found for variable "^v.vname)))) - end - - (* code generation *) - let indent x = " "^x - let get_globals () = [] (* TODO *) - - let codegen_proc (pname, fname as id) = - let pid = string_of_int @@ Pids.get pname in - let pfun = Option.get @@ Pfuns.get pname in - print_endline @@ "### codegen_proc: "^pname^", "^fname^", "^pfun; - let is_proc = fname = pfun in - let spid = if is_proc then "P_"^pname else "F_"^fname in - let head = if is_proc then (* process *) - let prio = match Prios.get pname with Some x -> " priority "^Int64.to_string x | None -> "" in - "proctype "^pname^"(byte tid)"^prio^" provided (can_run("^pid^") PRIO"^pid^") {\n int stack[20]; int sp = -1;" - else (* some function call in process *) - "Fun_"^fname^":" - in - (* build adjacency matrix for all nodes of this process *) - let module HashtblN = Hashtbl.Make (ArincDomain.Pred.Base) in - let a2bs = HashtblN.create 97 in - Set.iter (fun (a, _, b as edge) -> HashtblN.modify_def Set.empty a (Set.add edge) a2bs) (get_edges id); - let nodes = HashtblN.keys a2bs |> List.of_enum in - (* let out_edges node = HashtblN.find_default a2bs node Set.empty |> Set.elements in (* Set.empty leads to Out_of_memory!? *) *) - let out_edges node = try HashtblN.find a2bs node |> Set.elements with Not_found -> [] in - let in_edges node = HashtblN.filter (Set.mem node % Set.map Tuple3.third) a2bs |> HashtblN.values |> List.of_enum |> List.concat_map Set.elements in - let is_end_node = List.is_empty % out_edges in - let is_start_node = List.is_empty % in_edges in - let start_node = OList.find is_start_node nodes in (* node with no incoming edges is the start node *) - let label n = spid ^ "_" ^ Pred.string_of_elt n in - let end_label = spid ^ "_end" in - let goto label = "goto " ^ label ^ ";" in - let codegen_edge (a, action, b) = - let target_label = if is_end_node b then end_label else label b in - let str_action = match action with - | Call fname -> - let pc = string_of_int @@ FunTbl.get (fname,target_label) in - "mark("^pc^"); " ^ goto ("Fun_"^fname) - | Sys x -> x - in - (* for function calls the goto will never be reached since the function's return will already jump to that label; however it's nice to see where the program will continue at the site of the call. *) - str_action ^ " " ^ goto target_label - in - let choice xs = List.map (fun x -> "::\t"^x ) xs in (* choices in if-statements are prefixed with :: *) - let walk_edges (a, out_edges) = - let edges = Set.elements out_edges |> List.map codegen_edge in - (label a ^ ":") :: - if List.compare_length_with edges 1 > 0 then - "if" :: (choice edges) @ ["fi"] - else - edges - in - let locals = [] in (* TODO *) - let body = locals @ goto (label start_node) :: (List.concat_map walk_edges (HashtblN.enum a2bs |> List.of_enum)) @ [end_label ^ ":" ^ if is_proc then " status[tid] = DONE" else " ret_"^fname^"()"] in - String.concat "\n" @@ head :: List.map indent body @ [if is_proc then "}\n" else ""] - - let codegen () = - let procs = Pids.to_list () in - Hashtbl.keys extracted |> List.of_enum |> List.iter (fun (pname, fname) -> print_endline @@ pname ^ "_" ^ fname); - let proc_defs = Hashtbl.keys extracted |> List.of_enum |> List.map codegen_proc in - let num_actions s = Hashtbl.values extracted |> Set.of_enum |> flip (Set.fold Set.union) Set.empty |> Set.filter (fun (_,a,_) -> match a with Sys a -> startsWith s a | _ -> false) |> Set.cardinal in - let has_error_handler = num_actions "CreateErrorHandler" > 0 in - let nproc = List.length procs + (if has_error_handler then 1 else 0) in (* +1 is init process *) - let nbboard = num_actions "CreateBlackboard" in - let nsema = num_actions "CreateSemaphore" in - let nevent = num_actions "CreateEvent" in - let run_processes = procs |> List.filter_map (fun (name, id) -> if name = "main" then None else Some (id, "run "^name^"("^string_of_int id^");")) |> List.sort (compareBy fst) |> List.map snd in - let init_body = - "status[0] = READY;" :: - "run main(0);" :: - "(partition_mode == NORMAL); // TODO assert that all resources were created, see postInit" :: - (*"run monitor();" ::*) - (if has_error_handler then "run ErrorHandler("^string_of_int (Pids.get "ErrorHandler")^")" else "// no ErrorHandler") :: - run_processes - in - (* used for macros oneIs, allAre, noneAre... *) - let checkStatus = "(" ^ (String.concat " op2 " @@ List.of_enum @@ (0 --^ nproc) /@ (fun i -> "status["^string_of_int i^"] op1 v")) ^ ")" in - (* generate priority based running constraints for each process (only used ifdef PRIOS): process can only run if no higher prio process is ready *) - let prios = - let def (pname,id) = - let pri = Prios.get pname in - let higher = List.filter (fun (n,_) -> Prios.get n > pri) procs in - if List.is_empty higher - then None - else Some ("#undef PRIO" ^ string_of_int id ^ "\n#define PRIO" ^ string_of_int id ^ String.concat "" @@ List.map (fun (_,i) -> " && status[" ^ string_of_int i ^ "] != READY") higher) - in - List.filter_map def procs - in - let fun_mappings = - let fun_map xs = - if List.is_empty xs then [] else - let (name,_),_ = OList.hd xs in - let entries = xs |> List.map (fun ((_,k),v) -> "\t:: (stack[sp] == " ^ string_of_int v ^ ") -> sp--; goto " ^ k ^" \\") in - let debug_str = if GobConfig.get_bool "ana.pml.debug" then "\t:: else -> printf(\"wrong pc on stack!\"); assert(false) " else "" in - ("#define ret_"^name^"() if \\") :: entries @ [debug_str ^ "fi"] - in - FunTbl.to_list () |> List.group (compareBy (fst%fst)) |> List.concat_map fun_map - in - String.concat "\n" @@ - ("#define nproc "^string_of_int nproc) :: - ("#define nbboard "^string_of_int nbboard) :: - ("#define nsema "^string_of_int nsema) :: - ("#define nevent "^string_of_int nevent) :: "" :: - ("#define checkStatus(op1, v, op2) "^checkStatus) :: "" :: - "#include \"arinc.os.pml\"" :: "" :: - "init {" :: List.map indent init_body @ "}" :: "" :: - (List.of_enum @@ (0 --^ nproc) /@ (fun i -> "#define PRIO" ^ string_of_int i)) @ - "#ifdef PRIOS" :: prios @ "#endif" :: - "" :: fun_mappings @ - "" :: get_globals () @ - proc_defs - - (* queries *) - let query ctx (type a) (q: a Queries.t) = - match q with - | _ -> Queries.Result.top q - (* transfer functions *) - let assign ctx (lval:lval) (rval:exp) : D.t = - ctx.local - - let branch ctx (exp:exp) (tv:bool) : D.t = - ctx.local - - let body ctx (f:fundec) : D.t = - match ctx.presub "base" with - | base -> - let pid, ctxh, pred = ctx.local in - let module BaseMain = (val Base.get_main ()) in - let base_context = BaseMain.context_cpa f @@ Obj.obj base in - let context_hash = Hashtbl.hash (base_context, pid) in - pid, Ctx.of_int (Int64.of_int context_hash), pred - | exception Not_found -> ctx.local (* TODO when can this happen? *) - - let return ctx (exp:exp option) (f:fundec) : D.t = - ctx.local - - let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - let d_caller = ctx.local in - let pid, ctxh, pred = ctx.local in - let d_callee = if D.is_bot ctx.local then ctx.local else pid, Ctx.top (), Pred.of_node (MyCFG.Function f) in (* set predecessor set to start node of function *) - [d_caller, d_callee] - - let combine ctx (lval:lval option) fexp (fd:fundec) (args:exp list) fc (au:D.t) : D.t = - if D.is_bot ctx.local || D.is_bot au then ctx.local else - let pid, ctxh, pred = ctx.local in (* caller *) - let _ , _, pred' = au in (* callee *) - (* check if the callee has some relevant edges, i.e. advanced from the entry point. if not, we generate no edge for the call and keep the predecessors from the caller *) - if Pred.is_bot pred' then failwith "d_callee.pred is bot!"; (* set should never be empty *) - if Pred.equal pred' (Pred.of_node (MyCFG.Function fd)) then - ctx.local - else ( - (* set current node as new predecessor, since something interesting happend during the call *) - pid, ctxh, Pred.of_node (Option.get !MyCFG.current_node ) - ) - - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = - if not (String.starts_with f.vname "LAP_Se_") then ctx.local else - let pid, ctx_hash, pred = ctx.local in - if Pid.is_bot pid || Ctx.is_bot ctx_hash || Pred.is_bot pred then ctx.local else - let pname = Pid.to_int pid |> Option.get |> Int64.to_int |> Pids.inv |> Option.get in - let fname = str_remove "LAP_Se_" f.vname in - let eval_int exp = - match ctx.ask (Queries.EvalInt exp) with - | x when Queries.ID.is_int x -> [IntOps.BigIntOps.to_string (Option.get @@ Queries.ID.to_int x)] - | _ -> failwith @@ "Could not evaluate int-argument "^sprint d_plainexp exp - in - let eval_str exp = - match ctx.ask (Queries.EvalStr exp) with - | `Lifted x -> [x] - | _ -> failwith @@ "Could not evaluate string-argument "^sprint d_plainexp exp - in - let eval_id exp = - let module LS = Queries.LS in - match ctx.ask (Queries.MayPointTo exp) with - | x when not (LS.is_top x) -> - let top_elt = dummyFunDec.svar, `NoOffset in - if LS.mem top_elt x then M.info ~category:Unsound "Query result for MayPointTo contains top!"; - let xs = LS.remove top_elt x |> LS.elements in - List.map (fun (v,o) -> string_of_int (Res.i_by_v v)) xs - | _ -> failwith @@ "Could not evaluate id-argument "^sprint d_plainexp exp - in - let assign_id exp id = - if M.tracing then M.trace "extract_arinc" "assign_id %a %s\n" d_exp exp id.vname; - match exp with - | AddrOf lval -> ctx.emit (Assign {lval; exp = mkAddrOf @@ var id}) - | _ -> failwith @@ "Could not assign id. Expected &id. Found "^sprint d_exp exp - in - (* evaluates an argument and returns a list of possible values for that argument. *) - let eval = function - | Pml.EvalSkip -> const None - | Pml.EvalInt -> fun e -> Some (try eval_int e with Failure _ -> eval_id e) - | Pml.EvalString -> fun e -> Some (List.map (fun x -> "\""^x^"\"") (eval_str e)) - | Pml.EvalEnum f -> fun e -> Some (List.map (fun x -> Option.get (f (int_of_string x))) (eval_int e)) - | Pml.AssignIdOfString (res, pos) -> fun e -> - (* evaluate argument at i as string *) - let name = OList.hd @@ eval_str (OList.at arglist pos) in - (* generate variable from it *) - let v,i = Res.get (res, name) in - (* assign generated variable in base *) - assign_id e v; - Some [string_of_int i] - in - let node = Option.get !MyCFG.current_node in - let fundec = Node.find_fundec node in - let id = pname, fundec.svar.vname in - let extract_fun ?(info_args=[]) args = - let comment = if List.is_empty info_args then "" else " /* " ^ String.concat ", " info_args ^ " */" in (* append additional info as comment *) - let action = fname^"("^String.concat ", " args^");"^comment in - print_endline @@ "EXTRACT in "^pname^": "^action; - Pred.iter (fun pred -> add_edge id (pred, Sys action, Node.location node)) pred; - pid, ctx_hash, Pred.of_node node - in - match fname, arglist with (* first some special cases *) - | "CreateProcess", [AddrOf attr; pid'; r] -> - let cm = match unrollType (Cilfacade.typeOfLval attr) with - | TComp (c,_) -> c - | _ -> failwith "type-error: first argument of LAP_Se_CreateProcess not a struct." - in - let struct_fail f x = - f @@ "LAP_Se_CreateProcess: problem with first argument: " ^ - begin match x with - | `Field ofs -> "cannot access field " ^ ofs - | `Result (name, entry_point, pri, per, cap) -> - "struct PROCESS_ATTRIBUTE_TYPE needs all of the following fields (with result): NAME ("^name^"), ENTRY_POINT ("^entry_point^"), BASE_PRIORITY ("^pri^"), PERIOD ("^per^"), TIME_CAPACITY ("^cap^")" - end ^ ". Running scrambled: "^string_of_bool Goblintutil.scrambled - in - let field ofs = - try Lval (addOffsetLval (Field (getCompField cm ofs, NoOffset)) attr) - with Not_found -> struct_fail failwith (`Field ofs) - in - let name = ctx.ask (Queries.EvalStr (field Goblintutil.arinc_name)) in - let entry_point = ctx.ask (Queries.ReachableFrom (AddrOf attr)) in - let pri = ctx.ask (Queries.EvalInt (field Goblintutil.arinc_base_priority)) in - let per = ctx.ask (Queries.EvalInt (field Goblintutil.arinc_period)) in - let cap = ctx.ask (Queries.EvalInt (field Goblintutil.arinc_time_capacity)) in - begin match name, entry_point, pri, per, cap with - | `Lifted name, ls, pri, per, cap when not (Queries.LS.is_top ls) - && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) && Queries.ID.is_int pri && Queries.ID.is_int per && Queries.ID.is_int cap -> - let pri = (IntOps.BigIntOps.to_int64 (Option.get @@ Queries.ID.to_int pri)) in - let funs_ls = Queries.LS.filter (fun (v,o) -> let lval = Var v, Lval.CilLval.to_ciloffs o in isFunctionType (Cilfacade.typeOfLval lval)) ls in (* do we need this? what happens if we spawn a variable that's not a function? shouldn't this check be in spawn? *) - if M.tracing then M.tracel "extract_arinc" "starting a thread %a with priority '%Ld' \n" Queries.LS.pretty funs_ls pri; - let funs = funs_ls |> Queries.LS.elements |> List.map fst |> List.unique in - let f_d = Pid.of_int (Int64.of_int (Pids.get name)), Ctx.top (), Pred.of_loc f.vdecl in - List.iter (fun f -> Pfuns.add name f.vname) funs; - Prios.add name pri; - let tasks = Tasks.add (funs_ls, f_d) (ctx.global ()) in - ctx.sideg () tasks; - let v,i = Res.get ("process", name) in - assign_id pid' v; - List.fold_left (fun d f -> extract_fun ~info_args:[f.vname] [string_of_int i]) ctx.local funs - | _ -> let f (type a) (x: a Queries.result) = "TODO" in struct_fail (M.debug ~category:Analyzer "%s") (`Result (f name, f entry_point, f pri, f per, f cap)); ctx.local (* TODO: f *) - end - | _ -> match Pml.special_fun fname with - | None -> M.info ~category:Unsound "extract_arinc: unhandled function %s" fname; ctx.local - | Some eval_args -> - if M.tracing then M.trace "extract_arinc" "extract %s, args: %i code, %i pml\n" f.vname (List.length arglist) (List.length eval_args); - let rec combine_opt f a b = match a, b with - | [], [] -> [] - | x::xs, y::ys -> (x,y) :: combine_opt f xs ys - | [], x::xs -> f None (Some x) :: combine_opt f [] xs - | x::xs, [] -> f (Some x) None :: combine_opt f xs [] - in - (* combine list of eval rules with list of arguments, fill with Skip *) - let combine_skip a b = combine_opt (curry @@ function None, Some e -> Pml.EvalSkip, e | _, _ -> assert false) a b in - print_endline @@ String.concat "; " @@ List.map (fun (e,a) -> Pml.show_eval e^", "^sprint d_exp a) (combine_skip eval_args arglist); - let args_eval = List.filter_map (uncurry eval) @@ combine_skip eval_args arglist in - List.iter (fun args -> assert (args <> [])) args_eval; (* arguments that are not skipped always need to evaluate to at least one value *) - print_endline @@ "arinc: FUN " ^ fname ^ " with args_eval " ^ String.concat "; " (List.map (String.concat ", ") args_eval); - let args_product = List.n_cartesian_product @@ args_eval in - print_endline @@ "arinc: FUN " ^ fname ^ " with args_product " ^ String.concat "; " (List.map (String.concat ", ") args_product); - List.fold_left (fun d args -> - (* some calls have side effects *) - begin match fname, args with - | "SetPartitionMode", "NORMAL"::_ -> - let tasks = ctx.global () in - ignore @@ printf "arinc: SetPartitionMode NORMAL: spawning %i processes!\n" (Tasks.cardinal tasks); - Tasks.iter (fun (fs,f_d) -> Queries.LS.iter (fun f -> ctx.spawn None (fst f) []) fs) tasks; - | "SetPartitionMode", x::_ -> failwith @@ "SetPartitionMode: arg "^x - | s, a -> print_endline @@ "arinc: FUN: "^s^"("^String.concat ", " a^")" - end; - let str_args, args = List.partition (flip String.starts_with "\"") args in (* strings can't be arguments, but we want them as a comment *) - extract_fun ~info_args:str_args args - ) ctx.local args_product - - let startstate v = Pid.of_int 0L, Ctx.top (), Pred.of_node (MyCFG.Function (emptyFunction "main")) - let exitstate v = D.bot () - - let init marshal = (* registers which functions to extract and writes out their definitions *) - init (); (* TODO: why wasn't this called before? *) - let mainfuns = GobConfig.get_string_list "mainfun" in - ignore @@ List.map Pids.get mainfuns; - ignore @@ List.map (fun name -> Res.get ("process", name)) mainfuns; - assert (List.compare_length_with mainfuns 1 = 0); (* TODO? *) - List.iter (fun fname -> Pfuns.add "main" fname) mainfuns; - if GobConfig.get_bool "ana.arinc.export" then output_file ~filename:Fpath.(to_string @@ Goblintutil.create_dir (v "result") / "arinc.os.pml") ~text:(snd (Pml_arinc.init ())) - - let finalize () = (* writes out collected cfg *) - (* TODO call Pml_arinc.init again with the right number of resources to find out of bounds accesses? *) - if GobConfig.get_bool "ana.arinc.export" then ( - let path = Fpath.(Goblintutil.create_dir (v "result") / "arinc.pml") in (* returns abs. path *) - output_file ~filename:(Fpath.to_string path) ~text:(codegen ()); - print_endline @@ "Model saved as " ^ (Fpath.to_string path); - print_endline "Run ./spin/check.sh to verify." - ) - - let threadenter ctx lval f args = - let tasks = ctx.global () in - (* TODO: optimize finding *) - let tasks_f = Tasks.filter (fun (fs,f_d) -> - Queries.LS.exists (fun (ls_f, _) -> ls_f = f) fs - ) tasks - in - let f_d = snd (Tasks.choose tasks_f) in - [f_d] - - let threadspawn ctx lval f args fctx = ctx.local -end - -let _ = - MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index bb6db9608a..c91be80248 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -163,7 +163,6 @@ let classify fn exps: categories = -> `Lock(true, true, true) | "pthread_mutex_trylock" | "pthread_rwlock_trywrlock" -> `Lock (true, true, false) - | "LAP_Se_WaitSemaphore" (* TODO: only handle those when arinc analysis is enabled? *) | "_spin_lock" | "_spin_lock_irqsave" | "_spin_lock_bh" | "down_write" | "mutex_lock" | "mutex_lock_interruptible" | "_write_lock" | "_raw_write_lock" | "pthread_rwlock_wrlock" | "GetResource" | "_raw_spin_lock" @@ -175,7 +174,6 @@ let classify fn exps: categories = | "pthread_rwlock_tryrdlock" | "pthread_rwlock_rdlock" | "_read_lock" | "_raw_read_lock" | "down_read" -> `Lock (get_bool "sem.lock.fail", false, true) - | "LAP_Se_SignalSemaphore" | "__raw_read_unlock" | "__raw_write_unlock" | "raw_spin_unlock" | "_spin_unlock" | "spin_unlock" | "_spin_unlock_irqrestore" | "_spin_unlock_bh" | "_raw_spin_unlock_bh" | "mutex_unlock" | "_write_unlock" | "_read_unlock" | "_raw_spin_unlock_irqrestore" @@ -576,10 +574,6 @@ let invalidate_actions = [ (* no args, declare invalidate actions to prevent invalidating globals *) "__VERIFIER_atomic_begin", readsAll; "__VERIFIER_atomic_end", readsAll; - (* prevent base from spawning ARINC processes early, handled by arinc/extract_arinc *) - (* "LAP_Se_SetPartitionMode", writes [2]; *) - "LAP_Se_CreateProcess", writes [2; 3]; - "LAP_Se_CreateErrorHandler", writes [2; 3]; "isatty", readsAll; "setpriority", readsAll; "getpriority", readsAll; diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 501c6f09b8..0609d9e199 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -73,7 +73,6 @@ struct ctx.emit (Events.Lock (verifier_atomic, true)) let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = - let is_activated a = List.mem a (GobConfig.get_string_list "ana.activated") in (* TODO: proper LibraryFunctions group selection *) let remove_rw x = x in let unlock remove_fn = match f.vname, arglist with @@ -83,11 +82,6 @@ struct ctx.split () [Events.Unlock (remove_fn e)] ) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg); raise Analyses.Deadcode - | "LAP_Se_SignalSemaphore", [Lval arg; _] when is_activated "arinc" || is_activated "extract_arinc" -> - List.iter (fun e -> - ctx.split () [Events.Unlock (remove_fn e)] - ) (eval_exp_addr (Analyses.ask_of_ctx ctx) (Cil.mkAddrOf arg)); - raise Analyses.Deadcode | _ -> failwith "unlock has multiple arguments" in let desc = LF.find f in @@ -102,9 +96,6 @@ struct | "spin_lock_irqsave", [arg; _] -> (*print_endline @@ "Mutex `Lock "^f.vname;*) lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arg - | "LAP_Se_WaitSemaphore", [Lval arg; _; _] when is_activated "arinc" || is_activated "extract_arinc" -> - (*print_endline @@ "Mutex `Lock "^f.vname;*) - lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv (Cil.mkAddrOf arg) | _ -> failwith "lock has multiple arguments" end | Unlock _, "__raw_read_unlock" diff --git a/src/cdomains/arincDomain.ml b/src/cdomains/arincDomain.ml deleted file mode 100644 index 3cce7f0315..0000000000 --- a/src/cdomains/arincDomain.ml +++ /dev/null @@ -1,74 +0,0 @@ -open Prelude - -(* Information for one task *) -(* Process ID *) -module Pid = IntDomain.Flattened -(* Priority *) -module Pri = IntDomain.Reverse (IntDomain.Lifted) (* TODO reverse? *) -(* Period *) -module Per = IntDomain.Flattened -(* Capacity *) -module Cap = IntDomain.Flattened - -(* Information for all tasks *) -(* Partition mode *) -module Pmo = IntDomain.Flattened -(* Preemption lock *) -module PrE = IntDomain.Flattened -(* context hash for function calls *) -module Ctx = IntDomain.Flattened -(* predecessor nodes *) -module Pred = struct - module Base = Basetype.ExtractLocation - include SetDomain.Make (Base) - let of_loc = singleton - let of_node = of_loc % Node.location - let of_current_node () = of_node @@ Option.get !MyCFG.current_node - let string_of_elt = Basetype.ExtractLocation.show -end - -(* define record type here so that fields are accessable outside of D *) -type process = { pid: Pid.t; pri: Pri.t; per: Per.t; cap: Cap.t; pmo: Pmo.t; pre: PrE.t; pred: Pred.t; ctx: Ctx.t } [@@deriving eq, ord, hash, to_yojson] - -module D = -struct - type t = process [@@deriving eq, ord, hash, to_yojson] - include Printable.Std - - let name () = "ARINC state" - - (* printing *) - let show x = Printf.sprintf "{ pid=%s; pri=%s; per=%s; cap=%s; pmo=%s; pre=%s; pred=%s; ctx=%s }" (Pid.show x.pid) (Pri.show x.pri) (Per.show x.per) (Cap.show x.cap) (Pmo.show x.pmo) (PrE.show x.pre) (Pretty.sprint ~width:200 (Pred.pretty () x.pred)) (Ctx.show x.ctx) - include Printable.SimpleShow (struct - type nonrec t = t - let show = show - end) - - (* modify fields *) - let pid f d = { d with pid = f d.pid } - let pri f d = { d with pri = f d.pri } - let per f d = { d with per = f d.per } - let cap f d = { d with cap = f d.cap } - let pmo f d = { d with pmo = f d.pmo } - let pre f d = { d with pre = f d.pre } - let pred f d = { d with pred = f d.pred } - - let bot () = { pid = Pid.bot (); pri = Pri.bot (); per = Per.bot (); cap = Cap.bot (); pmo = Pmo.bot (); pre = PrE.bot (); pred = Pred.bot (); ctx = Ctx.bot () } - let is_bot x = x = bot () - let is_bot1 x = Pid.is_bot x.pid || Pri.is_bot x.pri || Per.is_bot x.per || Cap.is_bot x.cap || Pmo.is_bot x.pmo || PrE.is_bot x.pre || Pred.is_bot x.pred - let top () = { pid = Pid.top (); pri = Pri.top (); per = Per.top (); cap = Cap.top (); pmo = Pmo.top (); pre = PrE.top (); pred = Pred.top (); ctx = Ctx.top () } - let is_top x = Pid.is_top x.pid && Pri.is_top x.pri && Per.is_top x.per && Cap.is_top x.cap && Pmo.is_top x.pmo && PrE.is_top x.pre && Pred.is_top x.pred && Ctx.is_top x.ctx - - let leq x y = Pid.leq x.pid y.pid && Pri.leq x.pri y.pri && Per.leq x.per y.per && Cap.leq x.cap y.cap && Pmo.leq x.pmo y.pmo && PrE.leq x.pre y.pre && Pred.leq x.pred y.pred && Ctx.leq x.ctx y.ctx - let op_scheme op1 op2 op3 op4 op5 op6 op7 op8 x y: t = { pid = op1 x.pid y.pid; pri = op2 x.pri y.pri; per = op3 x.per y.per; cap = op4 x.cap y.cap; pmo = op5 x.pmo y.pmo; pre = op6 x.pre y.pre; pred = op7 x.pred y.pred; ctx = op8 x.ctx y.ctx } - let join x y = let r = op_scheme Pid.join Pri.join Per.join Cap.join Pmo.join PrE.join Pred.join Ctx.join x y in - (* let s x = if is_top x then "TOP" else if is_bot x then "BOT" else short 0 x in M.debug @@ "JOIN\t" ^ if equal x y then "EQUAL" else s x ^ "\n\t" ^ s y ^ "\n->\t" ^ s r; *) - if Pred.cardinal r.pred > 5 then (Messages.debug ~category:Analyzer "Pred.cardinal r.pred = %d with value %a" (Pred.cardinal r.pred) pretty r(* ; failwith "STOP" *)); - r - let widen = join - let meet = op_scheme Pid.meet Pri.meet Per.meet Cap.meet Pmo.meet PrE.meet Pred.meet Ctx.meet - let narrow = meet - - let pretty_diff () (x,y) = - Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y -end diff --git a/src/dune b/src/dune index d15dc7dabc..47ecda217f 100644 --- a/src/dune +++ b/src/dune @@ -7,7 +7,7 @@ (name goblint_lib) (public_name goblint.lib) (wrapped false) - (modules :standard \ goblint mainarinc mainspec privPrecCompare apronPrecCompare messagesCompare) + (modules :standard \ goblint mainspec privPrecCompare apronPrecCompare messagesCompare) (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. @@ -49,10 +49,10 @@ (copy_files# witness/z3/*.ml) (executables - (names goblint mainarinc mainspec) - (public_names goblint - -) + (names goblint mainspec) + (public_names goblint -) (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes - (modules goblint mainarinc mainspec) + (modules goblint mainspec) (libraries goblint.lib goblint.sites.dune) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall) diff --git a/src/main.camldoc b/src/main.camldoc index 00d85110c4..ec08a14a7b 100644 --- a/src/main.camldoc +++ b/src/main.camldoc @@ -78,7 +78,6 @@ ShapeDomain ListDomain BaseDomain -ArincDomain ConcDomain ContainDomain EscapeDomain @@ -109,7 +108,6 @@ MCP Base Spec -Arinc CondVars Contain Deadlock diff --git a/src/mainarinc.ml b/src/mainarinc.ml deleted file mode 100644 index 8d117c8506..0000000000 --- a/src/mainarinc.ml +++ /dev/null @@ -1,17 +0,0 @@ -open Prelude -open GobConfig - -let save_all ch = - ArincUtil.unmarshal ch; - ArincUtil.print_actions (); - ArincUtil.save_dot_graph (); - ArincUtil.save_promela_model () - -let _ = - let conf, cin = match Array.to_list Sys.argv with - | [_; conf; "-"] -> conf, stdin - | [_; conf; path] -> conf, open_in_bin path - | _ -> print_endline @@ "usage: " ^ Sys.argv.(0) ^ " "; exit 1 - in - merge_file (Fpath.v conf); - save_all cin diff --git a/src/util/arincUtil.ml b/src/util/arincUtil.ml deleted file mode 100644 index edd6f3da60..0000000000 --- a/src/util/arincUtil.ml +++ /dev/null @@ -1,411 +0,0 @@ -open Prelude -open Cil -(* we don't want to use M.debug because everything here should be done after the analysis, so the location would be some old value for all invocations *) -let debug_each msg = print_endline @@ MessageUtil.colorize ~fd:Unix.stdout @@ "{blue}"^msg - -(* ARINC types and Hashtables for collecting CFG *) -type resource = Process | Function | Semaphore | Event | Logbook | SamplingPort | QueuingPort | Buffer | Blackboard [@@deriving show { with_path = false }] -(* id is resource type and name, there is a 1:1 mapping to varinfo in the analysis used for assignments *) -type id = resource*string [@@deriving show] -let infinity = 4294967295L (* time value used for infinity *) -type time = int64 [@printer fun fmt t -> Format.(if t = infinity then fprintf fmt "∞" else fprintf fmt "%Ldns" t)] [@@deriving show] - -(* map int values to enum names *) -type partition_mode = Idle | Cold_Start | Warm_Start | Normal [@@deriving show { with_path = false }, enum] -let show_partition_mode_opt = String.uppercase % Option.default "Unknown!" % Option.map show_partition_mode -let mode_is f i = match Option.bind (ArincDomain.Pmo.to_int i) (partition_mode_of_enum % Int64.to_int) with Some x -> f x | None -> false -let mode_is_init = mode_is (function Cold_Start | Warm_Start -> true | _ -> false) -let mode_is_multi = mode_is (function Normal -> true | _ -> false) -type queuing_discipline = Fifo | Prio [@@deriving show { with_path = false }, enum] -let string_of_queuing_discipline = String.uppercase % Option.default "Unknown!" % Option.map show_queuing_discipline % queuing_discipline_of_enum % Int64.to_int -(* return code data type *) -type return_code = (* taken from ARINC_653_part1.pdf page 46 *) - | NO_ERROR (* request valid and operation performed *) - | NO_ACTION (* system’s operational status unaffected by request *) - | NOT_AVAILABLE (* the request cannot be performed immediately *) - | INVALID_PARAM (* parameter specified in request invalid *) - | INVALID_CONFIG (* parameter specified in request incompatible with current configuration (e.g., as specified by system integrator) *) - | INVALID_MODE (* request incompatible with current mode of operation *) - | TIMED_OUT (* time-out associated with request has expired *) -[@@deriving show { with_path = false }, enum] - -let pname_ErrorHandler = "ErrorHandler" - -module Action = (* encapsulate types because some process field names are also used for D.t -> use local opening of modules (since OCaml 4.00) for output *) -struct - type process = { pid: id; f: CilType.Varinfo.t; pri: int64; per: time; cap: time } [@@deriving show] - type semaphore = { sid: id; cur: int64; max: int64; queuing: int64 } [@@deriving show] -end -type action = - | Nop - | Cond of string * string - | Assign of string * string (* var_callee = var_caller *) - | Call of string - | LockPreemption | UnlockPreemption | SetPartitionMode of partition_mode option - | CreateProcess of Action.process | CreateErrorHandler of id * CilType.Varinfo.t | Start of id | Stop of id | Suspend of id | SuspendSelf of id * time | Resume of id - | CreateBlackboard of id | DisplayBlackboard of id | ReadBlackboard of id * time | ClearBlackboard of id - | CreateSemaphore of Action.semaphore | WaitSemaphore of id * time | SignalSemaphore of id - | CreateEvent of id | WaitEvent of id * time | SetEvent of id | ResetEvent of id - | TimedWait of time | PeriodicWait [@@deriving show { with_path = false }] -type node = ArincDomain.Pred.Base.t -let string_of_node = ArincDomain.Pred.string_of_elt -type edge = node * action * string option * node -let action_of_edge (_, action, _, _) = action -type edges = (id, edge Set.t) Hashtbl.t -let edges = ref (Hashtbl.create 199 : edges) -let get_a (a,_,_,_) = a -let get_b (_,_,_,b) = b - -let marshal ch = Marshal.to_channel ch !edges [] -let unmarshal ch = edges := Marshal.from_channel ch - -let get_edges (pid:id) : edge Set.t = - Hashtbl.find_default !edges pid Set.empty -let add_edge (pid:id) edge = - Hashtbl.modify_def Set.empty pid (Set.add edge) !edges - -let filter_map_actions p = - let all_edges = Hashtbl.values !edges |> List.of_enum |> List.concat_map Set.elements in - List.filter_map (p%action_of_edge) all_edges - -let filter_actions p = - (* filter_map_actions (Option.filter p % Option.some) *) - filter_map_actions (fun x -> if p x then Some x else None) - -let funs_for_process id : varinfo list = - let get_funs = function - | CreateProcess x when x.Action.pid=id -> Some x.Action.f - | CreateErrorHandler (id', f) when id'=id -> Some f - | _ -> None - in - filter_map_actions get_funs |> List.unique - -module type GenSig = sig type k type v val getNew: v Enum.t -> v end -module type SymTblSig = sig type k type v val get: k -> v val to_list: unit -> (k*v) list end -module SymTbl (Gen: GenSig) : SymTblSig with type k = Gen.k and type v = Gen.v = -struct - type k = Gen.k - type v = Gen.v - let h = (Hashtbl.create 123 : (k, v) Hashtbl.t) - let get k = - try Hashtbl.find h k - with Not_found -> - let v = Gen.getNew (Hashtbl.values h) in - Hashtbl.replace h k v; - v - let to_list () = Hashtbl.enum h |> List.of_enum -end - -(* this is just used to make sure that every var that is read has been written before *) -let return_vars = (Hashtbl.create 100 : (id * [`Read | `Write], string Set.t) Hashtbl.t) -let add_return_var pid kind var = Hashtbl.modify_def Set.empty (pid, kind) (Set.add var) return_vars -let get_return_vars pid kind = - if fst pid <> Process then failwith "get_return_vars: tried to get var for Function, but vars are saved per Process!" else - Hashtbl.find_default return_vars (pid, kind) Set.empty -let decl_return_vars xs = Set.elements xs |> List.map (fun vname -> "mtype " ^ vname ^ ";") -let is_global vname = startsWith "G" vname -let get_locals pid = Set.union (get_return_vars pid `Read) (get_return_vars pid `Write) |> Set.filter (neg is_global) |> decl_return_vars -let flatten_set xs = Set.fold Set.union xs Set.empty -let get_globals () = Hashtbl.values return_vars |> Set.of_enum |> flatten_set |> Set.filter is_global |> decl_return_vars - -(* ARINC output *) -(* console and dot *) -let str_resource id = - let str_funs fs = "["^(List.map CilType.Varinfo.show fs |> String.concat ", ")^"]" in - match id with - | Process, "mainfun" -> - "mainfun/["^String.concat ", " (GobConfig.get_string_list "mainfun")^"]" - | Process, name -> - name^"/"^str_funs @@ funs_for_process id - | resource_type, name -> - name -let str_resources ids = "["^(String.concat ", " @@ List.map str_resource ids)^"]" -let str_action pid = function - | Cond (r, cond) -> "If "^cond - | SetPartitionMode m -> "SetPartitionMode "^show_partition_mode_opt m - | CreateProcess x -> - Action.("CreateProcess "^str_resource x.pid^" (fun "^CilType.Varinfo.show x.f^", prio "^Int64.to_string x.pri^", period "^show_time x.per^", capacity "^show_time x.cap^")") - | CreateErrorHandler (id, funs) -> "CreateErrorHandler "^str_resource id - | CreateSemaphore x -> - Action.("CreateSemaphore "^str_resource x.sid^" ("^Int64.to_string x.cur^"/"^Int64.to_string x.max^", "^string_of_queuing_discipline x.queuing^")") - | a -> show_action a -let str_return_code = function Some r -> " : " ^ r | None -> "" -(* spin/promela *) -let pml_resources = Hashtbl.create 13 -let _ = Hashtbl.add pml_resources (Process, "mainfun") 0L -let id_pml id = (* give id starting from 0 (get_pid_by_id for all resources) *) - let resource, name as k = id in - try Hashtbl.find pml_resources k - with Not_found -> - let ids = Hashtbl.filteri (fun (r,n) v -> r=resource) pml_resources |> Hashtbl.values in - let id = if Enum.is_empty ids then 0L else Int64.succ (Enum.arg_max identity ids) in - Hashtbl.replace pml_resources k id; - id -let str_id_pml id = Int64.to_string @@ id_pml id -let str_pid_pml id = (if fst id = Process then "P" else "F") ^ str_id_pml id (* process or function *) -let str_ids_pml ids f = String.concat " " (List.map (f%str_id_pml) ids) -(* let ref_apply f r = r := f !r *) -let unset_ret_vars = ref Set.empty -let undef_funs = ref Set.empty -let action_may_fail = function - | SuspendSelf _ | ReadBlackboard _ | WaitSemaphore _ | WaitEvent _ -> true - | _ -> false -(* TODO also may_fail b/c they have timeout but missing above (b/c they don't affect the status of the modelled system (e.g. communication with outside)): - * {Send,Receive}QueuingMessage - * {Send,Receive}Buffer -*) -let str_action_pml pid r action = - let action_str = - match action with - | Nop -> "tmp = 0;" - | Cond (r, cond) -> - (* if the return var that is branched on was never set, we warn about it at the end and just leave out the condition, which leads to non-det. branching, i.e. the same behaviour as if it was set to top. TODO: this is not precise for globals, since those are initialized with 0. *) - if not @@ Set.mem r (get_return_vars pid `Write) then ( - unset_ret_vars := Set.add r !unset_ret_vars; "" - ) else if cond = "true" then "" else cond ^ " -> " - | Assign (lhs, rhs) -> (* for function parameters this is callee = caller *) - (* if the lhs is never read, we don't need to do anything *) - if not @@ Set.mem lhs (get_return_vars pid `Read) then "" - else lhs^" = "^rhs^";" - | Call fname -> - (* we shouldn't have calls to functions without edges! *) - if Hashtbl.mem !edges (Function, fname) then "goto Fun_"^fname^";" else (undef_funs := Set.add fname !undef_funs; "") - | LockPreemption -> "LockPreemption();" - | UnlockPreemption -> "UnlockPreemption();" - | SetPartitionMode i -> "SetPartitionMode("^show_partition_mode_opt i^");" - | CreateProcess x -> - Action.("CreateProcess("^str_id_pml x.pid^", "^Int64.to_string x.pri^", "^Int64.to_string x.per^", "^Int64.to_string x.cap^"); /* "^str_resource x.pid^" (prio "^Int64.to_string x.pri^", period "^show_time x.per^", capacity "^show_time x.cap^") */") - | CreateErrorHandler (id, f) -> "CreateErrorHandler("^str_id_pml id^");" - | Start id -> "Start("^str_id_pml id^");" - | Stop id -> "Stop("^str_id_pml id^");" - | Suspend id -> "Suspend("^str_id_pml id^");" - | SuspendSelf (id, timeout) -> "Suspend("^str_id_pml id^");" - | Resume id -> "Resume("^str_id_pml id^");" - | CreateBlackboard id -> "CreateBlackboard("^str_id_pml id^");" - | DisplayBlackboard id -> "DisplayBlackboard("^str_id_pml id^");" - | ReadBlackboard (id, timeout) -> "ReadBlackboard("^str_id_pml id^");" - | ClearBlackboard id -> "ClearBlackboard("^str_id_pml id^");" - | CreateSemaphore x -> - Action.("CreateSemaphore("^str_id_pml x.sid^", "^Int64.to_string x.cur^", "^Int64.to_string x.max^", "^string_of_queuing_discipline x.queuing^");") - | WaitSemaphore (id, timeout) -> "WaitSemaphore("^str_id_pml id^");" - | SignalSemaphore id -> "SignalSemaphore("^str_id_pml id^");" - | CreateEvent id -> "CreateEvent("^str_id_pml id^");" - | WaitEvent (id, timeout) -> "WaitEvent("^str_id_pml id^");" - | SetEvent id -> "SetEvent("^str_id_pml id^");" - | ResetEvent id -> "ResetEvent("^str_id_pml id^");" - | TimedWait t -> "TimedWait("^Int64.to_string t^");" - | PeriodicWait -> "PeriodicWait();" - in - match r with - | Some r when action_may_fail action (* when Set.mem r (get_return_vars pid `Read) *) -> "if :: "^action_str^" "^r^" = SUCCESS :: "^r^" = ERROR fi;" - | Some r -> action_str^" "^r^" = SUCCESS;" - | None -> action_str - -(* helpers *) -let find_option p xs = try Some (List.find p xs) with Not_found -> None (* why is this in batteries for Hashtbl but not for List? *) - -(* simplify graph here, i.e. merge functions which consist of the same edges and contract call chains *) -let simplify () = - let dups = Hashtbl.enum !edges |> List.of_enum |> List.group (compareBy ~cmp:Set.compare snd) |> List.filter_map (function x::y::ys -> Some (x, y::ys) | _ -> None) in - let replace_call oldname newname = - (* debug_each @@ "Replacing function calls to "^oldname^" with "^newname; *) - let f = function - | a, Call x, r, b when x = oldname -> a, Call newname, r, b - | x -> x - in - Hashtbl.map_inplace (fun _ v -> Set.map f v) !edges - in - let merge ((res,name),_) xs = - if res = Process then failwith "There should be no processes with duplicate content!" else - (* replace calls to the other functions with calls to name and remove them *) - List.iter (fun (k,_) -> - replace_call (snd k) name; - Hashtbl.remove_all !edges k - ) xs - in - List.iter (uncurry merge) dups; - (* contract call chains: replace functions which only contain another call *) - let rec contract_call_chains () = - let single_calls = Hashtbl.filter_map (fun (res,_) v -> match Set.choose v with _, Call name, _, _ when Set.cardinal v = 1 && res = Function -> Some (Function, name) | _ -> None) !edges in - let last_calls = Hashtbl.filteri (fun k v -> not @@ Hashtbl.mem single_calls v) single_calls in - Hashtbl.iter (fun k v -> - replace_call (snd k) (snd v); - Hashtbl.remove_all !edges k - ) last_calls; - if Hashtbl.length single_calls > 0 then contract_call_chains () - in contract_call_chains () - -(* output warnings *) -let validate () = - debug_each @@ "Validating arinc graph..."; - if neg Set.is_empty !undef_funs then ( - debug_each "The following functions are called, but have no edges:"; - Set.iter (fun fname -> debug_each @@ "call to undefined function " ^ fname) !undef_funs - ); - (* search for multi-edges (might appear for call-edges with intermediate context hash) *) - let warn_multi_edge id s = - Set.to_list s |> List.group (compareBy (fun x -> get_a x, get_b x)) |> List.filter ((>) 1 % List.length) - |> List.iter (fun xs -> let x = List.hd xs in debug_each @@ str_resource id ^ ": Found " ^ string_of_int (List.length xs) ^" multi-edges between " ^ string_of_node (get_a x) ^ " and " ^ string_of_node (get_b x) ^ ": [" ^ String.concat ", " (List.map (str_action id % action_of_edge) xs) ^ "]") - in - Hashtbl.iter (fun k v -> warn_multi_edge k v) !edges; - if neg Set.is_empty !unset_ret_vars then ( - debug_each "The following return code variables have never been set by arinc functions or assignments (conditions for these variables are ignored):"; (* this probably shouldn't happen in the input program - at least for local variables... *) - Set.iter (fun var -> debug_each @@ "branching on unset return var " ^ var) !unset_ret_vars - ) - -(* print to stdout *) -let print_actions () = - let print_process pid = - let str_node = string_of_node in - let str_edge (a, action, r, b) = str_node a ^ " -> " ^ str_action pid action ^ str_return_code r ^ " -> " ^ str_node b in - let xs = Set.map str_edge (get_edges pid) in - debug_each @@ str_resource pid^" ->\n\t"^String.concat "\n\t" (Set.elements xs) - in - Hashtbl.keys !edges |> Enum.iter print_process - -(* helper for exporting results *) -let save_result desc ext content = (* output helper *) - let dir = Goblintutil.create_dir (Fpath.v "result") in (* returns abs. path *) - let path = Fpath.(add_ext ext (dir / "arinc")) in - output_file ~filename:(Fpath.to_string path) ~text:content; - print_endline @@ "saved " ^ desc ^ " as " ^ (Fpath.to_string path) - -let save_dot_graph () = - let dot_process pid = - (* 1 -> w1 [label="fopen(_)"]; *) - let str_node x = "\"" ^ str_pid_pml pid ^ "_" ^ string_of_node x ^ "\"" in (* quote node names for dot *) - let str_edge (a, action, r, b) = str_node a ^ "\t->\t" ^ str_node b ^ "\t[label=\"" ^ str_action pid action ^ str_return_code r ^ "\"]" in - let xs = Set.map str_edge (get_edges pid) |> Set.elements in - ("subgraph \"cluster_"^str_resource pid^"\" {") :: xs @ ("label = \""^str_resource pid^"\";") :: ["}\n"] - in - let lines = Hashtbl.keys !edges |> List.of_enum |> List.concat_map dot_process in - let dot_graph = String.concat "\n " ("digraph file {"::lines) ^ "\n}" in - save_result "graph" "dot" dot_graph - -module FunTbl = SymTbl (struct type k = string*string type v = int let getNew xs = List.length @@ List.of_enum xs end) -let save_promela_model () = - let open Action in (* needed to distinguish the record field names from the ones of D.t *) - let indent s = "\t"^s in - let procs = List.unique @@ filter_map_actions (function CreateProcess x -> Some x | _ -> None) in - let has_error_handler = not @@ List.is_empty @@ filter_actions (function CreateErrorHandler _ -> true | _ -> false) in - let bboards = List.unique @@ filter_map_actions (function CreateBlackboard id -> Some id | _ -> None) in - let semas = List.unique @@ filter_map_actions (function CreateSemaphore x -> Some x | _ -> None) in - let events = List.unique @@ filter_map_actions (function CreateEvent id -> Some id | _ -> None) in - let nproc = List.length procs + 1 + (if has_error_handler then 1 else 0) in (* +1 is init process *) - let nbboard = List.length bboards in - let nsema = List.length semas in - let nevent = List.length events in - let run_processes = List.map (fun x -> let name = snd x.pid in let id = id_pml x.pid in id, "run "^name^"("^Int64.to_string id^");") procs |> List.sort (compareBy fst) |> List.map snd in - let init_body = - "preInit;" :: - "run mainfun(0);" :: (* keep mainfun as name for init process? *) - "postInit();" :: - "run monitor();" :: - (if has_error_handler then "run ErrorHandler("^str_id_pml (Process, "ErrorHandler")^")" else "// no ErrorHandler") :: - run_processes - in - let current_pname = ref "" in - let called_funs_done = ref Set.empty in - let rec process_def id = - if fst id = Function && Set.mem (snd id) !called_funs_done then [] else (* if we already generated code for this function, we just return [] *) - let iid = id_pml id in (* id is type*name, iid is int64 (starting from 0 for each type of resource) *) - let spid = str_pid_pml id in (* string for id (either Function or Process) *) - (* set the name of the current process (this function is also run for functions, which need a reference to the process for checking branching on return vars) *) - if fst id = Process then current_pname := snd id; - (* for a process we start with no called functions, for a function we add its name *) - called_funs_done := if fst id = Process then Set.empty else Set.add (snd id) !called_funs_done; - (* build adjacency matrix for all nodes of this process *) - let module HashtblN = Hashtbl.Make (ArincDomain.Pred.Base) in - let a2bs = HashtblN.create 97 in - Set.iter (fun (a, _, _, b as edge) -> HashtblN.modify_def Set.empty a (Set.add edge) a2bs) (get_edges id); - let nodes = HashtblN.keys a2bs |> List.of_enum in - (* let out_edges node = HashtblN.find_default a2bs node Set.empty |> Set.elements in (* Set.empty leads to Out_of_memory!? *) *) - let out_edges node = try HashtblN.find a2bs node |> Set.elements with Not_found -> [] in - let in_edges node = HashtblN.filter (Set.mem node % Set.map get_b) a2bs |> HashtblN.values |> List.of_enum |> List.concat_map Set.elements in - let is_end_node = List.is_empty % out_edges in - let is_start_node = List.is_empty % in_edges in - let start_node = List.find is_start_node nodes in (* node with no incoming edges is the start node *) - (* let str_nodes xs = "{"^(List.map string_of_node xs |> String.concat ",")^"}" in *) - let label n = spid ^ "_" ^ string_of_node n in - let end_label = spid ^ "_end" in - let goto node = "goto " ^ label node in - let called_funs = ref [] in - let str_edge (a, action, r, b) = - let target_label = if is_end_node b then end_label else label b in - let mark = match action with - | Call fname -> - called_funs := fname :: !called_funs; - let pc = string_of_int @@ FunTbl.get (fname,target_label) in "mark("^pc^"); " - | _ -> "" - in - (* for function calls the goto will never be reached since the function's return will already jump to that label; however it's nice to see where the program will continue at the site of the call. *) - mark ^ str_action_pml (Process, !current_pname) r action ^ " goto " ^ target_label - in - let choice xs = List.map (fun x -> "::\t"^x ) xs in (* choices in if-statements are prefixed with :: *) - let walk_edges (a, out_edges) = - let edges = Set.elements out_edges |> List.map str_edge in - (label a ^ ":") :: - if List.compare_length_with edges 1 > 0 then - "if" :: (choice edges) @ ["fi"] - else - edges - in - let locals = if not @@ GobConfig.get_bool "ana.arinc.assume_success" && fst id = Process then get_locals id else [] in - let body = locals @ goto start_node :: (List.concat_map walk_edges (HashtblN.enum a2bs |> List.of_enum)) @ [end_label ^ ":" ^ if fst id = Process then " status[id] = DONE" else " ret_"^snd id^"()"] in - let head = match id with - | Process, name -> - let proc = find_option (fun x -> x.pid=id) procs in (* None for mainfun *) - let priority = match proc with Some proc -> " priority "^Int64.to_string proc.pri | _ -> "" in - "proctype "^name^"(byte id)"^priority^" provided (canRun("^Int64.to_string iid^") PRIO"^Int64.to_string iid^") {\nint stack[20]; int sp = -1;" - | Function, name -> - "Fun_"^name^":" - | _ -> failwith "Only Process and Function are allowed as keys for collecting ARINC actions" - in - let called_fun_ids = List.map (fun fname -> Function, fname) !called_funs in - let funs = List.concat_map process_def called_fun_ids in - "" :: head :: List.map indent body @ funs @ [if fst id = Process then "}" else ""] - in - (* used for macros oneIs, allAre, noneAre... *) - let checkStatus = "(" ^ (String.concat " op2 " @@ List.of_enum @@ (0 --^ nproc) /@ (fun i -> "status["^string_of_int i^"] op1 v")) ^ ")" in - let allTasks = "(" ^ (String.concat " && " @@ List.of_enum @@ (0 --^ nproc) /@ (fun i -> "prop("^string_of_int i^")")) ^ ")" in - (* generate priority based running constraints for each process (only used ifdef PRIOS): process can only run if no higher prio process is ready *) - let prios = - let def proc = - let id = str_id_pml proc.pid in - let pri = proc.pri in - let higher = List.filter (fun x -> x.pri > pri) procs in - if List.is_empty higher - then None - else Some ("#undef PRIO" ^ id ^ "\n#define PRIO" ^ id ^ String.concat "" @@ List.map (fun x -> " && status[" ^ str_id_pml x.pid ^ "] != READY") higher) - in - List.filter_map def procs - in - (* sort definitions so that inline functions come before the processes *) - let process_defs = Hashtbl.keys !edges |> List.of_enum |> List.filter (fun id -> fst id = Process) |> List.sort (compareBy str_pid_pml) |> List.concat_map process_def in - let fun_mappings = - let fun_map xs = - if List.is_empty xs then [] else - let (name,_),_ = List.hd xs in - let entries = xs |> List.map (fun ((_,k),v) -> "\t:: (stack[sp] == " ^ string_of_int v ^ ") -> sp--; goto " ^ k ^" \\") in - let debug_str = if GobConfig.get_bool "ana.pml.debug" then "\t:: else -> printf(\"wrong pc on stack!\"); assert(false) " else "" in - ("#define ret_"^name^"() if \\") :: entries @ [debug_str ^ "fi"] - in - FunTbl.to_list () |> List.group (compareBy (fst%fst)) |> List.concat_map fun_map - in - let promela = String.concat "\n" @@ - ("#define nproc "^string_of_int nproc) :: - ("#define nbboard "^string_of_int nbboard) :: - ("#define nsema "^string_of_int nsema) :: - ("#define nevent "^string_of_int nevent) :: "" :: - ("#define checkStatus(op1, v, op2) "^checkStatus) :: "" :: - ("#define allTasks(prop) "^allTasks) :: "" :: - "#include \"arinc.base.pml\"" :: "" :: - "init {" :: List.map indent init_body @ "}" :: "" :: - (List.of_enum @@ (0 --^ nproc) /@ (fun i -> "#define PRIO" ^ string_of_int i)) @ - "#ifdef PRIOS" :: prios @ "#endif" :: - "" :: fun_mappings @ - "" :: get_globals () @ - process_defs - in - save_result "promela model" "pml" promela; - print_endline ("Copy spin/arinc_base.pml to same folder and then do: spin -a arinc.pml && cc -o pan pan.c && ./pan") diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml index 95e7923823..75099c2314 100644 --- a/src/util/goblintutil.ml +++ b/src/util/goblintutil.ml @@ -118,22 +118,6 @@ let print_gc_quick_stat chn = gc.Gc.compactions; gc -let scrambled = try Sys.getenv "scrambled" = "true" with Not_found -> false -(* typedef struct { - PROCESS_NAME_TYPE NAME; - SYSTEM_ADDRESS_TYPE ENTRY_POINT; - STACK_SIZE_TYPE STACK_SIZE; - PRIORITY_TYPE BASE_PRIORITY; - SYSTEM_TIME_TYPE PERIOD; - SYSTEM_TIME_TYPE TIME_CAPACITY; - DEADLINE_TYPE DEADLINE; - } PROCESS_ATTRIBUTE_TYPE; *) -let arinc_name = if scrambled then "M161" else "NAME" -let arinc_entry_point = if scrambled then "M162" else "ENTRY_POINT" -let arinc_base_priority = if scrambled then "M164" else "BASE_PRIORITY" -let arinc_period = if scrambled then "M165" else "PERIOD" -let arinc_time_capacity = if scrambled then "M166" else "TIME_CAPACITY" - let exe_dir = Fpath.(parent (v Sys.executable_name)) let command_line = match Array.to_list Sys.argv with | command :: arguments -> Filename.quote_command command arguments diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 8e42e70385..39e0b72d96 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -461,48 +461,6 @@ }, "additionalProperties": false }, - "arinc": { - "title": "ana.arinc", - "type": "object", - "properties": { - "assume_success": { - "title": "ana.arinc.assume_success", - "description": - "Assume that all ARINC functions succeed (sets return code to NO_ERROR, otherwise invalidates it).", - "type": "boolean", - "default": true - }, - "simplify": { - "title": "ana.arinc.simplify", - "description": - "Simplify the graph by merging functions consisting of the same edges and contracting call chains where functions just consist of another call.", - "type": "boolean", - "default": true - }, - "validate": { - "title": "ana.arinc.validate", - "description": - "Validate the graph and output warnings for: call to functions without edges, multi-edge-calls for intermediate contexts, branching on unset return variables.", - "type": "boolean", - "default": true - }, - "export": { - "title": "ana.arinc.export", - "description": - "Generate dot graph and Promela for ARINC calls right after analysis. Result is saved in result/arinc.out either way.", - "type": "boolean", - "default": true - }, - "merge_globals": { - "title": "ana.arinc.merge_globals", - "description": - "Merge all global return code variables into one.", - "type": "boolean", - "default": false - } - }, - "additionalProperties": false - }, "opt": { "title": "ana.opt", "type": "object", diff --git a/tests/regression/17-arinc/01-sema.c b/tests/regression/17-arinc/01-sema.c deleted file mode 100644 index 7121d726a9..0000000000 --- a/tests/regression/17-arinc/01-sema.c +++ /dev/null @@ -1,142 +0,0 @@ -// PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --set solver slr3 --disable ana.arinc.export - -typedef char * SEMAPHORE_NAME_TYPE; -typedef int SEMAPHORE_ID_TYPE; -/* typedef int RETURN_CODE_TYPE; */ -enum T13 { - NO_ERROR = 0, // request valid and operation performed - NO_ACTION = 1, // status of system unaffected by request - NOT_AVAILABLE = 2, // resource required by request unavailable - INVALID_PARAM = 3, // invalid parameter specified in request - INVALID_CONFIG = 4, // parameter incompatible with configuration - INVALID_MODE = 5, // request incompatible with current mode - TIMED_OUT = 6 // time-out tied up with request has expired -} ; -typedef enum T13 RETURN_CODE_TYPE; -typedef int SEMAPHORE_VALUE_TYPE; -typedef void * QUEUING_DISCIPLINE_TYPE; -/* typedef int SYSTEM_TIME_TYPE; // in monit.c it is defined as unsigned long, PDF says signed 64bit */ -typedef long SYSTEM_TIME_TYPE; - -extern void LAP_Se_GetSemaphoreId(SEMAPHORE_NAME_TYPE, SEMAPHORE_ID_TYPE*, RETURN_CODE_TYPE*); -extern void LAP_Se_CreateSemaphore(SEMAPHORE_NAME_TYPE,SEMAPHORE_VALUE_TYPE,SEMAPHORE_VALUE_TYPE,QUEUING_DISCIPLINE_TYPE,SEMAPHORE_ID_TYPE*,RETURN_CODE_TYPE*); -extern void LAP_Se_WaitSemaphore(SEMAPHORE_ID_TYPE,SYSTEM_TIME_TYPE,RETURN_CODE_TYPE*); -extern void LAP_Se_SignalSemaphore(SEMAPHORE_ID_TYPE,RETURN_CODE_TYPE*); - -typedef void * PROCESS_NAME_TYPE; -typedef void * SYSTEM_ADDRESS_TYPE; -typedef long STACK_SIZE_TYPE; -typedef long PRIORITY_TYPE; -typedef int DEADLINE_TYPE; - -typedef struct { - PROCESS_NAME_TYPE NAME; - SYSTEM_ADDRESS_TYPE ENTRY_POINT; - STACK_SIZE_TYPE STACK_SIZE; - PRIORITY_TYPE BASE_PRIORITY; - SYSTEM_TIME_TYPE PERIOD; - SYSTEM_TIME_TYPE TIME_CAPACITY; - DEADLINE_TYPE DEADLINE; -} PROCESS_ATTRIBUTE_TYPE; - -typedef int PROCESS_ID_TYPE; - -extern void LAP_Se_CreateProcess(PROCESS_ATTRIBUTE_TYPE*, PROCESS_ID_TYPE*, RETURN_CODE_TYPE*); - -extern void LAP_Se_GetMyId(PROCESS_ID_TYPE*, RETURN_CODE_TYPE*); -extern void LAP_Se_Start(PROCESS_ID_TYPE, RETURN_CODE_TYPE*); - -typedef - enum { - IDLE = 0, - COLD_START = 1, - WARM_START = 2, - NORMAL = 3 - } OPERATING_MODE_TYPE; - -extern void LAP_Se_SetPartitionMode ( - /*in */ OPERATING_MODE_TYPE OPERATING_MODE, - /*out*/ RETURN_CODE_TYPE *RETURN_CODE ); -extern void LAP_Se_PeriodicWait (RETURN_CODE_TYPE *RETURN_CODE); -// ----------------------- - -int g,g2; -SEMAPHORE_ID_TYPE sem_id; - -int bg; -void foo2() { - RETURN_CODE_TYPE r; - LAP_Se_PeriodicWait(&r); -} -void foo(int b) { - RETURN_CODE_TYPE r; - if(b) foo2(); - // if(b) LAP_Se_PeriodicWait(&r); - PROCESS_ID_TYPE pid; - LAP_Se_GetMyId(&pid, &r); - LAP_Se_Start(pid, &r); - // if(bg) LAP_Se_PeriodicWait(&r); -} - -void P1(void){ - // foo(0); - // foo(1); - RETURN_CODE_TYPE r; - while (r){ - LAP_Se_WaitSemaphore(sem_id,600,&r); - g = g + 1; // NOWARN! - LAP_Se_SignalSemaphore(sem_id,&r); - } - LAP_Se_PeriodicWait(&r); - LAP_Se_PeriodicWait(&r); - return; -} - -void P2(void){ - // foo(0); - // foo(1); - // here we only get 1 context for foo without bg b/c P2 may run arbitrarily - // foo(0); bg = 1; foo(0); - // different contexts for different arguments work fine: - // foo(0); foo(1); - RETURN_CODE_TYPE r; - while (1){ - LAP_Se_WaitSemaphore(sem_id,600,&r); - if(r == NO_ERROR) - LAP_Se_PeriodicWait(&r); - g = g - 1; // NOWARN! - g2 = g2 + 1; // RACE! - LAP_Se_SignalSemaphore(sem_id,&r); - } - return; -} - -int main(){ - // here we get 2 contexts for foo with bg=0 and bg=1: - // foo(0); bg = 1; foo(0); - RETURN_CODE_TYPE r; - PROCESS_ID_TYPE pi1, pi2; - SEMAPHORE_ID_TYPE sem_id_local; - PROCESS_ATTRIBUTE_TYPE p1, p2; - LAP_Se_CreateSemaphore("my_mutex",1,1,0,&sem_id_local,&r); - LAP_Se_GetSemaphoreId("my_mutex",&sem_id,&r); - p1.NAME = "proc1"; - p1.ENTRY_POINT = (void *) &P1; - p1.BASE_PRIORITY = 10; - p1.PERIOD = 600; - p1.TIME_CAPACITY = 600; - p2.NAME = "proc2"; - p2.ENTRY_POINT = (void *) &P2; - p2.BASE_PRIORITY = 10; - p2.PERIOD = 600; - p2.TIME_CAPACITY = 600; - LAP_Se_CreateProcess(&p1,&pi1,&r); - LAP_Se_CreateProcess(&p2,&pi2,&r); - LAP_Se_Start(pi1,&r); - LAP_Se_Start(pi2,&r); - LAP_Se_SetPartitionMode(NORMAL,&r); - while(1) { - g2 = g2 - 1; // RACE! - } - return 0; -} diff --git a/tests/regression/17-arinc/02-unique_proc.c b/tests/regression/17-arinc/02-unique_proc.c deleted file mode 100644 index 1977e0ebba..0000000000 --- a/tests/regression/17-arinc/02-unique_proc.c +++ /dev/null @@ -1,94 +0,0 @@ -// NOMARSHAL PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --set solver slr3t --disable ana.arinc.export - -typedef char * SEMAPHORE_NAME_TYPE; -typedef int SEMAPHORE_ID_TYPE; -typedef int RETURN_CODE_TYPE; -typedef int SEMAPHORE_VALUE_TYPE; -typedef void * QUEUING_DISCIPLINE_TYPE; -typedef int SYSTEM_TIME_TYPE; - -extern void LAP_Se_GetSemaphoreId(SEMAPHORE_NAME_TYPE, SEMAPHORE_ID_TYPE*, RETURN_CODE_TYPE*); -extern void LAP_Se_CreateSemaphore(SEMAPHORE_NAME_TYPE,SEMAPHORE_VALUE_TYPE,SEMAPHORE_VALUE_TYPE,QUEUING_DISCIPLINE_TYPE,SEMAPHORE_ID_TYPE*,RETURN_CODE_TYPE*); -extern void LAP_Se_WaitSemaphore(SEMAPHORE_ID_TYPE,SYSTEM_TIME_TYPE,RETURN_CODE_TYPE*); -extern void LAP_Se_SignalSemaphore(SEMAPHORE_ID_TYPE,RETURN_CODE_TYPE*); - -typedef void * PROCESS_NAME_TYPE; -typedef void * SYSTEM_ADDRESS_TYPE; -typedef long STACK_SIZE_TYPE; -typedef long PRIORITY_TYPE; -typedef long SYSTEM_TIME_TYPE; -typedef long SYSTEM_TIME_TYPE; -typedef int DEADLINE_TYPE; - -typedef struct { - PROCESS_NAME_TYPE NAME; - SYSTEM_ADDRESS_TYPE ENTRY_POINT; - STACK_SIZE_TYPE STACK_SIZE; - PRIORITY_TYPE BASE_PRIORITY; - SYSTEM_TIME_TYPE PERIOD; - SYSTEM_TIME_TYPE TIME_CAPACITY; - DEADLINE_TYPE DEADLINE; -} PROCESS_ATTRIBUTE_TYPE; - -typedef int PROCESS_ID_TYPE; - -extern void LAP_Se_CreateProcess(PROCESS_ATTRIBUTE_TYPE*, PROCESS_ID_TYPE*, RETURN_CODE_TYPE*); - -extern void LAP_Se_Start(PROCESS_ID_TYPE, RETURN_CODE_TYPE*); - -typedef - enum { - IDLE = 0, - COLD_START = 1, - WARM_START = 2, - NORMAL = 3 - } OPERATING_MODE_TYPE; - -extern void LAP_Se_SetPartitionMode ( - /*in */ OPERATING_MODE_TYPE OPERATING_MODE, - /*out*/ RETURN_CODE_TYPE *RETURN_CODE ); -// ----------------------- - -int g,h; -SEMAPHORE_ID_TYPE sem_id; - -void P1(void){ - RETURN_CODE_TYPE r; - while (1){ - g = g + 1; // NOWARN! - } - return; -} - -void P2(void){ - RETURN_CODE_TYPE r; - while (1){ - h = h + 1; // NOWARN! - } - return; -} - -int main(){ - RETURN_CODE_TYPE r; - PROCESS_ID_TYPE pi1, pi2; - SEMAPHORE_ID_TYPE sem_id_local; - PROCESS_ATTRIBUTE_TYPE p1, p2; - LAP_Se_CreateSemaphore("my_mutex",1,1,0,&sem_id_local,&r); - LAP_Se_GetSemaphoreId("my_mutex",&sem_id,&r); - p1.NAME = "proc1"; - p1.ENTRY_POINT = (void *) &P1; - p1.BASE_PRIORITY = 10; - p1.PERIOD = 600; - p1.TIME_CAPACITY = 600; - p2.NAME = "proc2"; - p2.ENTRY_POINT = (void *) &P2; - p2.BASE_PRIORITY = 20; - p2.PERIOD = 600; - p2.TIME_CAPACITY = 600; - LAP_Se_CreateProcess(&p1,&pi1,&r); - LAP_Se_CreateProcess(&p2,&pi2,&r); - LAP_Se_Start(pi1,&r); - LAP_Se_Start(pi2,&r); - LAP_Se_SetPartitionMode(NORMAL,&r); - return 0; -} diff --git a/tests/regression/17-arinc/03-preemt_lock.c b/tests/regression/17-arinc/03-preemt_lock.c deleted file mode 100644 index 3a931adb3c..0000000000 --- a/tests/regression/17-arinc/03-preemt_lock.c +++ /dev/null @@ -1,92 +0,0 @@ -// SKIP PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --disable ana.arinc.export -// probably doesn't pass because some preemption-based privatization was removed in b2fba1f43c402d3a3811502d6ea1079f22fe8d21 -#include - -typedef char * SEMAPHORE_NAME_TYPE; -typedef int SEMAPHORE_ID_TYPE; -typedef int RETURN_CODE_TYPE; -typedef int SEMAPHORE_VALUE_TYPE; -typedef void * QUEUING_DISCIPLINE_TYPE; -typedef int SYSTEM_TIME_TYPE; - -extern void LAP_Se_GetSemaphoreId(SEMAPHORE_NAME_TYPE, SEMAPHORE_ID_TYPE*, RETURN_CODE_TYPE*); -extern void LAP_Se_CreateSemaphore(SEMAPHORE_NAME_TYPE,SEMAPHORE_VALUE_TYPE,SEMAPHORE_VALUE_TYPE,QUEUING_DISCIPLINE_TYPE,SEMAPHORE_ID_TYPE*,RETURN_CODE_TYPE*); -extern void LAP_Se_WaitSemaphore(SEMAPHORE_ID_TYPE,SYSTEM_TIME_TYPE,RETURN_CODE_TYPE*); -extern void LAP_Se_SignalSemaphore(SEMAPHORE_ID_TYPE,RETURN_CODE_TYPE*); - -typedef void * PROCESS_NAME_TYPE; -typedef void * SYSTEM_ADDRESS_TYPE; -typedef long STACK_SIZE_TYPE; -typedef long PRIORITY_TYPE; -typedef long SYSTEM_TIME_TYPE; -typedef long SYSTEM_TIME_TYPE; -typedef int DEADLINE_TYPE; - -typedef struct { - PROCESS_NAME_TYPE NAME; - SYSTEM_ADDRESS_TYPE ENTRY_POINT; - STACK_SIZE_TYPE STACK_SIZE; - PRIORITY_TYPE BASE_PRIORITY; - SYSTEM_TIME_TYPE PERIOD; - SYSTEM_TIME_TYPE TIME_CAPACITY; - DEADLINE_TYPE DEADLINE; -} PROCESS_ATTRIBUTE_TYPE; - -typedef int PROCESS_ID_TYPE; - -extern void LAP_Se_CreateProcess(PROCESS_ATTRIBUTE_TYPE*, PROCESS_ID_TYPE*, RETURN_CODE_TYPE*); - -extern void LAP_Se_Start(PROCESS_ID_TYPE, RETURN_CODE_TYPE*); - -typedef int LOCK_LEVEL_TYPE; - -extern void LAP_Se_LockPreemption ( - /*out*/ LOCK_LEVEL_TYPE *LOCK_LEVEL, - /*out*/ RETURN_CODE_TYPE *RETURN_CODE ); - -extern void LAP_Se_UnlockPreemption ( - /*out*/ LOCK_LEVEL_TYPE *LOCK_LEVEL, - /*out*/ RETURN_CODE_TYPE *RETURN_CODE ); - -typedef - enum { - IDLE = 0, - COLD_START = 1, - WARM_START = 2, - NORMAL = 3 - } OPERATING_MODE_TYPE; - -extern void LAP_Se_SetPartitionMode ( - /*in */ OPERATING_MODE_TYPE OPERATING_MODE, - /*out*/ RETURN_CODE_TYPE *RETURN_CODE ); - -// ----------------------- - -int g; - -void P1(void){ - LOCK_LEVEL_TYPE ll; - RETURN_CODE_TYPE r; - while (1){ - LAP_Se_LockPreemption(&ll,&r); - g = 1; - __goblint_check(g==1); // TODO: privatization by preemption? - LAP_Se_UnlockPreemption(&ll,&r); - } - return; -} - -int main(){ - RETURN_CODE_TYPE r; - PROCESS_ID_TYPE pi1,pi2; - PROCESS_ATTRIBUTE_TYPE p1,p2; - p1.NAME = "proc1"; - p1.ENTRY_POINT = (void *) &P1; - p1.BASE_PRIORITY = 10; - p1.PERIOD = 600; - p1.TIME_CAPACITY = 600; - LAP_Se_CreateProcess(&p1,&pi1,&r); - LAP_Se_Start(pi1,&r); - LAP_Se_SetPartitionMode(NORMAL,&r); - return 0; -} diff --git a/tests/regression/17-arinc/04-sema-strcpy.c b/tests/regression/17-arinc/04-sema-strcpy.c deleted file mode 100644 index dd620968c2..0000000000 --- a/tests/regression/17-arinc/04-sema-strcpy.c +++ /dev/null @@ -1,146 +0,0 @@ -// SKIP PARAM: --set ana.activated[+] arinc --set ana.activated[+] thread --set solver slr3 --disable ana.arinc.export - -typedef char * SEMAPHORE_NAME_TYPE; -typedef int SEMAPHORE_ID_TYPE; -/* typedef int RETURN_CODE_TYPE; */ -enum T13 { - NO_ERROR = 0, // request valid and operation performed - NO_ACTION = 1, // status of system unaffected by request - NOT_AVAILABLE = 2, // resource required by request unavailable - INVALID_PARAM = 3, // invalid parameter specified in request - INVALID_CONFIG = 4, // parameter incompatible with configuration - INVALID_MODE = 5, // request incompatible with current mode - TIMED_OUT = 6 // time-out tied up with request has expired -} ; -typedef enum T13 RETURN_CODE_TYPE; -typedef int SEMAPHORE_VALUE_TYPE; -typedef void * QUEUING_DISCIPLINE_TYPE; -/* typedef int SYSTEM_TIME_TYPE; // in monit.c it is defined as unsigned long, PDF says signed 64bit */ -typedef long SYSTEM_TIME_TYPE; - -extern void LAP_Se_GetSemaphoreId(SEMAPHORE_NAME_TYPE, SEMAPHORE_ID_TYPE*, RETURN_CODE_TYPE*); -extern void LAP_Se_CreateSemaphore(SEMAPHORE_NAME_TYPE,SEMAPHORE_VALUE_TYPE,SEMAPHORE_VALUE_TYPE,QUEUING_DISCIPLINE_TYPE,SEMAPHORE_ID_TYPE*,RETURN_CODE_TYPE*); -extern void LAP_Se_WaitSemaphore(SEMAPHORE_ID_TYPE,SYSTEM_TIME_TYPE,RETURN_CODE_TYPE*); -extern void LAP_Se_SignalSemaphore(SEMAPHORE_ID_TYPE,RETURN_CODE_TYPE*); - -typedef void * PROCESS_NAME_TYPE; -typedef void * SYSTEM_ADDRESS_TYPE; -typedef long STACK_SIZE_TYPE; -typedef long PRIORITY_TYPE; -typedef int DEADLINE_TYPE; - -typedef struct { - PROCESS_NAME_TYPE NAME; - SYSTEM_ADDRESS_TYPE ENTRY_POINT; - STACK_SIZE_TYPE STACK_SIZE; - PRIORITY_TYPE BASE_PRIORITY; - SYSTEM_TIME_TYPE PERIOD; - SYSTEM_TIME_TYPE TIME_CAPACITY; - DEADLINE_TYPE DEADLINE; -} PROCESS_ATTRIBUTE_TYPE; - -typedef int PROCESS_ID_TYPE; - -extern void LAP_Se_CreateProcess(PROCESS_ATTRIBUTE_TYPE*, PROCESS_ID_TYPE*, RETURN_CODE_TYPE*); - -extern void LAP_Se_GetMyId(PROCESS_ID_TYPE*, RETURN_CODE_TYPE*); -extern void LAP_Se_Start(PROCESS_ID_TYPE, RETURN_CODE_TYPE*); - -typedef - enum { - IDLE = 0, - COLD_START = 1, - WARM_START = 2, - NORMAL = 3 - } OPERATING_MODE_TYPE; - -extern void LAP_Se_SetPartitionMode ( - /*in */ OPERATING_MODE_TYPE OPERATING_MODE, - /*out*/ RETURN_CODE_TYPE *RETURN_CODE ); -extern void LAP_Se_PeriodicWait (RETURN_CODE_TYPE *RETURN_CODE); - -typedef char T1; -char * F59(T1* destination, const T1* source ); // strcpy -// ----------------------- - -int g,g2; -SEMAPHORE_ID_TYPE sem_id; - -int bg; -void foo2() { - RETURN_CODE_TYPE r; - LAP_Se_PeriodicWait(&r); -} -void foo(int b) { - RETURN_CODE_TYPE r; - if(b) foo2(); - // if(b) LAP_Se_PeriodicWait(&r); - PROCESS_ID_TYPE pid; - LAP_Se_GetMyId(&pid, &r); - LAP_Se_Start(pid, &r); - // if(bg) LAP_Se_PeriodicWait(&r); -} - -void P1(void){ - // foo(0); - // foo(1); - RETURN_CODE_TYPE r; - while (r){ - LAP_Se_WaitSemaphore(sem_id,600,&r); - g = g + 1; // NOWARN! - LAP_Se_SignalSemaphore(sem_id,&r); - } - LAP_Se_PeriodicWait(&r); - LAP_Se_PeriodicWait(&r); - return; -} - -void P2(void){ - // foo(0); - // foo(1); - // here we only get 1 context for foo without bg b/c P2 may run arbitrarily - // foo(0); bg = 1; foo(0); - // different contexts for different arguments work fine: - // foo(0); foo(1); - RETURN_CODE_TYPE r; - while (1){ - LAP_Se_WaitSemaphore(sem_id,600,&r); - if(r == NO_ERROR) - LAP_Se_PeriodicWait(&r); - g = g - 1; // NOWARN! - g2 = g2 + 1; // RACE! - LAP_Se_SignalSemaphore(sem_id,&r); - } - return; -} - -int main(){ - // here we get 2 contexts for foo with bg=0 and bg=1: - // foo(0); bg = 1; foo(0); - RETURN_CODE_TYPE r; - PROCESS_ID_TYPE pi1, pi2; - SEMAPHORE_ID_TYPE sem_id_local; - PROCESS_ATTRIBUTE_TYPE p1, p2; - LAP_Se_CreateSemaphore("my_mutex",1,1,0,&sem_id_local,&r); - LAP_Se_GetSemaphoreId("my_mutex",&sem_id,&r); - F59(p1.NAME, (T1 *)"proc1"); - /*p1.NAME = "proc1";*/ - p1.ENTRY_POINT = (void *) &P1; - p1.BASE_PRIORITY = 10; - p1.PERIOD = 600; - p1.TIME_CAPACITY = 600; - p2.NAME = "proc2"; - p2.ENTRY_POINT = (void *) &P2; - p2.BASE_PRIORITY = 10; - p2.PERIOD = 600; - p2.TIME_CAPACITY = 600; - LAP_Se_CreateProcess(&p1,&pi1,&r); - LAP_Se_CreateProcess(&p2,&pi2,&r); - LAP_Se_Start(pi1,&r); - LAP_Se_Start(pi2,&r); - LAP_Se_SetPartitionMode(NORMAL,&r); - while(1) { - g2 = g2 - 1; // RACE! - } - return 0; -} diff --git a/tests/regression/17-arinc/05-term-simple.c b/tests/regression/17-arinc/05-term-simple.c deleted file mode 100644 index 75a13554b2..0000000000 --- a/tests/regression/17-arinc/05-term-simple.c +++ /dev/null @@ -1,33 +0,0 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','term','mallocWrapper','assert']" --enable dbg.debug --enable ana.int.interval --set solver slr3 --set ana.base.privatization none - -/*#include "stdio.h"*/ - -int main(){ - int i = 0; - int j = 0; - int t = 0; - - t=0; - while (i < 5) { - i++; - t=0; - while (j < 10) { - j++; - t=0; - } - t=0; - /* j = 3; */ - } - t=0; - - /* while (i < 5) { */ - /* i++; */ - /* if(i%2) continue; */ - /* j += i; */ - /* } */ - - /* for(i=0; i<5; i++){ */ - /* if(i%2) continue; */ - /* j += i; */ - /* } */ -} diff --git a/tests/regression/17-arinc/06-term.c b/tests/regression/17-arinc/06-term.c deleted file mode 100644 index 1140152605..0000000000 --- a/tests/regression/17-arinc/06-term.c +++ /dev/null @@ -1,113 +0,0 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','term','mallocWrapper','assert']" --enable dbg.debug --enable ana.int.interval --set solver slr3 --set ana.base.privatization none - -int main(){ - int i = 0; - while (i < 5) { - i++; - } -//#line 5 -// while (1) { -// while_continue: /* CIL Label */ ; -//#line 5 -// if (! (i < 5)) { -//#line 5 -// goto while_break; -// } -// { -//#line 6 -// i ++; -// } -// } -// while_break: /* CIL Label */ ; - while (1) { - if(i >= 5) break; - i++; - } -//#line 22 -// while (1) { -// while_continue___0: /* CIL Label */ ; -//#line 23 -// if (i >= 5) { -//#line 23 -// goto while_break___0; -// } -// { -//#line 24 -// i ++; -// } -// } -// while_break___0: /* CIL Label */ ; - while (1) { - i++; - if(i >= 5) break; - } -//#line 40 -// while (1) { -// while_continue___1: /* CIL Label */ ; -// { -//#line 41 -// i ++; -// } -//#line 42 -// if (i >= 5) { -//#line 42 -// goto while_break___1; -// } -// } -// while_break___1: /* CIL Label */ ; - for (i=0; i<5; i++) { - } -// { -//#line 58 -// i = 0; -// } -// { -//#line 58 -// while (1) { -// while_continue___2: /* CIL Label */ ; -//#line 58 -// if (! (i < 5)) { -//#line 58 -// goto while_break___2; -// } -// { -//#line 58 -// i ++; -// } -// } -// while_break___2: /* CIL Label */ ; -// } - while (1) { - if(i >= 5) return 1; - i++; - } -//#line 80 -// while (1) { -// while_continue___3: /* CIL Label */ ; -//#line 81 -// if (i >= 5) { -//#line 81 -// return (1); -// } -// { -//#line 82 -// i ++; -// } -// } -// while_break___3: /* CIL Label */ ; - while (1) { - i++; - } -// { -//#line 99 -// while (1) { -// while_continue___4: /* CIL Label */ ; -// { -//#line 100 -// i ++; -// } -// } -// while_break___4: /* CIL Label */ ; -// } - return 0; -} diff --git a/tests/regression/17-arinc/07-cond-var.c b/tests/regression/17-arinc/07-cond-var.c deleted file mode 100644 index 79b2a5726f..0000000000 --- a/tests/regression/17-arinc/07-cond-var.c +++ /dev/null @@ -1,28 +0,0 @@ -#include -#include -#include - -int main(){ - /* time_t t; */ - /* srand((unsigned) time(&t)); */ - /* int i = rand() % 2000; */ - int i; - int a, b; - printf("i = %d ", i); - a = (int) ((int) i < 1000); // casts shouldn't be a problem - if(a){ - printf("<"); - }else{ - printf(">="); - } - /* a = 1; // this should destroy b -> i < 1000 */ - b = a; - a = 1; // this shouldn't destroy b -> i < 1000 - if(b){ - printf("<"); - }else{ - printf(">="); - } - printf(" 1000\n"); - return 0; -} diff --git a/tests/regression/17-arinc/08-multi-cond.c b/tests/regression/17-arinc/08-multi-cond.c deleted file mode 100644 index c8b0ff7f50..0000000000 --- a/tests/regression/17-arinc/08-multi-cond.c +++ /dev/null @@ -1,23 +0,0 @@ - -int main(){ - // TO-DO: this is a problem of how the results are displayed - int x; - if(x > 1 && x < 10){ - x = 1; // [2,9] ok - }else{ - x = 3; // [-inf,1], but should be [-inf,1] join [10,inf] = top - } - - // results on CIL's output are fine: - int y; - if(y > 1){ // line 4 - if(y<10){ // line 4 - y = 1; // line 5 - }else{ - y = 3; // line 7 - } - }else{ - y = 3; // line 7 - } - return 0; -} diff --git a/tests/regression/17-arinc/09-cond-var-scope.c b/tests/regression/17-arinc/09-cond-var-scope.c deleted file mode 100644 index 52bab5d547..0000000000 --- a/tests/regression/17-arinc/09-cond-var-scope.c +++ /dev/null @@ -1,36 +0,0 @@ -#include -#include - -// expressions for a should not escape their scope -int a; - -void f(){ - int i; - if(a){ // Unknown - printf("<"); - }else{ - printf(">="); - } - a = i < 2; // this should not move to main -} - -int main(){ - int i; - a = i < 1; // this should not move to f - f(); - if(a){ // Unknown - printf("<"); - }else{ - printf(">="); - } - { - int i; - a = i < 3; // this should not escape - } - if(a){ // Unknown - printf("<"); - }else{ - printf(">="); - } - return 0; -} diff --git a/tests/regression/17-arinc/10-term-phases.c b/tests/regression/17-arinc/10-term-phases.c deleted file mode 100644 index 4d3a2bd483..0000000000 --- a/tests/regression/17-arinc/10-term-phases.c +++ /dev/null @@ -1,11 +0,0 @@ -/*#include "stdio.h"*/ - -int main(){ - int i = 0; - int j = 5; - - while (i < j) { - i++; - } - return j; -} diff --git a/tests/regression/17-arinc/README.md b/tests/regression/17-arinc/README.md new file mode 100644 index 0000000000..173faa7344 --- /dev/null +++ b/tests/regression/17-arinc/README.md @@ -0,0 +1,2 @@ +ARINC653 support has been removed from recent Goblint versions, please use Release 1.1.1 +Folder is left in place to avoid renumbering all tests diff --git a/tests/regression/17-arinc/arinc_sema.spec b/tests/regression/17-arinc/arinc_sema.spec deleted file mode 100644 index 46e6530440..0000000000 --- a/tests/regression/17-arinc/arinc_sema.spec +++ /dev/null @@ -1,14 +0,0 @@ -w1 "LAP_Se_CreateSemaphore" -w2 "LAP_Se_WaitSemaphore" -w3 "LAP_Se_SignalSemaphore" - - -1 -w1> 1 LAP_Se_CreateSemaphore(_) -1 -w2> 1 LAP_Se_WaitSemaphore(_) -1 -w3> 1 LAP_Se_SignalSemaphore(_) - - - -//1 -("cur>max" if cur > max)> created LAP_Se_CreateSemaphore(_, cur, max, $id, _) -//(created,wait) -> (wait if $id.cur == 0 else created) LAP_Se_WaitSemaphore($id, time, _) $id.cur-- -//(created,wait) -("cur>max" if cur > max)> (wait if $id.cur == 0 else created) LAP_Se_SignalSemaphore($id, _) $id.cur++ \ No newline at end of file From 3836a4dce21ee79344068fb9e0fbd2fd8523a023 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 2 Aug 2022 18:32:28 +0200 Subject: [PATCH 2/7] Remove `presub` --- src/analyses/mCP.ml | 1 - src/framework/analyses.ml | 1 - src/framework/constraints.ml | 1 - src/framework/control.ml | 5 ----- src/witness/witness.ml | 1 - src/witness/yamlWitness.ml | 2 -- 6 files changed, 11 deletions(-) diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 5bd9c82238..213f5b6952 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -311,7 +311,6 @@ struct { ctx with ask = (fun (type a) (q: a Queries.t) -> query' ~querycache Queries.Set.empty ctx q) ; emit - ; presub = assoc_sub ctx.local ; spawn ; sideg } diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index f2b99a68e4..6e2d54f845 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -289,7 +289,6 @@ type ('d,'g,'c,'v) ctx = ; edge : MyCFG.edge ; local : 'd ; global : 'v -> 'g - ; presub : string -> Obj.t (** raises [Not_found] if such dependency analysis doesn't exist *) ; spawn : lval option -> varinfo -> exp list -> unit ; split : 'd -> Events.t list -> unit ; sideg : 'v -> 'g -> unit diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index b444afd47a..819894ecb8 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -483,7 +483,6 @@ struct ; edge = edge ; local = pval ; global = getg - ; presub = (fun _ -> raise Not_found) ; spawn = spawn ; split = (fun (d:D.t) es -> assert (List.is_empty es); r := d::!r) ; sideg = sideg diff --git a/src/framework/control.ml b/src/framework/control.ml index e0e80631c5..d1ded03908 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -266,7 +266,6 @@ struct ; edge = MyCFG.Skip ; local = Spec.D.top () ; global = getg - ; presub = (fun _ -> raise Not_found) ; spawn = (fun _ -> failwith "Global initializers should never spawn threads. What is going on?") ; split = (fun _ -> failwith "Global initializers trying to split paths.") ; sideg = sideg @@ -366,7 +365,6 @@ struct ; edge = MyCFG.Skip ; local = st ; global = getg - ; presub = (fun _ -> raise Not_found) ; spawn = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.") ; split = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.") ; sideg = sideg @@ -399,7 +397,6 @@ struct ; edge = MyCFG.Skip ; local = st ; global = getg - ; presub = (fun _ -> raise Not_found) ; spawn = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.") ; split = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.") ; sideg = sideg @@ -600,7 +597,6 @@ struct ; edge = MyCFG.Skip ; local = local ; global = GHT.find gh - ; presub = (fun _ -> raise Not_found) ; spawn = (fun v d -> failwith "Cannot \"spawn\" in query context.") ; split = (fun d es -> failwith "Cannot \"split\" in query context.") ; sideg = (fun v g -> failwith "Cannot \"split\" in query context.") @@ -654,7 +650,6 @@ struct ; edge = MyCFG.Skip ; local = snd (List.hd startvars) (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *) ; global = (fun v -> try GHT.find gh v with Not_found -> EQSys.G.bot ()) - ; presub = (fun _ -> raise Not_found) ; spawn = (fun v d -> failwith "Cannot \"spawn\" in query context.") ; split = (fun d es -> failwith "Cannot \"split\" in query context.") ; sideg = (fun v g -> failwith "Cannot \"split\" in query context.") diff --git a/src/witness/witness.ml b/src/witness/witness.ml index db17dc6310..c35fac6723 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -295,7 +295,6 @@ struct ; edge = MyCFG.Skip ; local = local ; global = GHT.find gh - ; presub = (fun _ -> raise Not_found) ; spawn = (fun v d -> failwith "Cannot \"spawn\" in witness context.") ; split = (fun d es -> failwith "Cannot \"split\" in witness context.") ; sideg = (fun v g -> failwith "Cannot \"sideg\" in witness context.") diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 028f99e65d..981636e150 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -142,7 +142,6 @@ struct ; edge = MyCFG.Skip ; local = local ; global = (fun v -> try GHT.find gh v with Not_found -> Spec.G.bot ()) (* TODO: how can be missing? *) - ; presub = (fun _ -> raise Not_found) ; spawn = (fun v d -> failwith "Cannot \"spawn\" in witness context.") ; split = (fun d es -> failwith "Cannot \"split\" in witness context.") ; sideg = (fun v g -> failwith "Cannot \"sideg\" in witness context.") @@ -245,7 +244,6 @@ struct ; edge = MyCFG.Skip ; local = local ; global = (fun v -> try GHT.find gh v with Not_found -> Spec.G.bot ()) (* TODO: how can be missing? *) - ; presub = (fun _ -> raise Not_found) ; spawn = (fun v d -> failwith "Cannot \"spawn\" in witness context.") ; split = (fun d es -> failwith "Cannot \"split\" in witness context.") ; sideg = (fun v g -> failwith "Cannot \"sideg\" in witness context.") From 9b969c4021c9c887c54bfe00a1f538d204f01feb Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 3 Aug 2022 08:32:28 +0200 Subject: [PATCH 3/7] Remove obfuscated library functions --- src/analyses/base.ml | 8 ++++---- tests/regression/01-cpa/24-library_functions.c | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 460014bb82..4f8c11ad4a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2499,9 +2499,9 @@ struct let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *) let value = VD.zero_init_value dest_typ in set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value - | Unknown, "F59" (* strcpy *) - | Unknown, "F60" (* strncpy *) - | Unknown, "F63" (* memcpy *) + | Unknown, "strcpy" + | Unknown, "strncpy" + | Unknown, "memcpy" -> begin match args with | [dst; src] @@ -2524,7 +2524,7 @@ struct assign ctx (get_lval dst) src | _ -> failwith "strcpy arguments are strange/complicated." end - | Unknown, "F1" -> + | Unknown, "memset" -> begin match args with | [dst; data; len] -> (* memset: write char to dst len times *) let dst_lval = mkMem ~addr:dst ~off:NoOffset in diff --git a/tests/regression/01-cpa/24-library_functions.c b/tests/regression/01-cpa/24-library_functions.c index d742c136ec..d48e60aac4 100644 --- a/tests/regression/01-cpa/24-library_functions.c +++ b/tests/regression/01-cpa/24-library_functions.c @@ -55,7 +55,7 @@ void test_memcpy() { memcpy(&dest, &src, sizeof(int)); - __goblint_check(dest == 0); // UNKNOWN! + __goblint_check(dest == 0); //FAIL __goblint_check(src == 1); } From e73ee0351db087ad0ef827e6fe6c92d4abddb29e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 3 Aug 2022 11:10:17 +0200 Subject: [PATCH 4/7] Cleanup `memcpy` --- src/analyses/base.ml | 28 ++++++++-------------------- 1 file changed, 8 insertions(+), 20 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4f8c11ad4a..151ce38b86 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2502,26 +2502,14 @@ struct | Unknown, "strcpy" | Unknown, "strncpy" | Unknown, "memcpy" - -> - begin match args with - | [dst; src] - | [dst; src; _] -> - (* let dst_val = eval_rv ctx.ask ctx.global ctx.local dst in *) - (* let src_val = eval_rv ctx.ask ctx.global ctx.local src in *) - (* begin match dst_val with *) - (* | `Address ls -> set_savetop ctx.ask ctx.global ctx.local ls src_val *) - (* | _ -> ignore @@ Pretty.printf "strcpy: dst %a may point to anything!\n" d_exp dst; *) - (* ctx.local *) - (* end *) - let rec get_lval exp = match stripCasts exp with - | Lval x | AddrOf x | StartOf x -> x - | BinOp (PlusPI, e, i, _) - | BinOp (MinusPI, e, i, _) -> get_lval e - | x -> - ignore @@ Pretty.printf "strcpy: dst is %a!\n" d_plainexp dst; - failwith "strcpy: expecting first argument to be a pointer!" - in - assign ctx (get_lval dst) src + | Unknown, "__builtin___memcpy_chk" -> + begin match f.vname, args with + | _, [dst; src] + | _, [dst; src; _] + | "__builtin___memcpy_chk", [dst; src; _; _] -> + let dst_lval = mkMem ~addr:(Cil.stripCasts dst) ~off:NoOffset in + let src_a = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in + assign ctx dst_lval (Lval src_a) | _ -> failwith "strcpy arguments are strange/complicated." end | Unknown, "memset" -> From e18ccea1cd4c497415e7b10b001822565bae7a8b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 3 Aug 2022 11:30:55 +0200 Subject: [PATCH 5/7] Add second `memcopy` test --- tests/regression/01-cpa/24-library_functions.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/tests/regression/01-cpa/24-library_functions.c b/tests/regression/01-cpa/24-library_functions.c index d48e60aac4..29d7e9dc38 100644 --- a/tests/regression/01-cpa/24-library_functions.c +++ b/tests/regression/01-cpa/24-library_functions.c @@ -59,6 +59,19 @@ void test_memcpy() { __goblint_check(src == 1); } +void test_memcpy_two() { + int dest = 0; + int src = 1; + + int* destp = &dest; + int* srcp = &src; + + memcpy(destp, srcp, sizeof(int)); + + __goblint_check(dest == 0); //FAIL + __goblint_check(src == 1); +} + void test_fopen() { } @@ -191,6 +204,7 @@ int main () { test_getopt(); test_localtime(); test_memcpy(); + test_memcpy_two(); test_memset(); test_printf(); test_read(); From 54b9bfdce82ed7871c1b4b713a5a17ac76150449 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 3 Aug 2022 12:46:56 +0200 Subject: [PATCH 6/7] Rm spurious memset --- src/analyses/base.ml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 151ce38b86..a76e8da7bd 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2512,13 +2512,6 @@ struct assign ctx dst_lval (Lval src_a) | _ -> failwith "strcpy arguments are strange/complicated." end - | Unknown, "memset" -> - begin match args with - | [dst; data; len] -> (* memset: write char to dst len times *) - let dst_lval = mkMem ~addr:dst ~off:NoOffset in - assign ctx dst_lval data (* this is only ok because we use ArrayDomain.Trivial per default, i.e., there's no difference between the first element or the whole array *) - | _ -> failwith "memset arguments are strange/complicated." - end | Unknown, "__builtin" -> begin match args with | Const (CStr ("invariant",_)) :: ((_ :: _) as args) -> From 52ff270b6dd3f105ceb1377ef5c3e6026b96b62d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 3 Aug 2022 12:50:23 +0200 Subject: [PATCH 7/7] Rm `pml_arinc` and `plm` --- src/extract/pml.ml | 243 --------------------------------------- src/extract/pml_arinc.ml | 191 ------------------------------ 2 files changed, 434 deletions(-) delete mode 100644 src/extract/pml.ml delete mode 100644 src/extract/pml_arinc.ml diff --git a/src/extract/pml.ml b/src/extract/pml.ml deleted file mode 100644 index b1dd5f8763..0000000000 --- a/src/extract/pml.ml +++ /dev/null @@ -1,243 +0,0 @@ -open BatteriesExceptionless - -type 'a e = 'a * string (* some expression and its promela representation *) -type _ t = (* promela types *) - | Enum : 'a * ('a -> string) -> 'a t - | Chan : 'a chan -> 'a chan t - | Bool : bool -> bool t - | Byte : int -> int t | Short : int -> int t | Int : int -> int t (* maybe do something like Bigarray.kind to avoid conflating ints of different size *) - (* the following are for arguments, and can not be declared in promela *) - | String : string -> string t - | Void : unit t (* this is just for skipping uninteresting arguments *) -and 'a chan = { capacity : int e (* 0 = rendez-vous *); mutable content : 'a list; content_type : 'a t } - -let enums : (string, string) Hashtbl.t = Hashtbl.create 123 (* value -> type (both as strings) *) -let of_enums = Hashtbl.create 123 (* enum type -> (enum value as int -> enum value as string option) *) -let enum of_enum show name = - Hashtbl.add of_enums name (fun x -> Option.map show (of_enum x)); - let values = List.of_enum @@ (0 -- 13) //@ of_enum /@ show in - List.iter (flip (Hashtbl.add enums) name) values; - (), "mtype = { "^ String.concat ", " values ^" }" -let enum_type x = Hashtbl.find enums x -let is_enum = Option.is_some % Hashtbl.find enums -let rec is_declared : type a . a t -> bool = function - | Enum (x,s) -> is_enum (s x) - | Chan c -> is_declared c.content_type - | _ -> true -let rec unbox : type a . a t -> string * (a -> string) * a = function (* type, show, value *) - | Enum (x,s) -> "mtype", s, x - | Chan c -> - let t',s,x = unbox c.content_type in - "chan", (fun c -> "["^snd c.capacity^"] of {"^t'^"}"), c - | Bool x -> "bool", string_of_bool, x - | Byte x -> "byte", string_of_int, x - | Short x -> "short", string_of_int, x - | Int x -> "int", string_of_int, x - | String x -> "string", identity, x - | Void -> "byte", (fun () -> assert false), () - -type _ var = (* variable with initial value and printer. type: content * get * set * mod *) - | Var : { name : string; init : 'a t; value : 'a ref; show : 'a -> string } -> - ('a e * 'a e * ('a e -> unit e) * unit e) var - | Arr : { name : string; init : 'a t; value : 'a array; show : 'a -> string; show_all : 'a array -> string; length : int } -> - ('a e * (int e -> 'a e) * (int e * 'a e -> unit e) * (int e -> unit e)) var - -let var value name = - assert (is_declared value); - let t,s,v = unbox value in - Var { name; init = value; value = ref v; show = s }, - t^" "^name^" = "^s v^";" -let arr length value name = - assert (is_declared value); - let t,s,v = unbox value in - let show_arr a = Array.to_list a |> List.map s |> String.concat ", " in - Arr { name; init = value; value = Array.create (fst length) v; show = s; show_all = show_arr; length = fst length }, - t^" "^name^"["^snd length^"] = "^s v^";" - -let var_name : type x. x var -> string = function - | Var v -> v.name - | Arr v -> v.name - -let get : type c g s m. (c*g*s*m) var -> g = function - | Var v -> !(v.value), v.name - | Arr v -> fun i -> - assert (fst i >= 0 && fst i < v.length); - Array.get v.value (fst i), v.name^"["^snd i^"]" -let set : type c g s m. (c*g*s*m) var -> s = function - | Var v -> fun x -> (v.value := fst x), v.name^" = "^snd x^";" - | Arr v -> fun (i,x) -> - assert (fst i >= 0 && fst i < v.length); - Array.set v.value (fst i) (fst x), v.name^"["^snd i^"] = "^snd x^";" - -(* Var x: !x, x := v. Arr x: !x i, x := i, v *) -let (!) = get -let (:=) = set -let (@=) = set (* maybe use this since it has higher precedence than >> *) - -(* we do not define `not` since this may tempt people to use !empty instead of nempty (same with nfull) *) - -let _assert x = assert (fst x), "assert("^snd x^");" -let println x = (* print_endline (fst x) *) (), "printf(\""^snd x^"\\n\");" - -let _true = true, "true" -let _false = false, "false" - -let wait x = ignore (fst x = true), "("^snd x^");" (* a standalone expression in Promela is a statement that blocks until the expression is true *) -let break = (), "break" (* jumps to the end of the innermost do loop *) -let skip = wait _true -let nop = (), "" - -module Chan = struct (* channels *) - let create len content = Chan { capacity = len; content = []; content_type = content } - - let full (c,s) = List.compare_length_with c.content (fst c.capacity) >= 0, "full("^s^")" - let nfull (c,s) = List.compare_length_with c.content (fst c.capacity) < 0, "nfull("^s^")" - let empty (c,s) = c.content = [], "empty("^s^")" - let nempty (c,s) = c.content <> [], "nempty("^s^")" - let len (c,s) = List.length c.content, "len("^s^")" - - (* ? = first, ?? = any, no <> = consume, <> = remain, TODO eval, !! *) - let first c e = match c.content with x::_ when x = fst e -> true | _ -> false - let any c e = List.mem (fst e) c.content - let poll m (c,s) e = (* checks (no side-effects) if (the first|any) element is e *) - let b,op = match m with - | `First -> first c e, "?" - | `Any -> any c e, "??" - in - b, s^op^"["^snd e^"]" - let recv m (c,s) e = (* blocks until (the first|any) element is e (w/o changing e) and removes it from the channel *) - let b,op = match m with - | `First -> first c e, "?" - | `Any -> any c e, "??" - in - c.content <- List.remove c.content (fst e); - (), s^op^"eval("^snd e^")" - let send (c,s) e = (* append|sorted *) - fst (nfull (c,s)), s^"!"^snd e -end - -(* OCaml's ; - sequential composition *) -let (>>) a b = fst b, snd a^"\n"^snd b -let bind x f = x >> f (fst x) -let (>>=) = bind -let (let*) = bind (* introduced in OCaml 4.08.0: https://ocaml.org/manual/bindingops.html *) -let return x = x (* ? *) - -let indent x = String.split_on_string ~by:"\n" x |> List.map (fun x -> " "^x) |> String.concat "\n" - -let surround a b (v,s) = v, a^"\n"^indent s^"\n"^b -let _match xs = - assert (xs <> []); - let s = String.concat "\n" @@ List.map (fun (c,b) -> ":: "^snd c^" -> "^snd b) xs in - (*List.find (fst%fst) xs, s*) - (), s -let _do xs = surround "do" "od;" (_match xs) -let _if xs = surround "if" "fi;" (_match xs) -let _ifte b x y = - (* TODO `else` fails for channel operations, also, how to implement in OCaml? *) - let c = true, "else" in - _if [b, x; c, y] -let _ift b x = _ifte b x skip -let _for (Var i) (Arr v) b = (* for (i in a) { b } *) - surround ("for ("^i.name^" in "^v.name^") {") "}" b -let _foreach (Arr v as a) b = (* for (i in a) { `b i a[i]` } *) - var (Byte 0) ("i_"^v.name) >>= (* TODO this doesn't work for nested loops on the same array! *) - fun i -> _for i a (b !i (!a !i)) (* NOTE this already gives the values to the body instead of the variables TODO for interpreter *) - - -(* extraction *) -type ('a,'b,'c,'d,'e,'z) args = A0 of 'z e | A1 of 'a * ('a -> 'z e) | A2 of 'a*'b * ('a -> 'b -> 'z e) | A3 of 'a*'b*'c * ('a -> 'b -> 'c -> 'z e) | A4 of 'a*'b*'c*'d * ('a -> 'b -> 'c -> 'd -> 'z e) | A5 of 'a*'b*'c*'d*'e * ('a -> 'b -> 'c -> 'd -> 'e -> 'z e) - -module Macro = struct - let define name args = - let unpack p = function - | A0 z -> [], z - | A1 (a,f) -> [p a], f a - | A2 (a,b,f) -> [p a; p b], f a b - | A3 (a,b,c,f) -> [p a; p b; p c], f a b c - | A4 (a,b,c,d,f) -> [p a; p b; p c; p d], f a b c d - | A5 (a,b,c,d,e,f) -> [p a; p b; p c; p d; p e], f a b c d e - in - let aa, body = unpack (fun (Var v) -> v.name) args in - let args = String.concat ", " aa |> fun x -> if List.is_empty aa then x else "("^x^")" in - (), "\n#define "^name^args^" "^snd body - - (* let _if e body = (), "\n#if "^snd e^"\n"^indent body^"\n#endif" *) - let _if e = (), "#if "^snd e - let _endif = (), "#endif" -end - -type eval = (* how to evaluate function arguments *) - | EvalEnum of (int -> string option) | EvalInt | EvalString (* standard types *) - | EvalSkip (* don't evaluate *) - | AssignIdOfString of string * int (* kind * position: evaluate argument at position as a string, use it to generate an id of kind, and assign it to argument, map id to int for promela *) -(*| EvalSpecial of string*) -[@@deriving show] - -let extract_funs = Hashtbl.create 123 (* name of function to list of how to evaluate arguments *) -let special_fun name = Hashtbl.find extract_funs name -let special_funs () = Hashtbl.keys extract_funs |> List.of_enum - -let extract ?id fname args = (* generate code for function and register for extraction *) - let unpack = - let name (Var v) = v.name in - let eval (type a b c) (Var v : (a*b*c*unit e) var) = match v.init with - | Enum (x,s) -> EvalEnum (Option.get @@ Hashtbl.find of_enums (Option.get (enum_type (s x)))) - | Byte _ -> EvalInt - | Short _ -> EvalInt - | Int _ -> EvalInt - | String _ -> EvalString - | Void -> EvalSkip - | _ -> failwith ("unsupported argument type for "^v.name) - in - let p a = name a, eval a in - function - | A0 z -> [], z - | A1 (a,f) -> [p a], f a - | A2 (a,b,f) -> [p a; p b], f a b - | A3 (a,b,c,f) -> [p a; p b; p c], f a b c - | A4 (a,b,c,d,f) -> [p a; p b; p c; p d], f a b c d - | A5 (a,b,c,d,e,f) -> [p a; p b; p c; p d; p e], f a b c d e - in - let aa, body = unpack args in - let aa' = List.filter (fun (n,e) -> e <> EvalSkip && e <> EvalString) aa in (* don't want skipped arguments or strings in definition *) - let arg_names, arg_evals = List.map fst aa', List.map snd aa in - let arg_evals = match id with - | Some (dst, src, res) -> List.modify_at dst (fun _ -> AssignIdOfString (res, src)) arg_evals - | None -> arg_evals - in - Hashtbl.add extract_funs fname arg_evals; - (), "\ninline "^fname^"("^String.concat ", " arg_names^") { atomic {\n" ^ - indent (snd body) ^ - "\n}}\n" - - -(* overwrite remaining operators *) -let op o s x y = o (fst x) (fst y), snd x^" "^s^" "^snd y -let (==) x y = op (=) "==" x y -let (!=) x y = op (<>) "!=" x y -let (<) x y = op (<) "<" x y -let (>) x y = op (>) ">" x y -let (<=) x y = op (<=) "<=" x y -let (>=) x y = op (>=) ">=" x y -let (+) x y = op (+) "+" x y -let (-) x y = op (-) "-" x y -let (/) x y = op (/) "/" x y -let ( * ) x y = op ( * ) "*" x y -let (&&) x y = op (&&) "&&" x y -let (||) x y = op (||) "||" x y - -let i i = i, string_of_int i (* int literal *) -let s s = s, s (* string literal *) -let (^) a b = fst a^fst b, snd a^snd b (* string concatenation *) -let fail m = println (s "FAIL: "^m) >> _assert _true (* TODO _assert _false evaluates too early :( *) -let i2s (i,s) = string_of_int i, s -let e x s = x, s x -let e2s x = s (snd x) (* TODO ? *) - -let incr : type g s m. (int e*g*s*m) var -> m = function - | Var _ as v -> set v (get v + i 1) - | Arr _ as v -> fun j -> set v (j, (get v j + i 1)) -let decr : type g s m. (int e*g*s*m) var -> m = function - | Var _ as v -> set v (get v - i 1) - | Arr _ as v -> fun j -> set v (j, (get v j - i 1)) diff --git a/src/extract/pml_arinc.ml b/src/extract/pml_arinc.ml deleted file mode 100644 index 2fb6f9d1d8..0000000000 --- a/src/extract/pml_arinc.ml +++ /dev/null @@ -1,191 +0,0 @@ -open BatteriesExceptionless - -(* enums *) -type return_code = SUCCESS | ERROR -and partition_mode = IDLE | COLD_START | WARM_START | NORMAL -and status = NOTCREATED | STOPPED | SUSPENDED | WAITING | READY | DONE -and waiting_for = NONE | BLACKBOARD | SEMA | EVENT | TIME -and queuing_discipline = FIFO | PRIO -[@@deriving show { with_path = false }, enum] - -let extract_types = ["t123"] (* TODO extract variables of a certain type *) - -let init ?(nproc=99) ?(nsema=99) ?(nevent=99) ?(nbboard=99) () = (* TODO better solution for the number of resources? the numbers are only for checking out-of-bounds accesses... *) - let has_semas = nsema > 0 in - let open Pml in let open Chan in - let nproc = fst @@ var (Byte nproc) "nproc" in - let nsema = fst @@ var (Byte nsema) "nsema" in - let nevent = fst @@ var (Byte nevent) "nevent" in - let nbboard = fst @@ var (Byte nbboard) "nbboard" in - - (* Pml.do_; (* ppx_monadic: from now on ; is bind *) *) - (* switched to ocaml-monadic because ppx_monadic was constraining us to ocaml <4.08, now have to use ;%bind instead of just ; and `let%bind x = e in` instead of `x <-- e;` *) - (* Dropped ocaml-monadic and used let* syntax introduced in OCaml 4.08. Use `let* () = e in` instead of `e;%bind` *) - - (* type delcarations, TODO generate this? *) - (* TODO might need adjustment if there are enums with gaps or enums not starting at 0 *) - let* () = enum return_code_of_enum show_return_code "return_code" in - let* () = enum partition_mode_of_enum show_partition_mode "partition_mode" in - let* () = enum status_of_enum show_status "status" in - let* () = enum waiting_for_of_enum show_waiting_for "waiting_for" in - let* () = enum queuing_discipline_of_enum show_queuing_discipline "queuing_discipline" in - (* variable declarations *) - (* TODO inject: let%s status = arr nprocNOTCREATED in *) - let* partition_mode = var (Enum (COLD_START, show_partition_mode)) "partition_mode" in - let* lock_level = var (Byte 0) "lock_level" in (* scheduling only takes place if this is 0 *) - let* exclusive = var (Byte 0) "exclusive" in (* id of process that has exclusive privilige toecute if lockLevel > 0 *) - let* status = arr !nproc (Enum (NOTCREATED, show_status)) "status" in - (* TODO type for structured data types *) - let* waiting_for = arr !nproc (Enum (NONE, show_waiting_for)) "waiting_for" in - let* waiting_id = arr !nproc (Byte 0) "waiting_id" in - let* () = Macro._if !nsema in - let* semas = arr !nsema (Byte 0) "semas" in - let* semas_max = arr !nsema (Byte 0) "semas_max" in - let* semas_chan = arr !nsema (Chan.create !nproc (Byte 0)) "semas_chan" in - let* () = Macro._endif in - let* () = Macro._if !nevent in - let* events = arr !nevent (Bool false) "events" in - let* () = Macro._endif in - let* () = Macro._if !nbboard in - let* bboards = arr !nbboard (Bool false) "bboards" in - let* () = Macro._endif in - - (* just for asserts *) - let* tasks_created = var (Byte 0) "tasks_created" in - let* semas_created = var (Byte 0) "semas_created" in - - (* dummy variables for use in arguments *) - let tid,tid_decl = var (Byte 0) "tid" in (* this is the id we give out for every new task *) - (* general arguments *) - let id,_ = var (Byte 0) "id" in - let name,_ = var (String "") "name" in - (*let r,_ = var (Enum (SUCCESS, show_return_code)) "r" in*) - - (* macros - used in extracted pml *) - let* () = Macro.define "can_run" @@ A1 (id, fun id -> (!status !id == e READY show_status) && (!lock_level == i 0 || !exclusive == !id) && (!partition_mode == e NORMAL show_partition_mode || !id == i 0)) in - - (* helpers - these get inlined *) - let task_info id = s "status["^i2s id^s "] = "^e2s (!status id)^s ", waiting_for[] = "^e2s (!waiting_for id)^s ", waiting_id[] = "^i2s (!waiting_id id) in - let sema_info id = s "semas["^i2s id^s "] = "^i2s (!semas id) in - let set_waiting id wfor wid = - let* () = println (s "set_waiting: process "^i2s id^s " will wait for "^i2s wid) in - let* () = waiting_for := id, (e wfor show_waiting_for) in - let* () = waiting_id := id, wid in - status := id, (e WAITING show_status) - in - let set_ready id = - let* () = println (s "set_ready: process "^i2s id^s " set to ready. "^task_info id) in - let* () = waiting_for := id, (e NONE show_waiting_for) in - let* () = waiting_id := id, i 0 in - status := id, (e READY show_status) - in - let is_waiting id wfor wid = !status id == e WAITING show_status && !waiting_for id == e wfor show_waiting_for && !waiting_id id == wid in - let remove_waiting id = - if has_semas then - _foreach semas (fun j _ -> - _ift (poll `Any (!semas_chan j) id) (recv `Any (!semas_chan j) id) - ) - else let* () = nop in - waiting_for := id, e NONE show_waiting_for - in - - (* preemption *) - let mode,_ = var (Enum (COLD_START, show_partition_mode)) "mode" in - let* () = extract "LockPreemption" @@ A0 ( - let* () = incr lock_level in - exclusive := !tid (* TODO is this really changed if lock_level > 0? if yes, it is probably also restored... *) - ) in - let* () = extract "UnlockPreemption" @@ A0 ( - _ift (!lock_level > i 0) (decr lock_level) - ) in - let* () = extract "SetPartitionMode" @@ A1 (mode, fun mode -> - partition_mode := !mode - ) in - - (* processes *) - let* () = extract "CreateProcess" @@ A1 (id(*; pri; per; cap]*), fun id -> - let* () = _assert (!status !id == e NOTCREATED show_status) in - let* () = status := !id, e STOPPED show_status in - let* () = waiting_for := !id, e NONE show_waiting_for in - incr tasks_created - ) in - (* CreateErrorHandler *) - let* () = extract "Start" @@ A1 (id, fun id -> - let* () = _assert (!status !id != e NOTCREATED show_status) in - let* () = remove_waiting !id in - status := !id, e READY show_status - ) in - let* () = extract "Stop" @@ A1 (id, fun id -> - let* () = _assert (!status !id != e NOTCREATED show_status) in - let* () = remove_waiting !id in - status := !id, e STOPPED show_status - ) in - let* () = extract "Suspend" @@ A1 (id, fun id -> - let* () = _assert (!status !id != e NOTCREATED show_status) in - status := !id, e SUSPENDED show_status - ) in - let* () = extract "Resume" @@ A1 (id, fun id -> - let* () = _assert (!status !id != e NOTCREATED show_status) in - let* () = _ift (!status !id == e SUSPENDED show_status) ( - _ifte (!waiting_for !id == e NONE show_waiting_for) - (status := !id, e READY show_status) - (status := !id, e WAITING show_status) - ) in - status := !id, e SUSPENDED show_status - ) in - - (* semaphores *) - let cur,_ = var (Byte 0) "cur" in - let max,_ = var (Byte 0) "max" in - let queuing,_ = var (Enum (FIFO, show_queuing_discipline)) "queuing" in - let* () = extract "CreateSemaphore" ~id:(4,0,"sema") @@ A5 (name,cur,max,queuing,id, fun name cur max queuing id -> - let* () = println (s "CreateSemaphore: " ^ !name ^s ", "^ i2s !cur ^s ", "^ i2s !max ^s ", "^ e2s !queuing) in - let* () = _assert (!queuing == e FIFO show_queuing_discipline) in - let* () = semas := !id, !cur in - let* () = semas_max := !id, !max in - incr semas_created - ) in - let* () = extract "GetSemaphoreId" ~id:(1,0,"sema") @@ A2 (name, id, fun name id -> skip) in - let* () = extract "WaitSemaphore" @@ A1 (id, fun id -> - let id = !id in - let sema = !semas id in - let chan = !semas_chan id in - _if [ - sema == i 0, - println (s "WaitSema will block: "^sema_info id) >> - _if [ - full chan, fail (s "WaitSema: queue is full: "^sema_info id); - nfull chan, println (s "WaitSema: Process "^i2s !tid^s " put into queue for sema "^i2s id) - ] >> - set_waiting !tid SEMA id; - sema > i 0, - println (s "WaitSema will go through: "^sema_info id) >> - incr semas id; - sema < i 0, - fail (s "WaitSema: count<0: "^sema_info id) - ] - ) in - extract "SignalSemaphore" @@ A1 (id, fun id -> - let id = !id in - let sema = !semas id in - let chan = !semas_chan id in - _if [ - (* no processes waiting on this semaphore -> increase count until max *) - empty chan, - println (s "SignalSema: empty queue") >> - _ift (sema < !semas_max id) (incr semas id); - nempty chan, - println (s "SignalSema: "^i2s (len chan)^s " processes in queue for "^sema_info id) >> - _foreach status (fun j _ -> - println (s "SignalSema: check if process "^i2s j^s " is waiting. "^task_info j) >> - _ift (is_waiting j SEMA id && poll `First chan j) (* process is waiting for this semaphore and is at the front of its queue *) ( - println (s "SignalSema: process "^i2s !tid^s " is waking up process "^i2s j) >> - recv `First chan j >> (* consume msg from queue *) - set_ready j >> - break - ) - ) - ] - ) - -(* events *)