diff --git a/ivette/src/frama-c/kernel/api/project/index.ts b/ivette/src/frama-c/kernel/api/project/index.ts index fdb80fc3c0cf81ac936ceb6c3fb56fe1d664248e..1d7aab341873243a4177aa2fd493ec9ab68ee374 100644 --- a/ivette/src/frama-c/kernel/api/project/index.ts +++ b/ivette/src/frama-c/kernel/api/project/index.ts @@ -59,47 +59,6 @@ export const byProjectInfo: Compare.Order<projectInfo> = current: Compare.boolean, }); -/** Request to be executed on the specified project. */ -export type projectRequest = - { project: Json.key<'#project'>, request: string, data: Json.json }; - -/** Decoder for `projectRequest` */ -export const jProjectRequest: Json.Decoder<projectRequest> = - Json.jObject({ - project: Json.jKey<'#project'>('#project'), - request: Json.jString, - data: Json.jAny, - }); - -/** Natural order for `projectRequest` */ -export const byProjectRequest: Compare.Order<projectRequest> = - Compare.byFields - <{ project: Json.key<'#project'>, request: string, data: Json.json }>({ - project: Compare.string, - request: Compare.string, - data: Compare.structural, - }); - -const getCurrent_internal: Server.GetRequest<null,projectInfo> = { - kind: Server.RqKind.GET, - name: 'kernel.project.getCurrent', - input: Json.jNull, - output: jProjectInfo, - signals: [], -}; -/** Returns the current project */ -export const getCurrent: Server.GetRequest<null,projectInfo>= getCurrent_internal; - -const setCurrent_internal: Server.SetRequest<Json.key<'#project'>,null> = { - kind: Server.RqKind.SET, - name: 'kernel.project.setCurrent', - input: Json.jKey<'#project'>('#project'), - output: Json.jNull, - signals: [], -}; -/** Switches the current project */ -export const setCurrent: Server.SetRequest<Json.key<'#project'>,null>= setCurrent_internal; - const getList_internal: Server.GetRequest<null,projectInfo[]> = { kind: Server.RqKind.GET, name: 'kernel.project.getList', @@ -110,36 +69,6 @@ const getList_internal: Server.GetRequest<null,projectInfo[]> = { /** Returns the list of all projects */ export const getList: Server.GetRequest<null,projectInfo[]>= getList_internal; -const getOn_internal: Server.GetRequest<projectRequest,Json.json> = { - kind: Server.RqKind.GET, - name: 'kernel.project.getOn', - input: jProjectRequest, - output: Json.jAny, - signals: [], -}; -/** Execute a GET request within the given project */ -export const getOn: Server.GetRequest<projectRequest,Json.json>= getOn_internal; - -const setOn_internal: Server.SetRequest<projectRequest,Json.json> = { - kind: Server.RqKind.SET, - name: 'kernel.project.setOn', - input: jProjectRequest, - output: Json.jAny, - signals: [], -}; -/** Execute a SET request within the given project */ -export const setOn: Server.SetRequest<projectRequest,Json.json>= setOn_internal; - -const execOn_internal: Server.ExecRequest<projectRequest,Json.json> = { - kind: Server.RqKind.EXEC, - name: 'kernel.project.execOn', - input: jProjectRequest, - output: Json.jAny, - signals: [], -}; -/** Execute an EXEC request within the given project */ -export const execOn: Server.ExecRequest<projectRequest,Json.json>= execOn_internal; - const create_internal: Server.SetRequest<string,projectInfo> = { kind: Server.RqKind.SET, name: 'kernel.project.create', diff --git a/ivette/src/frama-c/plugins/eva/CoverageMeter.tsx b/ivette/src/frama-c/plugins/eva/CoverageMeter.tsx index f0b14be5161dec099d2a46216529c522d157e379..fe6bcd419683c8c3b24736818d28ec88cf8472fc 100644 --- a/ivette/src/frama-c/plugins/eva/CoverageMeter.tsx +++ b/ivette/src/frama-c/plugins/eva/CoverageMeter.tsx @@ -32,10 +32,15 @@ export interface CoverageProps { coverage: Coverage; } - export function percent(coverage: Coverage): string { - const q = coverage.reachable / (coverage.reachable + coverage.dead); - return `${(q * 100).toFixed(1)}%`; + const n = coverage.reachable + coverage.dead; + if (n > 0) { + const r = coverage.reachable; + if (r > 0) { + const q = r / n; + return `${(q * 100).toFixed(1)}%`; + } else return '0%'; + } else return 'n/a'; } export default function CoverageMeter(props: CoverageProps): JSX.Element { diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts index 633839855c693832a08bb16eac4416248dc5dcec..d4f5c94ba9e6456f2dc163598f58a34b0b62610f 100644 --- a/ivette/src/frama-c/server.ts +++ b/ivette/src/frama-c/server.ts @@ -762,13 +762,9 @@ export function send<In, Out>( const response: Response<Out> = new Promise<Out>((resolve, reject) => { const unwrap = (js: Json.json): void => { try { - const data = request.output(js); - if (data !== undefined) - resolve(data); - else - reject('Wrong response type'); + resolve(request.output(js)); } catch (err) { - reject(`Decoding Error (${err})`); + reject(`Invalid ${request.name} response (${err})`); } }; pending.set(rid, { resolve: unwrap, reject }); diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts index a4287f3245ade58c1603fd6d8c93a4c4d3c46652..015479c34d1f76eed45af5c6e56f1fbd526595ee 100644 --- a/ivette/src/frama-c/states.ts +++ b/ivette/src/frama-c/states.ts @@ -36,74 +36,20 @@ import { Order } from 'dome/data/compare'; import { GlobalState, useGlobalState } from 'dome/data/states'; import { Client, useModel } from 'dome/table/models'; import { CompactModel } from 'dome/table/arrays'; -import { getCurrent, setCurrent } from 'frama-c/kernel/api/project'; import * as Ast from 'frama-c/kernel/api/ast'; import * as Server from './server'; -const CurrentProject = new GlobalState<string>(""); - // -------------------------------------------------------------------------- // --- Pretty Printing (Browser Console) // -------------------------------------------------------------------------- const D = new Dome.Debug('States'); -// -------------------------------------------------------------------------- -// --- Synchronized Current Project -// -------------------------------------------------------------------------- - -Server.onReady(async () => { - try { - CurrentProject.setValue(""); - const { id } = await Server.send(getCurrent, null); - CurrentProject.setValue(id); - } catch (error) { - D.error(`Fail to retrieve the current project. ${error}`); - } -}); - -Server.onShutdown(() => { - CurrentProject.setValue(""); -}); - -// -------------------------------------------------------------------------- -// --- Project API -// -------------------------------------------------------------------------- - -/** - * Current Project (Custom React Hook). - * @return The current project. - */ -export function useProject(): string { - const [s] = useGlobalState(CurrentProject); - return s; -} - -/** - * Update Current Project. - * - * Make all states switching to their projectified value. - * - * Emits `PROJECT`. - * @param project The project identifier. - */ -export async function setProject(project: string): Promise<void> { - if (Server.isRunning()) { - try { - await Server.send(setCurrent, project); - const { id } = await Server.send(getCurrent, null); - CurrentProject.setValue(id); - } catch (error) { - D.error(`Fail to set the current project. ${error}`); - } - } -} - // -------------------------------------------------------------------------- // --- Cached GET Requests // -------------------------------------------------------------------------- -/** Options to tweak the behavior of `useReques()`. Null values means +/** Options to tweak the behavior of `useRequest()`. Null values means keeping the last result. */ export interface UseRequestOptions<A> { /** Returned value in case where the server goes offline. */ @@ -131,39 +77,47 @@ export function useRequest<In, Out>( params: In | undefined, options: UseRequestOptions<Out> = {}, ): Out | undefined { - const state = React.useRef<string>(); - const project = useProject(); - const [response, setResponse] = - React.useState<Out | undefined>(options.offline ?? undefined); - const footprint = - project ? JSON.stringify([project, rq.name, params]) : undefined; - - const update = (opt: Out | undefined | null): void => { + const initial = options.offline ?? undefined; + const [response, setResponse] = React.useState<Out | undefined>(initial); + const updateResponse = (opt: Out | undefined | null): void => { if (opt !== null) setResponse(opt); }; + // Fetch Request async function trigger(): Promise<void> { - if (project !== "" && rq && params !== undefined) { + if (Server.isRunning() && params !== undefined) { try { - update(options.pending); + updateResponse(options.pending); const r = await Server.send(rq, params); - update(r); + updateResponse(r); } catch (error) { D.error(`Fail in useRequest '${rq.name}'. ${error}`); - update(options.onError); + updateResponse(options.onError); } } else { - update(options.offline); + updateResponse(options.offline); } } + // Server & Cache Management + Server.useStatus(); + const cached = React.useRef(''); React.useEffect(() => { - if (state.current !== footprint) { - state.current = footprint; - trigger(); + if (Server.isRunning()) { + const footprint = JSON.stringify([rq.name, params]); + if (cached.current !== footprint) { + cached.current = footprint; + trigger(); + } + } else { + if (cached.current !== '') { + cached.current = ''; + updateResponse(options.offline); + } } }); + // Signal Management const signals = rq.signals.concat(options.onSignals ?? []); React.useEffect(() => { signals.forEach((s) => Server.onSignal(s, trigger)); @@ -252,17 +206,14 @@ class SyncState<A> extends GlobalState<A | undefined> { constructor(h: Handler<A>) { super(undefined); this.handler = h; - this.load = this.load.bind(this); this.fetch = this.fetch.bind(this); - this.offline = this.offline.bind(this); - Server.onReady(this.load); - Server.onShutdown(this.offline); } signal(): Server.Signal { return this.handler.signal; } - load(): void { - if (this.status === SyncStatus.OffLine) this.fetch(); + online(): void { + if (Server.isRunning() && this.status === SyncStatus.OffLine) + this.fetch(); } offline(): void { @@ -295,22 +246,19 @@ class SyncState<A> extends GlobalState<A | undefined> { const syncStates = new Map<string, SyncState<unknown>>(); -// Remark: use current project state - -function lookupSyncState<A>( - currentProject: string, - h: Handler<A> -): SyncState<A> { - const id = `${currentProject}@${h.name}`; - let s = syncStates.get(id) as SyncState<A> | undefined; +function lookupSyncState<A>(h: Handler<A>): SyncState<A> { + let s = syncStates.get(h.name) as SyncState<A> | undefined; if (!s) { s = new SyncState(h); - syncStates.set(id, s); + syncStates.set(h.name, s); } return s; } -Server.onShutdown(() => syncStates.clear()); +Server.onShutdown(() => { + syncStates.forEach((st) => st.offline()); + syncStates.clear(); +}); // -------------------------------------------------------------------------- // --- Synchronized State Hooks @@ -321,20 +269,18 @@ export function useSyncState<A>( state: State<A>, ): [A | undefined, (value: A) => void] { Server.useStatus(); - const pr = useProject(); - const st = lookupSyncState(pr, state); + const st = lookupSyncState(state); Server.useSignal(st.signal(), st.fetch); - st.load(); + st.online(); return useGlobalState(st); } /** Synchronization with a (projectified) server value. */ export function useSyncValue<A>(value: Value<A>): A | undefined { Server.useStatus(); - const pr = useProject(); - const st = lookupSyncState(pr, value); + const st = lookupSyncState(value); Server.useSignal(st.signal(), st.fetch); - st.load(); + st.online(); const [v] = useGlobalState(st); return v; } @@ -357,21 +303,20 @@ class SyncArray<K, A> { this.model.setNaturalOrder(h.order); this.fetch = this.fetch.bind(this); this.reload = this.reload.bind(this); - this.update = this.update.bind(this); } - update(): void { - if ( - !this.upToDate && - Server.isRunning() - ) this.fetch(); + online(): void { + if (!this.upToDate && Server.isRunning()) + this.fetch(); + } + + offline(): void { + this.upToDate = false; + this.model.clear(); } async fetch(): Promise<void> { - if ( - this.fetching || - !Server.isRunning() - ) return; + if (this.fetching || !Server.isRunning()) return; try { this.fetching = true; let pending; @@ -425,20 +370,19 @@ const syncArrays = new Map<string, SyncArray<unknown, unknown>>(); // Remark: lookup for current project -function currentSyncArray<K, A>( - currentProject: string, - array: Array<K, A>, -): SyncArray<K, A> { - const id = `${currentProject}@${array.name}`; - let st = syncArrays.get(id) as SyncArray<K, A> | undefined; +function currentSyncArray<K, A>(array: Array<K, A>): SyncArray<K, A> { + let st = syncArrays.get(array.name) as SyncArray<K, A> | undefined; if (!st) { st = new SyncArray(array); - syncArrays.set(id, st as SyncArray<unknown, unknown>); + syncArrays.set(array.name, st as SyncArray<unknown, unknown>); } return st; } -Server.onShutdown(() => syncArrays.clear()); +Server.onShutdown(() => { + syncArrays.forEach((st) => st.offline()); + syncArrays.clear(); +}); // -------------------------------------------------------------------------- // --- Synchronized Array Hooks @@ -446,7 +390,7 @@ Server.onShutdown(() => syncArrays.clear()); /** Force a Synchronized Array to reload. */ export function reloadArray<K, A>(arr: Array<K, A>): void { - currentSyncArray(CurrentProject.getValue(), arr).reload(); + currentSyncArray(arr).reload(); } /** @@ -463,10 +407,9 @@ export function useSyncArray<K, A>( sync = true, ): CompactModel<K, A> { Server.useStatus(); - const pr = useProject(); - const st = currentSyncArray(pr, arr); + const st = currentSyncArray(arr); Server.useSignal(arr.signal, st.fetch); - st.update(); + st.online(); useModel(st.model, sync); return st.model; } @@ -477,8 +420,7 @@ export function useSyncArray<K, A>( export function getSyncArray<K, A>( arr: Array<K, A>, ): CompactModel<K, A> { - const pr = CurrentProject.getValue(); - const st = currentSyncArray(pr, arr); + const st = currentSyncArray(arr); return st.model; } @@ -492,8 +434,7 @@ export function onSyncArray<K, A>( onReload?: () => void, onUpdate?: () => void, ): Client { - const pr = CurrentProject.getValue(); - const st = currentSyncArray(pr, arr); + const st = currentSyncArray(arr); return st.model.link(onReload, onUpdate); } diff --git a/src/plugins/server/kernel_project.ml b/src/plugins/server/kernel_project.ml index bae9e6271368e6af361c00236ebe0f39de19b8d8..91252b560d956180b82515a9c981336412c4137b 100644 --- a/src/plugins/server/kernel_project.ml +++ b/src/plugins/server/kernel_project.ml @@ -61,6 +61,7 @@ end (* --- Project Requests --- *) (* -------------------------------------------------------------------------- *) +(* module ProjectRequest = struct @@ -90,11 +91,13 @@ struct | None -> failwith (Printf.sprintf "Request '%s' undefined" request) end +*) (* -------------------------------------------------------------------------- *) (* --- Project Requests --- *) (* -------------------------------------------------------------------------- *) +(* let () = Request.register ~package ~kind:`GET ~name:"getCurrent" ~descr:(Md.plain "Returns the current project") @@ -106,6 +109,7 @@ let () = Request.register ~package ~descr:(Md.plain "Switches the current project") ~input:(module ProjectId) ~output:(module Junit) (fun pid -> Project.(set_current (from_unique_name pid))) +*) let () = Request.register ~package ~kind:`GET ~name:"getList" @@ -113,6 +117,7 @@ let () = Request.register ~package ~input:(module Junit) ~output:(module Jlist(ProjectInfo)) (fun () -> Project.fold_on_projects (fun ids p -> p :: ids) []) +(* let () = Request.register ~package ~kind:`GET ~name:"getOn" ~descr:(Md.plain "Execute a GET request within the given project") @@ -130,6 +135,7 @@ let () = Request.register ~package ~descr:(Md.plain "Execute an EXEC request within the given project") ~input:(module ProjectRequest) ~output:(module Jany) (ProjectRequest.process `EXEC) +*) (* -------------------------------------------------------------------------- *) (* --- Project Management --- *) diff --git a/src/plugins/server/kernel_project.mli b/src/plugins/server/kernel_project.mli index 62f4b23a0e6514ba454ad86278a6418aa2749f6c..99b3014dd15d2ab177838bb6bbb546e424dbd69b 100644 --- a/src/plugins/server/kernel_project.mli +++ b/src/plugins/server/kernel_project.mli @@ -20,13 +20,10 @@ (* *) (**************************************************************************) -open Data - (* -------------------------------------------------------------------------- *) (** Project Services *) (* -------------------------------------------------------------------------- *) module ProjectInfo : Data.S with type t = Project.t -module ProjectRequest : Request.Input with type t = Project.t * string * json (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml index b508302a5ac43957ff836690ae30bf0bb7399a75..06d8471f772e6b7712291d9b7961f187290d5791 100644 --- a/src/plugins/server/main.ml +++ b/src/plugins/server/main.ml @@ -108,8 +108,9 @@ type 'a server = { q_in : 'a pending Queue.t ; (* queue of pending `EXEC and `GET jobs *) q_out : 'a response Queue.t ; (* queue of pending responses *) mutable daemon : Db.daemon option ; (* Db.yield daemon *) - mutable s_active : Signals.t ; (* signals the client is listening to *) - mutable s_signal : Signals.t ; (* emitted signals since last synchro *) + mutable s_listen : Signals.t ; (* signals the client is listening to *) + mutable s_emitted : Signals.t ; (* emitted signals enqueued *) + mutable s_pending : Signals.t ; (* emitted signals not enqueued yet *) mutable shutdown : bool ; (* server has been asked to shut down *) mutable running : 'a running ; (* server running state *) mutable cmdline : bool option ; (* cmdline signal management *) @@ -254,12 +255,18 @@ let process_request (server : 'a server) (request : 'a request) : unit = end | `SigOn sg -> begin - server.s_active <- Signals.add sg server.s_active ; + server.s_listen <- Signals.add sg server.s_listen ; + if Signals.mem sg server.s_pending then + begin + server.s_emitted <- Signals.add sg server.s_emitted ; + server.s_pending <- Signals.remove sg server.s_pending ; + Queue.push (`Signal sg) server.q_out ; + end ; notify sg true ; end | `SigOff sg -> begin - server.s_active <- Signals.remove sg server.s_active ; + server.s_listen <- Signals.remove sg server.s_listen ; notify sg false ; end | `Kill id -> @@ -307,7 +314,7 @@ let communicate server = pool := List.rev !pool ; Queue.clear server.q_out ; server.cmdline <- None ; - server.s_signal <- Signals.empty ; + server.s_emitted <- Signals.empty ; Senv.debug ~level:2 "response(s) callback" ; if Senv.debug_atleast 2 then List.iter (Senv.debug "%a" (pp_response server.pretty)) !pool ; @@ -324,11 +331,16 @@ let do_yield server () = ignore ( communicate server ) let do_signal server s = - if Signals.mem s server.s_active && not (Signals.mem s server.s_signal) then + if Signals.mem s server.s_listen then begin - server.s_signal <- Signals.add s server.s_signal ; - Queue.push (`Signal s) server.q_out ; + if not (Signals.mem s server.s_emitted) then + begin + server.s_emitted <- Signals.add s server.s_emitted ; + Queue.push (`Signal s) server.q_out ; + end end + else + server.s_pending <- Signals.add s server.s_pending (* -------------------------------------------------------------------------- *) (* --- One Step Process --- *) @@ -380,8 +392,9 @@ let create ~pretty ?(equal=(=)) ~fetch () = fetch ; polling ; equal ; pretty ; q_in = Queue.create () ; q_out = Queue.create () ; - s_active = Signals.empty ; - s_signal = Signals.empty ; + s_listen = Signals.empty ; + s_emitted = Signals.empty ; + s_pending = Signals.empty ; daemon = None ; running = Idle ; cmdline = None ;